GAFT.lean

import Mathlib.tactic
import Mathlib.CategoryTheory.Limits.HasLimits
import Mathlib.CategoryTheory.Limits.Shapes.Terminal
import Mathlib.CategoryTheory.Limits.Shapes.Equalizers
import Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
import Mathlib.CategoryTheory.Limits.Creates
import Mathlib.CategoryTheory.Limits.HasLimits

open CategoryTheory
open Limits

noncomputable example [Category X] [Category A] [Category J]
  (F : X ⥤ A) (G : A ⥤ X) (φ : F ⊣ G)
  (T : J ⥤ A) (HT : HasLimit T) :
  LimitCone (T ⋙ G)
:= by
  let mkCone : Cone (T ⋙ G) → Cone T := λ s => by
    have σ := φ.homEquiv s.pt (limit T)
    refine {
      pt := F.obj s.pt
      π := {
        app j := (φ.homEquiv _ _).invFun (s.π.app j)
        naturality {j j'} f := by
          simp
          rw [φ.homEquiv_symm_apply, φ.homEquiv_symm_apply]; simp
          have E := φ.counit.naturality (T.map f)
          conv at E => arg 2; simp
          rw [<- E, Functor.comp_map, <- Category.assoc, <- F.map_comp, <- Functor.comp_map]
          have E' := s.π.naturality f
          rw [<- E']; simp
      }
    }
  refine {
    cone := {
      pt := G.obj (limit T)
      π := {
        app j := G.map (limit.π T j)
        naturality {j j'} f := by
          simp
          rw [<- G.map_comp, limit.w T f]
      }
    }
    isLimit := {
      lift s := (φ.homEquiv s.pt (limit T)) (limit.lift T (mkCone s))
      fac s j := by
        simp
        rw [φ.homEquiv_apply]; simp
        rw [<- G.map_comp, limit.lift_π]
        simp [mkCone]
        rw [φ.homEquiv_symm_apply]
        have E := φ.unit.naturality (s.π.app j)
        conv at E => arg 2; arg 1; simp
        rw [G.map_comp, <- Category.assoc, <- Functor.comp_map, <- E]; clear E
        rw [Functor.id_map, Category.assoc]
        have E := φ.right_triangle_components (T.obj j)
        conv => arg 1; arg 2; arg 1; simp
        rw [E]; simp
      uniq s m Hm := by
        simp at m Hm
        rw [φ.homEquiv_apply]
        have E := (limit.isLimit T).uniq (mkCone s) ((φ.homEquiv _ _).invFun m)
        simp at E
        rw [<- E, φ.homEquiv_symm_apply]; clear E
        rw [G.map_comp]
        have E := φ.unit.naturality m
        rw [<- Functor.comp_map, <- Category.assoc, <- E]; clear E
        have E := φ.right_triangle_components (limit T)
        rw [Category.assoc, E]; simp; clear E
        intro j
        simp [mkCone]
        rw [φ.homEquiv_symm_apply, φ.homEquiv_symm_apply]
        simp
        have E := φ.counit.naturality (limit.π T j)
        conv at E => arg 2; simp
        rw [<- E, Functor.comp_map, <- Category.assoc, <- F.map_comp, Hm j]
    }
  }

structure IsWeaklyInit [Category 𝓒] (S : Set 𝓒) where
  obj (c : 𝓒) : S
  hom c : (obj c).val ⟶ c

structure HasWeaklyInit (𝓒) [Category 𝓒] where
  inits : Set 𝓒
  isWeaklyInit : IsWeaklyInit inits

def HasWeaklyInit.obj [Category 𝓒] (S : HasWeaklyInit 𝓒) (c : 𝓒) : 𝓒 :=
  S.isWeaklyInit.obj c

def HasWeaklyInit.hom [Category 𝓒] (S : HasWeaklyInit 𝓒) (c : 𝓒) : S.obj c ⟶ c :=
  S.isWeaklyInit.hom c

lemma limit_π_Mono [Category 𝓐] [Category I] {D : I ⥤ 𝓐} [HasLimit D]
  {a : 𝓐} (f g : a ⟶ limit D) (H : ∀ i : I, f ≫ limit.π D i = g ≫ limit.π D i) :
  f = g
:= by
  let c : Cone D := {
    pt := a
    π := {
      app j := f ≫ limit.π D j
      naturality {j j'} h := by simp
    }
  }
  have EG := limit.lift_π c
  rw [(limit.isLimit D).uniq c g, (limit.isLimit D).uniq c f]
  all_goals (intro i; simp [c])
  rw [H i]

lemma limit_π_Mono' [Category 𝓐] [Category I] {D : I ⥤ 𝓐} (c : LimitCone D)
  {a : 𝓐} (f g : a ⟶ c.cone.pt) (H : ∀ i : I, f ≫ c.cone.π.app i = g ≫ c.cone.π.app i) :
  f = g
:= by
  let c' : Cone D := {
    pt := a
    π := {
      app j := f ≫ c.cone.π.app j
      naturality {j j'} h := by simp
    }
  }
  have EG := c.isLimit.fac c' --limit.lift_π c
  rw [(c.isLimit).uniq c' g, (c.isLimit).uniq c' f]
  all_goals (intro i; simp [c'])
  rw [H i]

lemma HasWeaklyInit.HasInitial [SmallCategory.{u} 𝓒] [HasLimits 𝓒] (S : HasWeaklyInit 𝓒) :
  HasInitial 𝓒
:= by
  let P : ObjectProperty 𝓒 := S.inits
  apply IsInitial.hasInitial (X := limit P.ι)
  suffices H : (Y : 𝓒) → Unique ((limit P.ι) ⟶ Y)
  apply IsInitial.ofUnique
  intro C
  set j : P.FullSubcategory := ⟨S.obj C, (S.isWeaklyInit.obj C).property⟩
  refine {
    default := limit.π P.ι j ≫ S.hom C
    uniq := by
      intro f; simp
      set g := limit.π P.ι j ≫ S.hom C
      set h := S.hom (equalizer f g) ≫ equalizer.ι f g
      let c : Cone P.ι := {
        pt := S.obj (equalizer f g)
        π := {
          app i := h ≫ limit.π P.ι i
          naturality {i i'} k := by
            simp
            rw [<- limit.w P.ι k]; simp
        }
      }
      set i : P.FullSubcategory := ⟨S.obj (equalizer f g), (S.isWeaklyInit.obj (equalizer f g)).property⟩
      have E : limit.π P.ι i ≫ h = 𝟙 _ := by
        simp [h]
        apply limit_π_Mono (D := P.ι)
        intro k; simp
        let l : i ⟶ k := c.π.app k; simp [c] at l
        have El := limit.w P.ι l
        simp [l, c, h] at El
        rw [El]
      rw [<- Category.id_comp f, <- Category.id_comp g, <- E]
      simp [h]; rw [equalizer.condition f g]
  }

def StructuredArrow.proj  [Category 𝓐] [Category 𝓑] (A : 𝓐) (G : 𝓑 ⥤ 𝓐)  :
  StructuredArrow A G ⥤ 𝓑
:= {
  obj f := f.right
  map {f f'} F := F.right
  map_id f := by simp
  map_comp {f f' f''} F G := by simp
}

noncomputable def StructuredArrow.proj_CreatesLimits [Category.{u, v1} 𝓐] [Category.{u, v2} 𝓑] (G : 𝓑 ⥤ 𝓐) (A : 𝓐) [HG : PreservesLimits G] :
  CreatesLimits (StructuredArrow.proj A G)
:= by
  refine {
    CreatesLimitsOfShape {J HJ} := {
        CreatesLimit {K} := {
          lifts c Hc := by
            have H := (((HG.preservesLimitsOfShape (J := J)).preservesLimit (K := K ⋙ StructuredArrow.proj A G)).preserves Hc).some
            let c' : Cone ((K ⋙ StructuredArrow.proj A G) ⋙ G) := {
              pt := A
              π := {
                app j := (K.obj j).hom
                naturality {j j'} f := by simp [StructuredArrow.proj]
              }
            }
            refine {
              liftedCone := {
                pt := {
                  left := ⟨PUnit.unit⟩
                  right := c.pt
                  hom := H.lift c'
                }
                π := {
                  app j := {
                    left := 𝟙 _
                    right := c.π.app j
                    w := by
                      simp
                      have E := H.fac c' j; simp at E
                      rw [E]
                  }
                  naturality {j j'} f := by
                    simp
                    have E := c.π.naturality f; simp [StructuredArrow.proj] at E
                    rw [E]
                }
              }
              validLift := by
                simp [StructuredArrow.proj]
                refine {
                  hom := {
                    hom := 𝟙 c.pt
                    w j := by simp
                  }
                  inv := {
                    hom := 𝟙 c.pt
                    w j := by simp
                  }
                  hom_inv_id := by simp; ext; simp
                  inv_hom_id := by simp; ext; simp
                }
            }

          reflects := by
            intro c Hc; constructor
            have H := (((HG.preservesLimitsOfShape (J := J)).preservesLimit (K := K ⋙ StructuredArrow.proj A G)).preserves Hc).some
            refine {
              lift s := by
                set s' := (((StructuredArrow.proj A G).mapCone s))
                refine {
                  left := by
                    have E : s.pt.left = c.pt.left := by ext
                    rw [E]; exact 𝟙 _
                  right := Hc.lift s'
                  w := by
                    simp
                    let D := (K ⋙ StructuredArrow.proj A G)
                    apply limit_π_Mono' ⟨(G.mapCone ((StructuredArrow.proj A G).mapCone c)), H⟩
                    intro i; simp [StructuredArrow.proj]
                    rw [<- G.map_comp]
                    have E := Hc.fac s' i; simp [StructuredArrow.proj] at E
                    rw [E]; simp [s', StructuredArrow.proj]
                }
              fac s j := by
                simp
                set s' := (((StructuredArrow.proj A G).mapCone s))
                have E := Hc.fac s' j; simp [StructuredArrow.proj] at E
                rw [E]; simp [s', StructuredArrow.proj]
              uniq s m Hm := by
                simp
                set s' := (((StructuredArrow.proj A G).mapCone s))
                rw [Hc.uniq s' m.right]
                intro j; simp [StructuredArrow.proj, s']
                rw [<- Hm j]; simp
            }
        }
      }
  }

noncomputable def PreserversLimits.StructuredArrow_HasLimits
  [Category.{u, v1} 𝓐] [Category.{u, v2} 𝓑] (G : 𝓑 ⥤ 𝓐) (A : 𝓐)
  [HG : PreservesLimits G] [H𝓑 : HasLimits 𝓑] :
  HasLimits (StructuredArrow A G)
:= by
  constructor; unfold autoParam
  intro J HJ
  constructor; unfold autoParam
  intro K
  have C := ((StructuredArrow.proj_CreatesLimits G A).CreatesLimitsOfShape (J := J)).CreatesLimit (K := K)
  have H := (H𝓑.has_limits_of_shape (J := J)).has_limit (F := K ⋙ StructuredArrow.proj A G)
  constructor; constructor
  have H' := H.exists_limit.some
  rcases H' with ⟨c', Hc'⟩
  have ⟨c, Hc⟩ := C.lifts c' Hc'
  have H2 := C.toReflectsLimit
  rcases H2 with ⟨H2⟩
  use c
  suffices : IsLimit ((StructuredArrow.proj A G).mapCone c)
  exact (H2 this).some
  exact Hc'.ofIsoLimit Hc.symm

lemma initial.to_hcongr [Category 𝓐] [HasInitial 𝓐] {A A' : 𝓐} (H : A = A') :
  HEq (initial.to A) (initial.to A')
:= by
  subst A'; rfl

lemma StructuredArrow.right_hcongr [Category 𝓐] [Category 𝓑]
  {A : 𝓐} {G : 𝓑 ⥤ 𝓐} {a b c d : StructuredArrow A G}
  {f : a ⟶ b} {g : c ⟶ d} (Hd : a = c) (Hc : b = d) (H : HEq f g) :
  HEq f.right g.right
:= by
  subst c d; cases H; rfl

lemma HasInitial.IsrightAdjoint [Category 𝓑] [Category 𝓐] (G : 𝓑 ⥤ 𝓐)
  (H : ∀ A : 𝓐, HasInitial (StructuredArrow A G )) :
  G.IsRightAdjoint
:= by
  constructor
  refine ⟨?_, ?_⟩
  · refine {
      obj A := (⊥_ StructuredArrow A G).right
      map {A A'} f := (initial.to (StructuredArrow.mk (f ≫ (⊥_ StructuredArrow A' G).hom))).right
      map_id A := by
        rw [Category.id_comp]
        apply eq_of_heq
        have E := (StructuredArrow.eq_mk (⊥_ StructuredArrow A G)).symm
        have E' := initial.to_hcongr E
        apply HEq.trans
        · apply StructuredArrow.right_hcongr _ _ E'; simp
          rw [<- StructuredArrow.eq_mk (⊥_ StructuredArrow A G)]
        · simp
          rw [initial.hom_ext  ((initial.to (⊥_ StructuredArrow A G))) (𝟙 _)]
          simp
      map_comp {A₁ A₂ A₃} f g := by
        set F := (StructuredArrow.mk ((f ≫ g) ≫ (⊥_ StructuredArrow A₃ G).hom))
        set L := (StructuredArrow.mk (f ≫ (⊥_ StructuredArrow A₂ G).hom))
        set R := (StructuredArrow.mk (g ≫ (⊥_ StructuredArrow A₃ G).hom))
        change (initial.to F).right = (initial.to L).right ≫ (initial.to R).right
        let LF : L ⟶ F := {
          left := 𝟙 _
          right := (initial.to R).right
          w := by simp [F, L, R]
        }
        have E := initial.hom_ext (initial.to F) (initial.to L ≫ LF)
        have E' := StructuredArrow.comp_right (initial.to L) LF
        rw [E, E']
    }
  · constructor
    refine {
      unit := {
        app A := (⊥_ StructuredArrow A G).hom
        naturality {A A'} f := by simp
      }
      counit := {
        app B := (initial.to (StructuredArrow.mk (𝟙 G.obj B))).right
        naturality {B B'} f := by
          simp
          set L := (StructuredArrow.mk (G.map f ≫ (⊥_ StructuredArrow (G.obj B') G).hom))
          set R := (StructuredArrow.mk (𝟙 (G.obj B')))
          set F := (StructuredArrow.mk (𝟙 (G.obj B)))
          change (initial.to L).right ≫ (initial.to R).right = (initial.to F).right ≫ f
          let Gf := StructuredArrow.mk (G.map f)
          let K : ⊥_ StructuredArrow (G.obj B) G ⟶ Gf := {
            left := 𝟙 _
            right := (initial.to F).right ≫ f
            w := by simp [Gf, F]
          }
          let LGf : L ⟶ Gf := {
            left := 𝟙 _
            right := (initial.to R).right
            w := by simp [Gf, L, R]
          }
          have E := initial.hom_ext (initial.to L ≫ LGf) K
          have EK : K.right = (initial.to F).right ≫ f := by simp [K]
          have E' := StructuredArrow.comp_right (initial.to L) LGf
          rw [<- EK, <- E, E']
      }
      left_triangle_components := by
        intro A; simp
        set L := (StructuredArrow.mk ((⊥_ StructuredArrow A G).hom ≫ (⊥_ StructuredArrow (G.obj (⊥_ StructuredArrow A G).right) G).hom))
        set R := (StructuredArrow.mk (𝟙 (G.obj (⊥_ StructuredArrow A G).right)))
        change (initial.to L).right ≫ (initial.to R).right = _
        have E0 : CommaMorphism.right (𝟙 (⊥_ StructuredArrow A G))= 𝟙 (⊥_ StructuredArrow A G).right := by simp
        rw [<- E0]; clear E0
        let R' : L ⟶ ⊥_ StructuredArrow A G := {
          left := 𝟙 _
          right := (initial.to R).right
          w := by simp [L, R]
        }
        have E := initial.hom_ext (initial.to L ≫ R') (𝟙 (⊥_ StructuredArrow A G))
        have E' := StructuredArrow.comp_right (initial.to L) R'
        rw [<- E, E']
      right_triangle_components := by intro B; simp
    }

example [Category.{u, v1} 𝓐] [SmallCategory.{u} 𝓑] [H𝓑 : HasLimits 𝓑]
  (G : 𝓑 ⥤ 𝓐) (H𝓐 : ∀ A : 𝓐, HasWeaklyInit (StructuredArrow A G)) (HG : PreservesLimits G) :
  G.IsRightAdjoint
:= by
  apply HasInitial.IsrightAdjoint
  intro A
  have HA := H𝓐 A
  have := PreserversLimits.StructuredArrow_HasLimits G A
  apply HasWeaklyInit.HasInitial HA