HasExp.lean

import Mathlib
import Mathlib.CategoryTheory.Limits.Shapes.Terminal
import Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
import Mathlib.CategoryTheory.Limits.Shapes.Products





open CategoryTheory
open Limits


noncomputable def prod.functor' [Category 𝓒] [HasBinaryProducts 𝓒] (A : 𝓒) : 𝓒 ⥤ 𝓒 where
  obj C := C ⨯ A
  map {C C'} f := prod.map f (𝟙 A)
  map_id C := by simp
  map_comp {C₁ C₂ C₃} f g := by simp

class HasExp 𝓒 [Category 𝓒] extends HasBinaryProducts 𝓒  where
  has_terminal : HasTerminal 𝓒
  exp (A : 𝓒) : 𝓒 ⥤ 𝓒
  adj A : (prod.functor' A) ⊣ exp A



instance HasExp.hasTerminal [Category 𝓒] [P : HasExp 𝓒] : HasTerminal 𝓒 := P.has_terminal
noncomputable def HasExp.unit [Category 𝓒] [P : HasExp 𝓒]  := terminal 𝓒

instance HasExp.Pow [Category 𝓒] [P : HasExp 𝓒] : Pow 𝓒 𝓒 := ⟨λ C A => (exp A).obj C⟩

noncomputable def HasExp.ev [Category 𝓒] [P : HasExp 𝓒] (A : 𝓒) :
  exp A ⋙ prod.functor' A ⟶ 𝟭 𝓒
:= (P.adj A).counit


noncomputable def HasExp.eval [Category 𝓒] [P : HasExp 𝓒] (A C : 𝓒) :
  C ^A ⨯ A ⟶ C
:= (ev A).app C

noncomputable def HasExp.curry [Category 𝓒] [P : HasExp 𝓒] {A B C : 𝓒} (f : B ⨯ A ⟶ C) :
  B ⟶ C ^A
:= (P.adj A).homEquiv _ _ f

lemma HasExp.curry_spec [Category 𝓒] [P : HasExp 𝓒] {A B C : 𝓒} (f : B ⨯ A ⟶ C) :
  f = prod.map (curry f) (𝟙 A) ≫ P.eval A C
:= by
  simp [curry, eval, ev]
  rw [(adj A).homEquiv_apply]
  simp [prod.functor']
  have E := (adj A).counit.naturality f; dsimp [prod.functor'] at E
  rw [@prod.map_comp_id_assoc, E]; clear E
  have E := (adj A).left_triangle_components B; dsimp [prod.functor'] at E
  rw [<- Category.assoc, E]; simp

lemma HasExp.curry_uniq [Category 𝓒] [P : HasExp 𝓒] {A B C : 𝓒}
  (f : B ⨯ A ⟶ C) (g : B ⟶ C ^A) (Hg : f = prod.map g (𝟙 A) ≫ P.eval A C) :
  g = P.curry f
:= by
  simp [curry]
  rw [Hg, eval, ev]
  rw [(adj A).homEquiv_apply]
  simp
  have E := (adj A).unit.naturality g; dsimp [prod.functor'] at E
  slice_rhs 1 2 => rw [<- E]
  simp; clear E
  have E := (adj A).right_triangle_components C; dsimp [prod.functor'] at E
  conv => arg 2; arg 2; change (adj A).unit.app ((exp A).obj C) ≫ (exp A).map ((adj A).counit.app C); rw [E]
  conv => arg 2; arg 2; change 𝟙 (C ^ A)
  simp






noncomputable def  HasExp.uncurry [Category 𝓒] [P : HasExp 𝓒] {A B C : 𝓒} (g : B ⟶ C^A) :
  B ⨯ A ⟶ C
:= ((adj A).homEquiv _ _).invFun g

lemma HasExp.uncurry_spec [Category 𝓒] [P : HasExp 𝓒] {A B C : 𝓒} (g : B ⟶ C^A) :
  uncurry g = prod.map g (𝟙 A) ≫ P.eval A C
:= by
  rw [uncurry, eval, ev]; simp
  rw [(adj A).homEquiv_symm_apply]
  simp only [prod.functor']

lemma HasExp.uncurry_uniq  [Category 𝓒] [P : HasExp 𝓒] {A B C : 𝓒}
  (g : B ⟶ C^A) (f : B ⨯ A ⟶ C) (Hf : f = prod.map g (𝟙 A) ≫ P.eval A C) :
  f = uncurry g
:= by
  rw [Hf, uncurry, eval, ev]; simp
  rw [(adj A).homEquiv_symm_apply]
  simp only [prod.functor']

noncomputable def HasExp.curry_iso [Category 𝓒] [P : HasExp 𝓒] (A B C : 𝓒) :
  (B ⨯ A ⟶ C) ≅ (B ⟶ C ^ A)
where
  hom := P.curry
  inv := P.uncurry
  hom_inv_id := by
    ext f; simp  [curry, uncurry]
  inv_hom_id := by
    ext g; simp [curry, uncurry]




noncomputable def HasExp.unit_iso [Category 𝓒] [P : HasExp 𝓒] (A : 𝓒) :
  unit ⨯ A ≅ A
where
  hom := prod.snd
  inv := prod.lift (terminal.from A) (𝟙 A)
  hom_inv_id := by
    rw [prod.comp_lift, Category.comp_id, terminal.comp_from]
    have E : terminal.from (unit ⨯ A) = prod.fst := terminal.hom_ext _ _
    rw [E, prod.lift_fst_snd]
  inv_hom_id := by
    rw [prod.lift_snd]


instance HasExp.preservesColimits [Category 𝓒] [P : HasExp 𝓒] (A : 𝓒) :
  PreservesColimits (prod.functor' A)
:= ⟨((P.adj A).leftAdjoint_preservesColimits).preservesColimitsOfShape⟩

instance HasExp.preservesLimits [Category 𝓒] [P : HasExp 𝓒] (A : 𝓒) :
  PreservesLimits (P.exp A)
:= ⟨(P.adj A).rightAdjoint_preservesLimits.preservesLimitsOfShape⟩

noncomputable def HasExp.preservesColimitsIso [Category 𝓒] [P : HasExp 𝓒] (A : 𝓒)
  [Category J] (K : J ⥤ 𝓒) [HasColimit K] :
  (prod.functor' A).obj (colimit K) ≅ colimit (K ⋙ prod.functor' A)
:= preservesColimitIso _ _

noncomputable def HasExp.preservesLimitsIso [Category 𝓒] [P : HasExp 𝓒] (A : 𝓒)
  [Category J] (K : J ⥤ 𝓒) [HasLimit K] :
  (exp A).obj (limit K) ≅ limit (K ⋙ exp A)
:= preservesLimitIso _ _

noncomputable def HasExp.coprod_prod [Category.{0, v} 𝓒] [P : HasExp 𝓒] [H : HasBinaryCoproducts 𝓒] (A B C : 𝓒) :
  (A ⨿ B) ⨯ C ≅ (A ⨯ C) ⨿ (B ⨯ C)
:= by
  unfold coprod
  have E := preservesColimitsIso C (pair A B)
  conv at E => arg 1; simp [prod.functor']
  suffices :  pair (A ⨯ C) (B ⨯ C) = pair A B ⋙ prod.functor' C; rw [this]; exact E
  apply CategoryTheory.Functor.ext; intro i j f
  simp [prod.functor']
  rcases f with ⟨⟨E⟩⟩
  rcases i with ⟨i⟩
  rcases j with ⟨j⟩
  simp at E; subst j; simp
  intro ⟨k⟩; rcases k<;> simp [prod.functor']

noncomputable def HasExp.prod_exp [Category.{0, v} 𝓒] [P : HasExp 𝓒]  (A B C : 𝓒) :
  (A ⨯ B) ^ C ≅ (A ^ C) ⨯ (B ^ C)
:= by
  have E := preservesLimitsIso C (pair A B)
  conv => arg 2; simp [Limits.prod]
  have : pair (A ^ C) (B ^ C) = pair A B ⋙ (P.exp C) := by
    apply CategoryTheory.Functor.ext ?_ ?_
    · intro ⟨i⟩; simp; cases i<;> simp<;> rfl
    · intro i j f;
      rcases f with ⟨⟨E⟩⟩
      rcases i with ⟨i⟩
      rcases j with ⟨j⟩
      simp at E; subst j; simp
  rw [this]
  apply E

def Yoneda.iso_exp [Category 𝓐] (A A' : 𝓐) (σ : yoneda.obj A ≅ yoneda.obj A') :
  A ≅ A'
:= by
  let f := (σ.app (Opposite.op A)).hom (𝟙 A); simp at f
  let g := (σ.app (Opposite.op A')).inv (𝟙 A'); simp at g
  use f, g <;> unfold autoParam<;> simp only [f, g]
  · rw [σ.app_hom, σ.app_inv]
    have E := Yoneda.naturality σ.inv (σ.hom.app (Opposite.op A) (𝟙 A)) (𝟙 _)
    rw [E]; simp
  · rw [σ.app_inv, σ.app_hom]
    have E := Yoneda.naturality σ.hom (σ.inv.app (Opposite.op A') (𝟙 A')) (𝟙 _)
    rw [E]; simp

def Yoneda.exp_iso [Category 𝓐] (A A' : 𝓐) (σ : A ≅ A') :
  yoneda.obj A ≅ yoneda.obj A'
:= by
  apply NatIso.ofComponents ?_ ?_
  · intro X'; simp
    refine {
      hom f := f ≫ σ.hom
      inv g := g ≫ σ.inv
      hom_inv_id := by ext; simp
      inv_hom_id := by ext; simp
    }
  · intro X Y f; ext g; simp


noncomputable def HasExp.exp_exp_iso {𝓒} [Category 𝓒] [P : HasExp 𝓒] (A B C : 𝓒) :
  (C ^ A) ^ B ≅ C ^ (A ⨯ B)
:= by
  apply Yoneda.iso_exp
  apply NatIso.ofComponents ?_ ?_
  · intro X'; simp
    apply Iso.trans  (curry_iso _ _ _ ).symm
    apply Iso.trans (curry_iso _ _ _ ).symm
    apply Iso.symm
    apply Iso.trans (curry_iso _ _ _).symm
    have σ : Opposite.unop X' ⨯ A ⨯ B ≅ (Opposite.unop X' ⨯ B) ⨯ A := by
      apply Iso.trans (Limits.prod.mapIso (Iso.refl X'.unop) (Limits.prod.braiding A B))
      apply  (Limits.prod.associator _ _ _ ).symm
    refine {
      hom f := σ.inv ≫ f
      inv g := σ.hom ≫ g
      hom_inv_id := by ext; simp
      inv_hom_id := by ext; simp
    }
  · intro X Y f; ext g; simp [curry_iso, curry, uncurry]; simp at g
    rw [(adj _).homEquiv_apply, (adj _).homEquiv_apply]
    rw [(adj _).homEquiv_symm_apply, (adj _).homEquiv_symm_apply, (adj _).homEquiv_symm_apply, (adj _).homEquiv_symm_apply]
    simp
    have E := (adj (A ⨯ B)).unit.naturality f.unop; dsimp at E
    slice_rhs 1 2 => rw [E]
    set h := (adj (A ⨯ B)).unit.app (Opposite.unop Y); simp
    rw [<- (exp (A ⨯ B)).map_comp, <- (exp (A ⨯ B)).map_comp, <- (exp (A ⨯ B)).map_comp, <- (exp (A ⨯ B)).map_comp]
    rw [<- (exp (A ⨯ B)).map_comp, <- (exp (A ⨯ B)).map_comp]
    simp [prod.functor']
    set k := (exp (A ⨯ B)).map ((adj A).counit.app C)
    rw [<- Category.assoc ((exp (A ⨯ B)).map (prod.map f.unop (𝟙 (A ⨯ B)))) _ k]; congr
    rw [<- (exp _).map_comp]; congr
    simp

Topos.lean

import Mathlib

import Mathlib.CategoryTheory.Limits.Shapes.Terminal
import Mathlib.CategoryTheory.Limits.Shapes.Equalizers
import Category.SCT.chapter3_Topos.HasExp

open CategoryTheory
open Limits

class Topos 𝓒 extends Category 𝓒, HasExp 𝓒 where
  Ω : 𝓒
  truth : terminal 𝓒 ⟶ Ω
  has_pullback {A} (f : A ⟶ Ω) : HasPullback f truth
  cl {A A' : 𝓒} {f : A' ⟶ A} (Hf : Mono f) : A ⟶ Ω
  is_pullback {A A' : 𝓒} {f : A' ⟶ A} (Hf : Mono f) :
    IsPullback f (terminal.from A') (cl Hf) truth

instance Topos.hasPullback [Topos 𝓒] {A : 𝓒} (f : A ⟶ Ω ) :
  HasPullback f truth
:= has_pullback f

noncomputable def Topos.delta [Topos 𝓒] (A : 𝓒) : A ⟶ A ⨯ A := prod.lift (𝟙 A) (𝟙 A)

lemma Topos.delta_mono [Topos 𝓒] (A : 𝓒) :
  Mono (delta A)
:= by
  constructor; intro Z g h
  simp [delta]; intro E
  rw [<- prod.lift_fst g g, <- prod.lift_fst h h, E]

noncomputable def Topos.equal [Topos 𝓒] (A : 𝓒) :A ⨯ A ⟶ Ω := cl (delta_mono A)

lemma Topos.equal_is_pullback  [Topos 𝓒] (A : 𝓒) :
  IsPullback (delta A) (terminal.from (A)) (equal A) truth
:= is_pullback (delta_mono A)

noncomputable def Topos.singleton [Topos 𝓒] (A : 𝓒) :
  A ⟶ Ω ^ A
:= HasExp.curry (equal A)

instance Topos.hasEqualizers [Topos 𝓒] :
  HasEqualizers 𝓒
:= by
  refine @hasEqualizers_of_hasLimit_parallelPair 𝓒 ?_ ?_
  intro A B f g
  apply HasLimit.mk
  refine {
    cone := {
      pt := pullback (prod.lift f g ≫ equal B) truth
      π := {
        app i := by
          simp
          have E := pullback.condition (f := prod.lift f g ≫ equal B) (g := truth)
          rw [<- Category.assoc] at E
          cases i<;> simp
          · exact pullback.fst _ _
          · exact (equal_is_pullback B).lift _ _ E
        naturality {i i'} h := by
          set HB := equal_is_pullback B
          have Efg : pullback.fst (prod.lift f g ≫ equal B) truth ≫ f = pullback.fst (prod.lift f g ≫ equal B) truth ≫ g := by
            conv => arg 1; arg 2; rw [<- Limits.prod.lift_fst f g]
            conv => arg 2; arg 2; rw [<- Limits.prod.lift_snd f g]
            have E := pullback.condition (f := prod.lift f g ≫ equal B) (g := truth)
            rw [<- Category.assoc] at E
            have E' := HB.lift_fst _ _ E
            rw [<- Category.assoc, <- Category.assoc, <- E', Category.assoc, Category.assoc]
            simp [delta]
          rcases h<;> simp
          · apply HB.hom_ext
            · rw [HB.lift_fst]; simp
              apply Limits.prod.hom_ext
              · rw [prod.lift_fst]; simp [delta]
              · rw [prod.lift_snd]; simp [delta]
                rw [Efg]
            · simp
          · apply HB.hom_ext<;> simp
            apply Limits.prod.hom_ext
            · rw [prod.lift_fst]; simp [delta]
              rw [Efg]
            · rw [prod.lift_snd]; simp [delta]
      }
    }
    isLimit := {
      lift s := by
        simp
        change Fork f g at s
        apply pullback.lift s.ι (terminal.from s.pt) ?_
        rw [<- Category.assoc, prod.comp_lift]
        have HB := equal_is_pullback B
        have Hw := HB.w
        have Hw' : s.ι ≫ f ≫ delta B ≫ equal B = s.ι ≫ f ≫ terminal.from B ≫ truth := by rw [Hw]
        conv at Hw' => arg 2; rw [<- Category.assoc, <- Category.assoc, terminal.comp_from]; simp
        rw [<- Hw']
        suffices : prod.lift (s.ι ≫ f) (s.ι ≫ g) = s.ι ≫ f ≫ delta B; rw [this]; simp
        apply Limits.prod.hom_ext
        · rw [prod.lift_fst]; simp [delta]
        · rw [prod.lift_snd, <- s.condition]; simp [delta]
      fac s j := by
        simp; cases j<;> simp
        set HB := equal_is_pullback B
        change Fork f g at s
        apply HB.hom_ext<;> simp
        apply Limits.prod.hom_ext
        · rw [prod.lift_fst]; simp [delta]
        · rw [prod.lift_snd]; simp [delta]
          rw [s.condition]
      uniq s m Hm := by
        simp at m Hm; simp
        change Fork f g at s
        apply pullback.hom_ext
        · rw [pullback.lift_fst]
          exact Hm WalkingParallelPair.zero
        · rw [pullback.lift_snd]
          apply terminal.hom_ext
    }
  }

#check hasPullbacks_of_hasBinaryProducts_of_hasEqualizers
example [Category 𝓒] [H1 : HasBinaryProducts 𝓒] [H2 : HasEqualizers 𝓒] :
  HasPullbacks 𝓒
:= by
  apply @hasPullbacks_of_hasLimit_cospan 𝓒 inferInstance ?_
  intro X Y Z f g
  let E := equalizer (prod.fst ≫ f) (prod.snd ≫ g)
  let h : E ⟶ X ⨯ Y :=  equalizer.ι (prod.fst ≫ f) (prod.snd ≫ g)
  have Ep : (equalizer.ι (prod.fst ≫ f) (prod.snd ≫ g) ≫ prod.fst) ≫ f = (equalizer.ι (prod.fst ≫ f) (prod.snd ≫ g) ≫ prod.snd) ≫ g := by simp; rw [equalizer.condition (prod.fst ≫ f) (prod.snd ≫ g)]
  constructor; constructor
  use PullbackCone.mk _ _ Ep
  refine {
    lift s := by
      simp
      change PullbackCone f g at s
      apply equalizer.lift (prod.lift s.fst s.snd)
      rw [<- Category.assoc, <- Category.assoc, prod.lift_fst, prod.lift_snd, s.condition]
    fac s j := by
      rcases j with _ | j<;> simp
      cases j<;> simp
    uniq s m Hm := by
      simp at m Hm; simp
      change PullbackCone f g at s
      apply equalizer.hom_ext
      apply Limits.prod.hom_ext<;> simp
      · exact Hm WalkingCospan.left
      · exact Hm WalkingCospan.right
  }

instance Topos.hasPullbacks [Topos 𝓒] :
  HasPullbacks 𝓒
:= by
  apply hasPullbacks_of_hasBinaryProducts_of_hasEqualizers

lemma Topos.singleton_mono [Topos 𝓒] (A : 𝓒) :
  Mono (singleton A)
:= by
  constructor; intro X f g E

  have EA : equal A = prod.map (singleton A) (𝟙 A) ≫ HasExp.eval A Ω := HasExp.curry_spec (equal A)

  have Efg : prod.map f (𝟙 A) ≫ equal A = prod.map g (𝟙 A) ≫ equal A := by
    have Eg := HasExp.uncurry_spec (f ≫ singleton A)
    have Ef := HasExp.uncurry_spec (g ≫ singleton A)
    rw [<- Category.id_comp (𝟙 A), <- prod.map_map, Category.assoc, <- EA] at Eg Ef
    rw [<- Eg, <- Ef, E]

  have Hf : IsPullback (prod.lift f (𝟙 X) ) f (prod.map (𝟙 _) f) (delta A) := by
    refine IsPullback.of_isLimit' ?_ ?_
    · constructor; unfold autoParam
      apply Limits.prod.hom_ext<;> simp [delta]
    · refine {
        lift s := PullbackCone.fst s ≫ prod.snd
        fac s j := by
          change PullbackCone _ _ at s
          have E1 : (s.fst ≫ prod.map (𝟙 A) f) ≫ prod.fst = (s.snd ≫ delta A) ≫ prod.fst := by rw [s.condition]
          have E2 : (s.fst ≫ prod.map (𝟙 A) f) ≫ prod.snd = (s.snd ≫ delta A) ≫ prod.snd := by rw [s.condition]
          simp at E1 E2; simp [delta] at E1 E2
          simp [CommSq.cone]
          rcases j with _ | j; simp
          · apply Limits.prod.hom_ext<;> simp; rw [E1, E2]
          · cases j<;> simp
            · apply Limits.prod.hom_ext<;> simp; rw [E1, E2]
            · rw [E2]
        uniq s m Hm := by
          simp [CommSq.cone] at m Hm
          change PullbackCone _ _ at s
          have El := Hm WalkingCospan.left
          simp at El
          rw [<- El, prod.lift_snd (m ≫ f) m]
      }

  have Hg : IsPullback (prod.lift g (𝟙 X) ) g (prod.map (𝟙 _) g) (delta A) := by
    refine IsPullback.of_isLimit' ?_ ?_
    · constructor; unfold autoParam
      apply Limits.prod.hom_ext<;> simp [delta]
    · refine {
        lift s := PullbackCone.fst s ≫ prod.snd
        fac s j := by
          change PullbackCone _ _ at s
          have E1 : (s.fst ≫ prod.map (𝟙 A) g) ≫ prod.fst = (s.snd ≫ delta A) ≫ prod.fst := by rw [s.condition]
          have E2 : (s.fst ≫ prod.map (𝟙 A) g) ≫ prod.snd = (s.snd ≫ delta A) ≫ prod.snd := by rw [s.condition]
          simp at E1 E2; simp [delta] at E1 E2
          simp [CommSq.cone]
          rcases j with _ | j; simp
          · apply Limits.prod.hom_ext<;> simp; rw [E1, E2]
          · cases j<;> simp
            · apply Limits.prod.hom_ext<;> simp; rw [E1, E2]
            · rw [E2]
        uniq s m Hm := by
          simp [CommSq.cone] at m Hm
          change PullbackCone _ _ at s
          have El := Hm WalkingCospan.left
          simp at El
          rw [<- El, prod.lift_snd (m ≫ g) m]
      }

  have HA := equal_is_pullback A
  have HCg := CategoryTheory.Limits.pasteHorizIsPullback (t₁ := Hg.cone) (t₂ := HA.cone) rfl HA.isLimit Hg.isLimit
  set Cf := HA.cone.pasteHoriz Hf.cone rfl
  set Cg := HA.cone.pasteHoriz Hg.cone rfl
  have HCg' := IsPullback.of_isLimit HCg; simp [Cg] at HCg'

  let Cg' : PullbackCone (prod.map (𝟙 A) g ≫ equal A) truth := by
    apply PullbackCone.mk Cf.fst Cf.snd  _
    simp [Cf]; rw [ <- Category.assoc, terminal.comp_from f]
    conv => arg 1; arg 2; rw [EA]
    simp; rw [E, Category.id_comp g]
    nth_rw 2 [<- Category.comp_id g]
    rw [<- prod.lift_map, Category.assoc, <- EA]
    have := Cg.condition; simp [Cg] at this
    rw [Category.id_comp g] at this
    rw [this, <- Category.assoc, terminal.comp_from g]

  have E := HCg'.lift_fst _ _ Cg'.condition
  conv at E => arg 2; simp [Cg', Cf]
  have E1 := congrArg (fun h => h ≫ Limits.prod.snd) E
  have E2 := congrArg (fun h => h ≫ Limits.prod.fst) E
  simp at E1 E2
  have : _ ≫ 𝟙 X = _ := Category.comp_id (HCg'.lift Cg'.fst Cg'.snd Cg'.condition)
  rw [this] at E1
  rw [<- E2, E1, Category.id_comp g]