Skip to content

Instantly share code, notes, and snippets.

@ChrisHughes24

ChrisHughes24/zorn_category

Created May 29, 2023 08:47
Show Gist options
  • Save ChrisHughes24/e97dcf6be2b0e67449ab0fa1f5540d58 to your computer and use it in GitHub Desktop.
Save ChrisHughes24/e97dcf6be2b0e67449ab0fa1f5540d58 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
zorn_category
import order.zorn
import category_theory.category.preorder
import category_theory.limits.cones
universes u v w
namespace category_theory
open limits
open set
variables (C : Type u) [category.{v} C]
#print is_linear_order
structure chain :=
( objs : set C )
( rel : objs → objs → Prop )
[ lin : is_linear_order _ rel ]
( of_rel : ∀ X Y : objs, rel X Y → ((X : C) ⟶ (Y : C)) )
( of_rel_refl : ∀ X (hX : rel X X), of_rel X X ‹_› = 𝟙 X )
( of_rel_trans : ∀ (X Y Z : objs) (hXY hYZ hXZ), of_rel X Y ‹_› ≫ of_rel Y Z ‹_› = of_rel X Z ‹_› )
attribute [instance] chain.lin
instance : partial_order (chain C) :=
{ le := λ c₁ c₂,
∃ h : c₁.objs ⊆ c₂.objs,
∃ (f : ∀ X Y : c₁.objs, c₁.rel X Y → c₂.rel (set.inclusion h X) (set.inclusion h Y)),
∀ X Y h, c₁.of_rel X Y h = c₂.of_rel _ _ (f _ _ h),
le_refl := λ _, ⟨subset_refl _, λ _ _, by simp, λ X Y _, by cases X; cases Y; refl⟩,
le_trans := λ a b c hab hbc, ⟨hab.fst.trans hbc.fst,
λ X Y hXY, hbc.snd.fst _ _ (hab.snd.fst X Y hXY),
λ X Y hXY, (hab.snd.snd _ _ hXY).trans (hbc.snd.snd _ _ _)⟩,
le_antisymm := λ a b hab hba,
begin
cases a with a arel _ aof_rel arefl atrans,
cases b with b brel _ bof_rel brefl btrans,
have : a = b := set.subset.antisymm hab.fst hba.fst,
subst b,
have : arel = brel,
{ ext x y,
cases x with x hx,
cases y with y hy,
exact ⟨hab.snd.fst _ _, hba.snd.fst _ _⟩ },
subst brel,
have : aof_rel = bof_rel,
{ ext x y hxy,
cases x with x hx,
cases y with y hy,
exact hab.snd.snd _ _ _ },
subst bof_rel
end }
variable {C}
@[simps]
noncomputable def chain_max (s : set (chain C)) (hs : is_chain (≤) s) : chain C :=
let objs := ⋃ (c : s), c.1.objs in
let rel : objs → objs → Prop := λ x y, ∃ (c : s) (hx : x.1 ∈ c.1.objs) (hy : y.1 ∈ c.1.objs),
(c.1.rel ⟨x.1, hx⟩ ⟨y.1, hy⟩) in
have tot : is_total _ rel :=
⟨begin
rintros ⟨x, hx⟩ ⟨y, hy⟩,
rcases mem_Union.1 hx with ⟨⟨cx, hxs⟩, hxc⟩,
rcases mem_Union.1 hy with ⟨⟨cy, hys⟩, hyc⟩,
rcases hs.directed_on _ hxs _ hys with ⟨c, hcs, hc⟩,
have : c.rel ⟨x, hc.1.fst hxc⟩ ⟨y, hc.2.fst hyc⟩ ∨ _ :=
is_total.total _ _,
rcases this with hxy | hyx,
{ left,
use [c, hcs, hc.1.fst hxc, hc.2.fst hyc, hxy] },
{ right,
use [c, hcs, hc.2.fst hyc, hc.1.fst hxc, hyx] }
end⟩,
have ant : is_antisymm _ rel :=
⟨begin
rintros ⟨x, hx⟩ ⟨y, hy⟩ ⟨c₁, hxc₁, hyc₁, hr₁⟩ ⟨c₂, hxc₂, hyc₂, hr₂⟩,
rcases hs.directed_on _ c₁.prop _ c₂.prop with ⟨c, hcs, hc⟩,
simpa using antisymm (hc.1.snd.fst _ _ hr₁) (hc.2.snd.fst _ _ hr₂)
end⟩,
have ref : is_refl _ rel :=
⟨begin
rintros ⟨x, hx⟩,
rcases mem_Union.1 hx with ⟨⟨cx, hxs⟩, hxc⟩,
use [cx, hxs, hxc, hxc, is_refl.refl _]
end⟩,
have tran : is_trans _ rel :=
⟨begin
rintros ⟨x, hx⟩ ⟨y, hy⟩ ⟨z, hz⟩ ⟨c₁, hxc₁, hyc₁, hr₁⟩ ⟨c₂, hyc₂, hzc₂, hr₂⟩,
rcases hs.directed_on _ c₁.prop _ c₂.prop with ⟨c, hcs, hc⟩,
have := hc.1.fst hyc₁,
use [c, hcs, hc.1.fst hxc₁, hc.2.fst hzc₂],
exact trans (hc.1.snd.fst _ _ hr₁) (hc.2.snd.fst _ _ hr₂)
end⟩,
{ objs := objs,
rel := rel,
lin := by resetI; exact {},
of_rel := λ x y hxy,
hxy.some.1.of_rel ⟨x.1, hxy.some_spec.fst⟩ ⟨y.1, hxy.some_spec.snd.fst⟩ hxy.some_spec.snd.snd,
of_rel_refl := λ x hx, hx.some.1.of_rel_refl _ _,
of_rel_trans := begin
rintros X Y Z hX hY hZ,
rcases hs.exists3 hX.some.2 hY.some.2 hZ.some.2 with ⟨c, hcs, hcc₁, hcc₂, hcc₃⟩,
dsimp,
erw [hcc₁.snd.snd, hcc₂.snd.snd, hcc₃.snd.snd],
exact c.of_rel_trans _ _ _ _ _ _
end }
instance : nonempty (chain C) := ⟨chain_max ∅ is_chain_empty⟩
theorem le_chain_max {s : set (chain C)} {hs : is_chain (≤) s} {c : chain C}
(hc : c ∈ s) : c ≤ chain_max s hs :=
begin
fsplit,
{ exact subset_Union (λi : s, i.1.objs) (⟨c, hc⟩ : s) },
fsplit,
{ rintros ⟨X, hX⟩ ⟨Y, hY⟩ hXY,
dsimp [chain_max],
use [⟨c, hc⟩, hX, hY, hXY] },
{ rintros ⟨X, hX⟩ ⟨Y, hY⟩ hXY,
dsimp [chain_max],
have : ∃ (c : s) (hX : X ∈ c.1.objs) (hY : Y ∈ c.1.objs), c.1.rel ⟨X, hX⟩ ⟨Y, hY⟩ :=
⟨⟨c, hc⟩, hX, hY, hXY⟩,
rcases hs.directed_on _ hc _ this.some.2 with ⟨m, hms, hm⟩,
erw [hm.1.snd.snd, hm.2.snd.snd],
refl }
end
open_locale classical
noncomputable def chain.insert (c : chain C) (X : C) (f : ∀ Y : c.objs, (Y : C) ⟶ X)
(f_trans : ∀ X Y (h : c.rel X Y), c.of_rel X Y h ≫ f Y = f X)
(hxC : X ∉ c.objs) : chain C :=
let objs := c.objs ∪ {X} in
let rel : objs → objs → Prop :=
λ A B, X = B ∨ ∃ (hA : A.1 ∈ c.objs) (hB : B.1 ∈ c.objs), c.rel ⟨A.1, hA⟩ ⟨B.1, hB⟩ in
have tot : is_total _ rel :=
⟨begin
rintros ⟨A, hA⟩ ⟨B, hB⟩,
simp only [set.mem_insert_iff, set.union_singleton, objs] at hA hB,
rcases hB with rfl | hB,
{ dsimp [rel], simp },
{ rcases hA with rfl | hA,
{ dsimp [rel], simp },
{ rcases (is_total.total ⟨A, hA⟩ ⟨B, hB⟩ : c.rel _ _ ∨ _) with h | h,
{ left, right, exact ⟨hA, hB, h⟩ },
{ right, right, exact ⟨hB, hA, h⟩ } } }
end⟩,
have ant : is_antisymm _ rel :=
⟨begin
rintros ⟨A, hA⟩ ⟨B, hB⟩ hAB hBA,
simp only [set.mem_insert_iff, set.union_singleton, objs] at hA hB,
dsimp [rel] at hAB hBA,
rcases hA with rfl | hA,
{ rcases hB with rfl | hB,
{ refl },
{ have hAnB : A ≠ B := by rintro rfl; contradiction,
exact (hxC (hAB.resolve_left hAnB).fst).elim } },
{ have hXnA : X ≠ A := by rintro rfl; contradiction,
have : B ∈ c.objs := (hBA.resolve_left hXnA).fst,
have hXnB : X ≠ B := by rintro rfl; contradiction,
simpa using antisymm (hAB.resolve_left hXnB).snd.snd (hBA.resolve_left hXnA).snd.snd }
end⟩,
have ref : is_refl _ rel :=
⟨begin
rintros ⟨A, hA⟩,
dsimp [rel] at hA,
rcases hA with hA | rfl,
{ dsimp [rel], simp [hA, @is_refl.refl _ c.rel _] },
{ dsimp [rel], simp }
end⟩,
have tran : is_trans _ rel :=
⟨begin
rintros ⟨A, hA⟩ ⟨B, hB⟩ ⟨C, hC⟩ hAB hBC,
dsimp [objs, rel] at hAB hBC,
rcases hBC with rfl | hBC,
{ left, refl },
{ rcases hAB with rfl | hAB,
{ exact (hxC hBC.fst).elim },
{ right, exact ⟨hAB.fst, hBC.snd.fst, trans hAB.snd.snd hBC.snd.snd⟩ } }
end⟩,
{ objs := c.objs ∪ {X},
rel := λ A B, X = B ∨ ∃ (hA : A.1 ∈ c.objs) (hB : B.1 ∈ c.objs), c.rel ⟨A.1, hA⟩ ⟨B.1, hB⟩,
lin := by resetI; exact {},
of_rel := λ A B hAB,
if hB : X = B
then if hA : X = A
then begin
resetI,
cases A with A hAc, cases B with B hBc,
dsimp at hA hB,
simp [← hA, hB],
exact 𝟙 _
end
else by rw [← hB];
exact f ⟨A, by simpa [ne.symm hA] using A.prop⟩
else c.of_rel ⟨A, (hAB.resolve_left hB).fst⟩
⟨B, (hAB.resolve_left hB).snd.fst⟩ (hAB.resolve_left hB).snd.snd,
of_rel_refl := begin
rintros ⟨A, hAc⟩ hA,
split_ifs with h,
{ cases h, refl },
{ exact c.of_rel_refl _ _ }
end,
of_rel_trans := begin
rintros ⟨A, hAc⟩ ⟨B, hBc⟩ ⟨D, hDc⟩ hAB hBD hAD,
dsimp,
split_ifs with hXB hXA hXC hXD,
{ substs X A D, simp },
{ substs X B, simp },
{ substs X B, simp },
{ subst B, exact (hxC (hBD.resolve_left hXD).fst).elim },
{ substs X A, exact (hxC (hAB.resolve_left hXB).fst).elim },
{ subst X, simp [f_trans] },
{ exact c.of_rel_trans _ _ _ _ _ _ }
end }
theorem chain.lt_insert (c : chain C) (X : C) (f : ∀ Y : c.objs, (Y : C) ⟶ X)
(f_trans : ∀ X Y (h : c.rel X Y), c.of_rel X Y h ≫ f Y = f X)
(hxC : X ∉ c.objs) : c < c.insert X f f_trans hxC :=
begin
apply lt_of_le_of_ne,
{ fsplit,
{ simp [chain.insert] },
fsplit,
{ rintros ⟨A, hA⟩ ⟨B, hB⟩ hAB, right, exact ⟨hA, hB, hAB⟩ },
{ rintros ⟨A, hA⟩ ⟨B, hB⟩ hAB,
have hXB : X ≠ B,
{ rintros rfl, exact hxC hB },
have hXA : X ≠ A,
{ rintros rfl, exact hxC hA },
dsimp [chain.insert], simp *, } },
{ intro h,
have h : c.objs = c.objs ∪ {X} := congr_arg chain.objs h,
exact hxC (h.symm ▸ by simp) }
end
variable (C)
theorem exists_maximal_chain : ∃ c₁ : chain C, ∀ c₂ : chain C, c₁ ≤ c₂ → c₂ = c₁ :=
zorn_partial_order (λ s hs, ⟨chain_max s hs, λ _, le_chain_max⟩)
noncomputable def max_chain : chain C := (exists_maximal_chain C).some
theorem max_chain_spec : ∀ c : chain C, max_chain C ≤ c → c = max_chain C :=
(exists_maximal_chain C).some_spec
noncomputable def chain.linear_order (c : chain C) : linear_order c.objs :=
{ le := c.rel,
le_trans := λ _ _ _, trans,
le_refl := λ _, is_refl.refl _,
le_antisymm := λ _ _ hAB hBA, antisymm hAB hBA,
le_total := is_total.total,
decidable_le := classical.dec_rel _}
variable {C}
theorem zorn_category_chain (h : ∀ c : chain C, ∃ M : C,
∃ f : ∀ X : c.objs, (X : C) ⟶ M, ∀ X Y (h : c.rel X Y), c.of_rel X Y h ≫ f Y = f X) :
∃ M : C, ∀ X : C, (M ⟶ X) → nonempty (X ⟶ M) :=
begin
rcases exists_maximal_chain C with ⟨c, hc⟩,
rcases h c with ⟨M, f, hf⟩,
use M,
intros X g,
by_cases hXc : X ∈ c.objs,
{ exact ⟨f ⟨X, hXc⟩⟩ },
{ have h := c.lt_insert X (λ X, f X ≫ g) (by intros; rw [← category.assoc, hf]) hXc,
exact (ne_of_gt h (hc _ (le_of_lt h))).elim }
end
local attribute [instance] chain.linear_order
theorem zorn_category {C : Type u} [category.{v} C]
(h : ∀ (ι : Type u) [linear_order ι], by exactI ∀ (F : ι ⥤ C), nonempty (cocone F)) :
∃ M : C, ∀ X : C, (M ⟶ X) → nonempty (X ⟶ M) :=
zorn_category_chain begin
intro c,
have := h c.objs
{ obj := λ X : c.objs, (X : C),
map := λ X Y ⟨⟨f⟩⟩, c.of_rel _ _ f,
map_id' := begin rintros ⟨x, hx⟩, dsimp, simp [c.of_rel_refl], refl end,
map_comp' := begin rintro ⟨x, hx⟩ ⟨y, hy⟩ ⟨z, hz⟩⟨⟨f⟩⟩ ⟨⟨g⟩⟩,
dsimp, rw [c.of_rel_trans], refl end },
rcases this with ⟨M, f, hf⟩,
dsimp at f hf,
use [M, f],
rintros ⟨X, hXc⟩ ⟨Y, hYc⟩ hXY,
have := hf ⟨⟨hXY⟩⟩,
simp only [category_theory.category.comp_id] at this,
rw [← this]
end
end category_theory
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment