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