CreatesLimit.lean

import Mathlib.tactic
import Mathlib.CategoryTheory.Limits.Creates


open CategoryTheory
open Limits

#check LiftableCone
/-
  c : Cone (K ⋙ F) がLiftable
  := F.mapCone c' ≅ c となる c' : Cone K が存在
-/

#check ReflectsLimit
/-
  F : C ⥤ D が K : J ⥤ C の極限を反映する
  := 任意の c : Cone K に対して、F.mapCone c が極限なら c も極限
-/

#print PreservesLimit
/-
  F : C ⥤ D が K : J ⥤ C の極限を保存する
  := 任意の c : Cone K に対して、c が極限なら F.mapCone c も極限
-/

#check CreatesLimit
/-
  F が K の極限を創出する
  := F が K の極限を反映し、かつ
     任意の　c : Cone (K ⋙ F) に対して、cが極限ならば c はLiftable
-/


#check IsLimit.uniqueUpToIso
def ConeIso [Category J] [Category C] {F : J ⥤ C} {c c' : Cone F} (Hc : IsLimit c) (Hc' : IsLimit c') :
  c ≅ c'
:= {
  hom := {
    hom := Hc'.lift c
    w := by simp
  }
  inv := {
    hom := Hc.lift c'
    w := by simp
  }
  hom_inv_id := by
    ext; simp
    have E := Hc.uniq c (Hc'.lift c ≫ Hc.lift c')
    rw [E]; swap; simp
    have E := Hc.uniq c (𝟙 _)
    rw [E]; simp
  inv_hom_id := by
    ext; simp
    have E := Hc'.uniq c' (Hc.lift c' ≫ Hc'.lift c)
    rw [E]; swap; simp
    have E := Hc'.uniq c' (𝟙 _)
    rw [E]; simp
}

#check HasLimit
example
  [Category J] [Category C] [Category D] (F : C ⥤ D) (K : J ⥤ C)
  (H₁ : CreatesLimit K F) (H₂ : HasLimit (K ⋙ F)) :
  HasLimit K ∧ PreservesLimit K F
:= by
  let lift := H₁.lifts
  have HR := H₁.toReflectsLimit
  have ⟨c, Hc⟩ := H₂.1.some
  have ⟨c', Hc'⟩ := lift c Hc
  have HR' := HR.reflects (c := c')
  refine ⟨?H1, ?H2⟩
  · constructor; constructor
    use c'
    suffices : IsLimit (F.mapCone c')
    exact (HR' this).some
    refine {
      lift s := Hc.lift s ≫ Hc'.inv.hom
      fac s j := by
        simp
        have E := Hc'.inv.w j; simp at E
        rw [<- Hc.fac s j, E]
      uniq s m Hm := by
        rw [<- Category.comp_id m]
        have E := Hc'.hom_inv_id
        injection E with E
        rw [<- E]; clear E
        have E := Hc.uniq s (m ≫ Hc'.hom.hom)
        rw [<- Category.assoc, E]; clear E
        intro j; simp
        have E := Hm j; simp at E
        rw [E]
    }
  · constructor
    intro d Hd; constructor
    refine {
      lift s := Hc.lift s ≫ Hc'.inv.hom ≫ F.map (Hd.lift c')
      fac s j := by
        simp
        have Ed := Hd.fac c' j
        rw [<- F.map_comp, Hd.fac c' j]
        have E := Hc'.inv.w j
        conv at E => arg 1; simp
        rw [E]
        have Ec := Hc.fac s j
        rw [Ec]
      uniq s m Hm := by
        have H : IsLimit (F.mapCone c') := {
          lift e := Hc.lift e ≫ Hc'.inv.hom
          fac e j := by
            simp
            have E := Hc'.inv.w j; simp at E
            rw [E]; simp
          uniq e n Hn := by
            simp at n Hn
            have E := Hc.uniq e (n ≫ Hc'.hom.hom)
            rw [<- E]; simp; clear E
            have E := Hc'.hom_inv_id; injection E with E; rw [E]; simp
            intro j; simp; rw [Hn]
        }
        have H' := (HR' H).some

        simp at m Hm
        have Es := H.uniq s (m ≫ F.map (H'.lift d)); simp at Es
        have Es' := Hc.uniq s (H.lift s ≫ Hc.lift (F.mapCone c')); simp at Es'
        rw [<- Es']; swap
        · intro j
          have := H.fac s j; simp at this; rw [this]
        rw [<- Es]; swap
        · intro j
          rw [<- F.map_comp, H'.fac d j, Hm]
        simp
        have Ec' := Hc.uniq (F.mapCone c') Hc'.hom.hom; simp at Ec'
        have E := Hc'.hom_inv_id; injection E with E
        slice_rhs 3 4 => rw [<- Ec', E]
        simp; clear Ec' E
        rw [<- F.map_comp]
        have : H'.lift d ≫ Hd.lift c' = 𝟙 _ := by
          have := Hd.uniq d (H'.lift d ≫ Hd.lift c')
          rw [this]; swap; simp
          have := Hd.uniq d (𝟙 _)
          rw [this]; simp
        rw [this]; simp

    }
#check ReflectsLimit
lemma IsEquivalence.reflectsLilmit [Category J] [Category C] [Category D] (F : C ⥤ D) (K : J ⥤ C) (H : F.FullyFaithful) :
  ReflectsLimit K F
:= by
  apply ReflectsLimit.mk ?_
  intro c Hc; constructor
  rcases H with ⟨inv, mapInv, invMap⟩
  refine {
    lift s := inv (Hc.lift (F.mapCone s))
    fac s j := by
      rw [<- invMap (inv (Hc.lift (F.mapCone s)) ≫ c.π.app j)]; simp
      rw [mapInv]
      have E := Hc.fac (F.mapCone s) j; simp at E
      rw [<- invMap (s.π.app j), <- E]
    uniq s m Hm := by
      have E := Hc.uniq (F.mapCone s) (F.map m)
      rw [<- E, invMap]
      intro j; simp
      rw [<- F.map_comp, Hm]
  }

noncomputable def IsEquivalence.mkCone
  [Category J] [Category C] [Category D]
  {F : C ⥤ D} {K : J ⥤ C} (H : F.IsEquivalence) (s : Cone (K ⋙ F)) :
  Cone K
:= by
  let Hs := H.essSurj.mem_essImage s.pt
  let σ := Hs.choose_spec.some
  set x := Hs.choose
  refine {
    pt := x
    π := {
      app j := (F.map_surjective (σ.hom ≫ s.π.app j)).choose
      naturality {j j'} f := by
        set H := F.map_surjective (σ.hom ≫ s.π.app j)
        set H' := F.map_surjective (σ.hom ≫ s.π.app j')
        have Hy := H.choose_spec
        have Hy' := H'.choose_spec
        set y := H.choose
        set y' := H'.choose
        simp
        apply F.map_injective; simp
        rw [Hy, Hy']; simp
        have := s.π.naturality f; simp at this
        rw [this]
    }
  }



def IsEquivalence.PreservesLimits [Category J] [Category C] [Category D] (F : C ⥤ D) (K : J ⥤ C) (H : F.IsEquivalence) :
  PreservesLimit K F
:= by
  constructor; intro c Hc; constructor
  refine {
    lift s := (((H.essSurj.mem_essImage) s.pt).choose_spec.some).inv ≫ F.map (Hc.lift (mkCone H s))
    fac s j := by
      simp
      set σ := ((H.essSurj.mem_essImage) s.pt).choose_spec.some
      rw [<- F.map_comp]
      have E := Hc.fac (mkCone H s) j
      rw [E]
      simp [mkCone]
      set H' := (F.map_surjective (σ.hom ≫ s.π.app j))
      slice_lhs 2 2 => change H'.choose
      have E := H'.choose_spec
      rw [E]; simp
    uniq s m Hm := by
      simp at m Hm
      have Hs := (H.essSurj.mem_essImage) s.pt
      set x := Hs.choose
      set σ : F.obj x ≅ s.pt := Hs.choose_spec.some
      let H' := F.map_surjective (σ.hom ≫ m)
      let Hf := H'.choose_spec
      set f := H'.choose
      have E := Hc.uniq (mkCone H s) f; simp at E
      rw [<- E, Hf]; simp
      intro j; simp [mkCone]
      set Hs := (F.map_surjective (σ.hom ≫ s.π.app j))
      conv => arg 2; change Hs.choose
      have E := Hs.choose_spec
      apply F.map_injective; simp
      rw [Hf, E]; simp
      rw [Hm j]
  }

noncomputable def IsEquivalence.CreatesLimits [Category J] [Category C] [Category D] (F : C ⥤ D) (K : J ⥤ C) (H : F.IsEquivalence) :
  CreatesLimit K F
:= by
  constructor
  intro c Hc
  use mkCone H c
  refine IsLimit.uniqueUpToIso ?_ Hc
  refine {
    lift s := by
      simp [mkCone]
      let Hs := H.essSurj.mem_essImage c.pt
      let σ := Hs.choose_spec.some
      set x := Hs.choose
      change s.pt ⟶ F.obj x
      exact Hc.lift s ≫ σ.inv
    fac s j := by
      simp
      have E := Hc.fac s j
      simp [mkCone]
      set Hs := H.essSurj.mem_essImage c.pt
      set x := Hs.choose
      set σ : F.obj x ≅ c.pt := Hs.choose_spec.some
      let f := σ.hom ≫ c.π.app j
      have E := F.map_surjective f
      let g := E.choose
      have Hg : F.map g = f := E.choose_spec
      conv => arg 1; arg 2; arg 1; change σ.inv
      conv => arg 1; arg 2; arg 2; change F.map E.choose
      rw [Hg]; simp [f]
    uniq s m Hm := by
      simp
      simp at m Hm
      set Hs := H.essSurj.mem_essImage c.pt
      set x := Hs.choose
      set σ : F.obj x ≅ c.pt := Hs.choose_spec.some
      have E := Hc.uniq s (m ≫ σ.hom)
      rw [<- E]; simp; clear E
      intro j; simp
      rw [<- Hm]; simp [mkCone]
      have E := F.map_surjective (σ.hom ≫ c.π.app j)
      set g := E.choose
      rw [E.choose_spec]
  }