From c5420fa7860be2e51b014e465e403b15fe4cfb25 Mon Sep 17 00:00:00 2001 From: jlh18 Date: Fri, 12 Dec 2025 09:28:32 -0500 Subject: [PATCH] feat: Structured model --- HoTTLean.lean | 1 + HoTTLean/ForMathlib.lean | 32 - .../CategoryTheory/Adjunction/Basic.lean | 49 + .../Adjunction/PartialAdjoint.lean | 66 + .../Bicategory/Grothendieck.lean | 20 +- HoTTLean/ForMathlib/CategoryTheory/Clan.lean | 532 +++++++ .../CategoryTheory/ClovenIsofibration.lean | 800 ++++++++++ .../Comma/Over/Pushforward.lean | 73 + .../CategoryTheory/Comma/Presheaf/Basic.lean | 203 +++ .../CategoryTheory/Functor/FullyFaithful.lean | 16 + .../Limits/Shapes/Pullback/CommSq.lean | 16 + .../MorphismProperty/Limits.lean | 82 + .../MorphismProperty/OverAdjunction.lean | 495 ++++++ .../ForMathlib/CategoryTheory/NatTrans.lean | 29 + .../ForMathlib/CategoryTheory/Polynomial.lean | 1340 +++++++++++++++++ .../ForMathlib/CategoryTheory/Yoneda.lean | 71 + .../Model/Structured/StructuredUniverse.lean | 923 ++++++++++++ lake-manifest.json | 10 +- lakefile.lean | 2 +- 19 files changed, 4718 insertions(+), 42 deletions(-) create mode 100644 HoTTLean/ForMathlib/CategoryTheory/Adjunction/Basic.lean create mode 100644 HoTTLean/ForMathlib/CategoryTheory/Adjunction/PartialAdjoint.lean create mode 100644 HoTTLean/ForMathlib/CategoryTheory/Clan.lean create mode 100644 HoTTLean/ForMathlib/CategoryTheory/ClovenIsofibration.lean create mode 100644 HoTTLean/ForMathlib/CategoryTheory/Comma/Over/Pushforward.lean create mode 100644 HoTTLean/ForMathlib/CategoryTheory/Comma/Presheaf/Basic.lean create mode 100644 HoTTLean/ForMathlib/CategoryTheory/Functor/FullyFaithful.lean create mode 100644 HoTTLean/ForMathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean create mode 100644 HoTTLean/ForMathlib/CategoryTheory/MorphismProperty/Limits.lean create mode 100644 HoTTLean/ForMathlib/CategoryTheory/MorphismProperty/OverAdjunction.lean create mode 100644 HoTTLean/ForMathlib/CategoryTheory/Polynomial.lean create mode 100644 HoTTLean/Model/Structured/StructuredUniverse.lean diff --git a/HoTTLean.lean b/HoTTLean.lean index 2c6e609b..3d952541 100644 --- a/HoTTLean.lean +++ b/HoTTLean.lean @@ -2,4 +2,5 @@ import HoTTLean.Groupoids.Sigma import HoTTLean.Groupoids.Pi import HoTTLean.Groupoids.Id import HoTTLean.Model.Unstructured.Interpretation +import HoTTLean.Model.Structured.StructuredUniverse import HoTTLean.Frontend.Commands diff --git a/HoTTLean/ForMathlib.lean b/HoTTLean/ForMathlib.lean index 0d1cd8c9..d940f90b 100644 --- a/HoTTLean/ForMathlib.lean +++ b/HoTTLean/ForMathlib.lean @@ -538,30 +538,6 @@ variable {C : Type u₁} [SmallCategory C] {F G : Cᵒᵖ ⥤ Type u₁} (naturality : ∀ {X Y : C} (f : X ⟶ Y) (α : yoneda.obj Y ⟶ F), app (yoneda.map f ≫ α) = yoneda.map f ≫ app α) -variable (F) in -/-- - A presheaf `F` on a small category `C` is isomorphic to - the hom-presheaf `Hom(y(•),F)`. --/ -def yonedaIso : yoneda.op ⋙ yoneda.obj F ≅ F := - NatIso.ofComponents (fun _ => Equiv.toIso yonedaEquiv) - (fun f => by ext : 1; dsimp; rw [yonedaEquiv_naturality']) - -def yonedaIsoMap : yoneda.op ⋙ yoneda.obj F ⟶ yoneda.op ⋙ yoneda.obj G where - app _ := app - naturality _ _ _ := by ext : 1; apply naturality - -/-- Build natural transformations between presheaves on a small category - by defining their action when precomposing by a morphism with - representable domain -/ -def NatTrans.yonedaMk : F ⟶ G := - (yonedaIso F).inv ≫ yonedaIsoMap app naturality ≫ (yonedaIso G).hom - -theorem NatTrans.yonedaMk_app {X : C} (α : yoneda.obj X ⟶ F) : - α ≫ yonedaMk app naturality = app α := by - rw [← yonedaEquiv.apply_eq_iff_eq, yonedaEquiv_comp] - simp [yonedaMk, yonedaIso, yonedaIsoMap] - namespace Functor theorem precomp_heq_of_heq_id {A B : Type u} {C : Type*} [Category.{v} A] [Category.{v} B] [Category C] @@ -624,14 +600,6 @@ lemma Discrete.functor_eq {X C : Type*} [Category C] {F : Discrete X ⥤ C} : cases h simp -lemma Discrete.functor_ext {X C : Type*} [Category C] (F G : Discrete X ⥤ C) - (h : ∀ x : X, F.obj ⟨x⟩ = G.obj ⟨x⟩) : - F = G := - calc F - _ = Discrete.functor (fun x => F.obj ⟨x⟩) := Discrete.functor_eq - _ = Discrete.functor (fun x => G.obj ⟨x⟩) := Discrete.functor_ext' h - _ = G := Discrete.functor_eq.symm - lemma Discrete.hext {X Y : Type u} (a : Discrete X) (b : Discrete Y) (hXY : X ≍ Y) (hab : a.1 ≍ b.1) : a ≍ b := by aesop_cat diff --git a/HoTTLean/ForMathlib/CategoryTheory/Adjunction/Basic.lean b/HoTTLean/ForMathlib/CategoryTheory/Adjunction/Basic.lean new file mode 100644 index 00000000..1e458884 --- /dev/null +++ b/HoTTLean/ForMathlib/CategoryTheory/Adjunction/Basic.lean @@ -0,0 +1,49 @@ +import Mathlib.CategoryTheory.Adjunction.Basic + +namespace CategoryTheory + +open CategoryTheory.Functor NatIso Category + +-- declare the `v`'s first; see `CategoryTheory.Category` for an explanation +universe v₁ v₂ v₃ u₁ u₂ u₃ +variable {C : Type u₁} [Category.{v₁} C] {D : Type u₂} + +/-- The natural hom-set isomorphism `C(F(-),⋆) ≅ D(-,G(⋆))` given by an adjunction. -/ +def Adjunction.homIso [Category.{v₁} D] {F : C ⥤ D} {G : D ⥤ C} (adj : F ⊣ G) : + yoneda ⋙ (Functor.whiskeringLeft _ _ _).obj (F.op) ≅ G ⋙ yoneda := + NatIso.ofComponents + (fun X => (adj.representableBy X).toIso.symm) + (fun {X Y} f => by ext; simp [Functor.RepresentableBy.toIso, Functor.representableByEquiv, + adj.homEquiv_naturality_right]) + +namespace Equivalence + +variable [Category.{v₂} D] {e : C ≌ D} + +def isoCompInverse {J : Type*} [Category J] {X : J ⥤ C} {Y : J ⥤ D} (α : X ⋙ e.functor ≅ Y) : + X ≅ Y ⋙ e.inverse := + calc X + _ ≅ X ⋙ 𝟭 _ := X.rightUnitor.symm + _ ≅ X ⋙ e.functor ⋙ e.inverse := Functor.isoWhiskerLeft X e.unitIso + _ ≅ (X ⋙ e.functor) ⋙ e.inverse := Functor.associator .. + _ ≅ Y ⋙ e.inverse := Functor.isoWhiskerRight α e.inverse + +@[simp] +lemma isoCompInverse_hom_app {J : Type*} [Category J] {X : J ⥤ C} {Y : J ⥤ D} + (α : X ⋙ e.functor ≅ Y) (A : J) : + (isoCompInverse α).hom.app A = e.unitIso.hom.app (X.obj A) ≫ e.inverse.map (α.hom.app A) := by + simp [isoCompInverse, Trans.trans] + +@[simp] +lemma isoCompInverse_inv_app {J : Type*} [Category J] {X : J ⥤ C} {Y : J ⥤ D} + (α : X ⋙ e.functor ≅ Y) (A : J) : + (isoCompInverse α).inv.app A = e.inverse.map (α.inv.app A) ≫ e.unitIso.inv.app (X.obj A) := by + simp [isoCompInverse, Trans.trans] + +@[simps] +def compFunctorNatIsoEquiv {J : Type*} [Category J] (X : J ⥤ C) (Y : J ⥤ D) : + (X ⋙ e.functor ≅ Y) ≃ (X ≅ Y ⋙ e.inverse) where + toFun := isoCompInverse + invFun α := (e.symm.isoCompInverse α.symm).symm + left_inv := by cat_disch + right_inv := by cat_disch diff --git a/HoTTLean/ForMathlib/CategoryTheory/Adjunction/PartialAdjoint.lean b/HoTTLean/ForMathlib/CategoryTheory/Adjunction/PartialAdjoint.lean new file mode 100644 index 00000000..523a8882 --- /dev/null +++ b/HoTTLean/ForMathlib/CategoryTheory/Adjunction/PartialAdjoint.lean @@ -0,0 +1,66 @@ +import Mathlib.CategoryTheory.Adjunction.PartialAdjoint + + +universe v₁ v₂ u₁ u₂ + +namespace CategoryTheory + +namespace Functor + +open Category Opposite Limits + +section PartialRightAdjoint + +variable {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D] (F : C ⥤ D) + +structure PartialRightAdjoint (G : F.PartialRightAdjointSource ⥤ C) where + (repr : ∀ Y, (F.op ⋙ yoneda.obj Y.obj).RepresentableBy (G.obj Y)) + (repr_homEquiv : ∀ X Y (f : X ⟶ Y), (repr Y).homEquiv (G.map f) = + (repr X).homEquiv (𝟙 _) ≫ f) + +@[simps] +noncomputable def PartialRightAdjoint.partialRightAdjoint : + PartialRightAdjoint F (partialRightAdjoint F) where + repr _ := Functor.representableBy _ + repr_homEquiv _ _ _ := by + simp only [partialRightAdjoint_obj, comp_obj, op_obj, yoneda_obj_obj, partialRightAdjoint_map, + partialRightAdjointMap, partialRightAdjointHomEquiv] + erw [Equiv.apply_symm_apply] + +@[simps] +noncomputable def rightAdjoint.partialRightAdjoint (L : C ⥤ D) [IsLeftAdjoint L] : + PartialRightAdjoint L (ObjectProperty.ι _ ⋙ rightAdjoint L) where + repr Y := Adjunction.representableBy (Adjunction.ofIsLeftAdjoint L) _ + repr_homEquiv a b c := by + simp [Equiv.symm_apply_eq, Adjunction.homEquiv_naturality_right] + +lemma PartialRightAdjoint.repr_homEquiv_comp {G : F.PartialRightAdjointSource ⥤ C} + (P : PartialRightAdjoint F G) {X Y Z} (f : X ⟶ Y) (a : Z ⟶ G.obj X) : + (P.repr Y).homEquiv (a ≫ G.map f) = (P.repr X).homEquiv a ≫ f := by + have := (P.repr X).homEquiv_comp a (𝟙 _) + rw [(P.repr Y).homEquiv_comp, P.repr_homEquiv] + cat_disch + +lemma PartialRightAdjoint.repr_homEquiv_symm_comp {G : F.PartialRightAdjointSource ⥤ C} + (P : PartialRightAdjoint F G) {X Y Z} (f : X ⟶ Y) (a : F.obj Z ⟶ X.obj) : + (P.repr Y).homEquiv.symm (a ≫ f) = (P.repr X).homEquiv.symm a ≫ G.map f := by + rw [Equiv.symm_apply_eq, repr_homEquiv_comp, Equiv.apply_symm_apply] + +def PartialRightAdjoint.uniqueUpToIso {G G' : F.PartialRightAdjointSource ⥤ C} + (P : PartialRightAdjoint F G) (P' : PartialRightAdjoint F G') : G ≅ G' := + NatIso.ofComponents (fun X => (P.repr _).uniqueUpToIso (P'.repr _)) + (fun {X Y} f => by + apply yoneda.map_injective + ext Z a + simp only [yoneda_obj_obj, RepresentableBy.uniqueUpToIso_hom, comp_obj, op_obj, map_comp, + FullyFaithful.map_preimage, FunctorToTypes.comp, yoneda_map_app, NatIso.ofComponents_hom_app, + Function.comp_apply] + calc (P'.repr Y).homEquiv.symm ((P.repr Y).homEquiv (a ≫ G.map f)) + _ = (P'.repr Y).homEquiv.symm ((P.repr X).homEquiv a ≫ f) := by + simpa using PartialRightAdjoint.repr_homEquiv_comp .. + _ = (P'.repr X).homEquiv.symm ((P.repr X).homEquiv a) ≫ G'.map f := by + apply repr_homEquiv_symm_comp) + +noncomputable abbrev isoPartialRightAdjoint (G : F.PartialRightAdjointSource ⥤ C) + (P : PartialRightAdjoint F G) : G ≅ partialRightAdjoint F := + PartialRightAdjoint.uniqueUpToIso _ P (PartialRightAdjoint.partialRightAdjoint _) diff --git a/HoTTLean/ForMathlib/CategoryTheory/Bicategory/Grothendieck.lean b/HoTTLean/ForMathlib/CategoryTheory/Bicategory/Grothendieck.lean index 3f256088..32b23508 100644 --- a/HoTTLean/ForMathlib/CategoryTheory/Bicategory/Grothendieck.lean +++ b/HoTTLean/ForMathlib/CategoryTheory/Bicategory/Grothendieck.lean @@ -56,12 +56,24 @@ section variable {B : Type u₁} [Bicategory B] variable (F : Pseudofunctor B Cat) {a b : B} + @[simp] lemma _root_.CategoryTheory.LocallyDiscrete.Iso.hom_inv {C : Type u₁} [Category C] (X Y : LocallyDiscrete C) (e : X ≅ Y) : e.hom.toLoc ≫ e.inv.toLoc = 𝟙 _ := LocallyDiscrete.eq_of_hom ⟨⟨by simp⟩⟩ -attribute [reassoc] StrongTrans.naturality_comp_inv_app - +-- Autogenerated by adding @[to_app (attr := reassoc)] to `StrongTrans.naturality_comp_inv` +def StrongTrans.naturality_comp_inv_app_assoc + {B : Type*} [Bicategory B] + {F G : Pseudofunctor B Cat} (α : F ⟶ G) {a b c : B} (f : a ⟶ b) (g : b ⟶ c) + (X : ↑(F.obj a)) {Z : ↑(G.obj c)} (h : (F.map (f ≫ g) ≫ α.app c).obj X ⟶ Z) : + (α.naturality (f ≫ g)).inv.app X ≫ h = + (G.mapComp f g).hom.app ((α.app a).obj X) ≫ + (α_ (α.app a) (G.map f) (G.map g)).inv.app X ≫ + (G.map g).map ((α.naturality f).inv.app X) ≫ + (α_ (F.map f) (α.app b) (G.map g)).hom.app X ≫ + (α.naturality g).inv.app ((F.map f).obj X) ≫ + (α_ (F.map f) (F.map g) (α.app c)).inv.app X ≫ (α.app c).map ((F.mapComp f g).inv.app X) ≫ h := + sorry end lemma _root_.CategoryTheory.Functor.toPseudofunctor'_map₂ {C : Type u₁} [Category.{v₁} C] (F : C ⥤ Cat) @@ -1179,7 +1191,7 @@ include hom_id in lemma functorFromCompHom_id (c : C) : functorFromCompHom fib hom G (𝟙 c) = eqToHom (by simp [Cat.id_eq_id, Functor.id_comp]) := by ext x - simp [hom_id, functorFromCompHom] + simp [hom_id, eqToHom_map, functorFromCompHom] include hom_comp in lemma functorFromCompHom_comp (c₁ c₂ c₃ : C) (f : c₁ ⟶ c₂) (g : c₂ ⟶ c₃): @@ -1188,7 +1200,7 @@ lemma functorFromCompHom_comp (c₁ c₂ c₃ : C) (f : c₁ ⟶ c₂) (g : c₂ Functor.whiskerLeft (F.map f) (functorFromCompHom fib hom G g) ≫ eqToHom (by simp[Cat.comp_eq_comp, Functor.map_comp, Functor.assoc]) := by ext - simp [functorFromCompHom, hom_comp] + simp [functorFromCompHom, hom_comp, eqToHom_map] theorem functorFrom_comp : functorFrom fib hom hom_id hom_comp ⋙ G = functorFrom (functorFromCompFib fib G) (functorFromCompHom fib hom G) diff --git a/HoTTLean/ForMathlib/CategoryTheory/Clan.lean b/HoTTLean/ForMathlib/CategoryTheory/Clan.lean new file mode 100644 index 00000000..87ba7df3 --- /dev/null +++ b/HoTTLean/ForMathlib/CategoryTheory/Clan.lean @@ -0,0 +1,532 @@ +import HoTTLean.ForMathlib.CategoryTheory.MorphismProperty.OverAdjunction +import Mathlib.CategoryTheory.Functor.TwoSquare +import HoTTLean.ForMathlib.CategoryTheory.Comma.Over.Pushforward +import HoTTLean.ForMathlib.CategoryTheory.MorphismProperty.Limits +import HoTTLean.ForMathlib.CategoryTheory.Limits.Shapes.Pullback.CommSq +import Mathlib.CategoryTheory.Limits.Constructions.Over.Basic +import HoTTLean.ForMathlib +import HoTTLean.ForMathlib.CategoryTheory.NatTrans +import Mathlib.Tactic.DepRewrite +import Poly.ForMathlib.CategoryTheory.LocallyCartesianClosed.BeckChevalley +import HoTTLean.ForMathlib.CategoryTheory.Yoneda +import Poly.ForMathlib.CategoryTheory.LocallyCartesianClosed.Presheaf +import HoTTLean.ForMathlib.CategoryTheory.Adjunction.PartialAdjoint +import HoTTLean.ForMathlib.CategoryTheory.Comma.Presheaf.Basic +import HoTTLean.ForMathlib.CategoryTheory.Functor.FullyFaithful + +universe w v u v₁ u₁ + +noncomputable section + +namespace CategoryTheory + +open Category Limits MorphismProperty + +variable {C : Type u} [Category.{v} C] {C' : Type u₁} [Category.{v₁} C'] (F : C ⥤ C') + +class Functor.PreservesMorphismProperty (R : MorphismProperty C) (R' : MorphismProperty C') where + map_mem {X Y : C} (f : X ⟶ Y) : R f → R' (F.map f) + +abbrev Functor.map_mem {R : MorphismProperty C} {R' : MorphismProperty C'} + [F.PreservesMorphismProperty R R'] {X Y : C} (f : X ⟶ Y) : R f → R' (F.map f) := + PreservesMorphismProperty.map_mem f + +class Functor.PreservesPullbacksOf (R : MorphismProperty C) where + pb {P X Y Z : C} (fst : P ⟶ X) (snd : P ⟶ Y) (f : X ⟶ Z) (g : Y ⟶ Z) : + R snd → IsPullback fst snd f g → IsPullback (F.map fst) (F.map snd) (F.map f) (F.map g) + +-- NOTE this definition should refactor NaturalModel.Universe +structure RepresentableChosenPullbacks {X Y : Psh C} (f : X ⟶ Y) where + ext {Γ : C} (A : y(Γ) ⟶ Y) : C + disp {Γ : C} (A : y(Γ) ⟶ Y) : ext A ⟶ Γ + var {Γ : C} (A : y(Γ) ⟶ Y) : y(ext A) ⟶ X + disp_pullback {Γ : C} (A : y(Γ) ⟶ Y) : + IsPullback (var A) ym(disp A) f A + +open Functor in +theorem NatTrans.isIso_of_whiskerRight_isIso {C D E : Type*} [Category C] [Category D] [Category E] + {G H : C ⥤ D} (α : G ⟶ H) (F : D ⥤ E) [IsIso (whiskerRight α F)] [F.ReflectsIsomorphisms] : + IsIso α := by + rw [NatTrans.isIso_iff_isIso_app] at * + intro + apply (config := {allowSynthFailures:= true}) Functor.ReflectsIsomorphisms.reflects F + cat_disch + +namespace MorphismProperty + +variable (R : MorphismProperty C) + +section pullback + +variable {R} [R.HasPullbacks] {X : C} + +variable (X) + +end pullback + +abbrev chosenTerminal [R.ContainsIdentities] (X) : R.Over ⊤ X := .mk ⊤ (𝟙 X) (R.id_mem _) + +def Over.pullback_obj_chosenTerminal [R.IsStableUnderBaseChange] [R.ContainsIdentities] + {X Y : C} (f : X ⟶ Y) [R.HasPullbacksAlong f] : + (Over.pullback R ⊤ f).obj (R.chosenTerminal Y) ≅ R.chosenTerminal X := + have : HasPullback (𝟙 Y) f := HasPullbacksAlong.hasPullback (𝟙 Y) (R.id_mem Y) + MorphismProperty.Over.isoMk (IsPullback.id_vert f).isoPullback.symm + +variable [R.HasPullbacks] [R.IsStableUnderBaseChange] + +@[simp] +protected abbrev Over.yoneda (X : C) : R.Over ⊤ X ⥤ CategoryTheory.Over y(X) := + Over.forget _ _ _ ⋙ CategoryTheory.Over.post yoneda + +-- @[simps] +-- protected def Over.yoneda (X : C) : R.Over ⊤ X ⥤ CategoryTheory.Over y(X) where +-- obj A := .mk ym(A.hom) +-- map {A1 A2} f := CategoryTheory.Over.homMk ym(f.left) + +-- instance (X : C) : (Over.yoneda R X).Full where +-- map_surjective {A B} f := +-- ⟨Over.homMk (yoneda.preimage f.left) (by +-- apply yoneda.map_injective; simpa using CategoryTheory.Over.w f), +-- by cat_disch⟩ + +-- instance (X : C) : (Over.yoneda R X).Faithful where +-- map_injective {A B} f f' hf := by +-- ext +-- apply yoneda.map_injective +-- exact Functor.congr_map (CategoryTheory.Over.forget _) hf + +variable (F : Psh C) + +instance : (⊤ : MorphismProperty C).HasOfPostcompProperty ⊤ where + of_postcomp := by simp + +instance (P : MorphismProperty C) {X} : P.HasPullbacksAlong (𝟙 X) where + hasPullback g hg := + have : IsPullback (𝟙 _) g g (𝟙 X) := IsPullback.of_horiz_isIso (by simp) + IsPullback.hasPullback this + +/-- `Over.pullback` commutes with composition. -/ +@[simps! hom_app_left inv_app_left] +noncomputable def Over.pullbackId (P Q : MorphismProperty C) (X) + [Q.IsMultiplicative] [P.IsStableUnderBaseChange] [Q.IsStableUnderBaseChange] + [Q.RespectsIso] : Over.pullback P Q (𝟙 X) ≅ 𝟭 _ := + NatIso.ofComponents (fun X ↦ Over.isoMk (asIso (pullback.fst X.hom (𝟙 _))) + (by simp [pullback.condition])) + +def pullbackPullbackTwoSquare {T : Type u} [Category.{v} T] {R : MorphismProperty T} + {X Y Z W : T} (h : X ⟶ Z) (f : X ⟶ Y) (g : Z ⟶ W) (k : Y ⟶ W) (sq : h ≫ g = f ≫ k) + [R.IsStableUnderBaseChangeAlong h] [R.IsStableUnderBaseChangeAlong f] + [R.IsStableUnderBaseChangeAlong g] [R.IsStableUnderBaseChangeAlong k] + [R.HasPullbacksAlong h] [R.HasPullbacksAlong f] [R.HasPullbacksAlong g] + [R.HasPullbacksAlong k] : TwoSquare (Over.pullback R ⊤ k) (Over.pullback R ⊤ g) + (Over.pullback R ⊤ f) (Over.pullback R ⊤ h) := + (Over.pullbackComp _ _).inv ≫ (Over.pullbackCongr sq).inv ≫ (Over.pullbackComp _ _).hom + +@[simp] +lemma pullbackPullbackTwoSquare_app_left {T : Type u} [Category.{v} T] {R : MorphismProperty T} + {X Y Z W : T} (h : X ⟶ Z) (f : X ⟶ Y) (g : Z ⟶ W) (k : Y ⟶ W) (sq : h ≫ g = f ≫ k) + [R.IsStableUnderBaseChangeAlong h] [R.IsStableUnderBaseChangeAlong f] + [R.IsStableUnderBaseChangeAlong g] [R.IsStableUnderBaseChangeAlong k] + [R.HasPullbacksAlong h] [R.HasPullbacksAlong f] [R.HasPullbacksAlong g] + [R.HasPullbacksAlong k] (A : R.Over ⊤ W) : + ((pullbackPullbackTwoSquare h f g k sq).app A).left = + pullback.lift (pullback.map _ _ _ _ (pullback.fst _ _) h k + (by simp [pullback.condition]) sq.symm) (pullback.snd _ _) (by cat_disch) := by + dsimp [pullbackPullbackTwoSquare] + ext <;> simp + +/-- Fixing a commutative square, +``` + Y - k → W + ∧ ∧ + f | | g + | | + X - h → Z +``` +`pullbackMapTwoSquare` is the Beck-Chevalley natural transformation for `Over.map` between +the `MorphismProperty.Over` categories, +of type `pullback f ⋙ map h ⟶ map k ⋙ pullback g`. +``` + map k + R.Over Y --------> R.Over W + | | + | | +pullback f ↗ pullback g + | | + v V + R.Over X --------> R.Over Z + map h +``` +-/ +def pullbackMapTwoSquare {T : Type u} [Category.{v} T] (R : MorphismProperty T) + [R.IsStableUnderComposition] + {X Y Z W : T} (h : X ⟶ Z) (f : X ⟶ Y) (g : Z ⟶ W) (k : Y ⟶ W) (rk : R k) (rh : R h) + [R.IsStableUnderBaseChangeAlong h] [R.IsStableUnderBaseChangeAlong f] + [R.IsStableUnderBaseChangeAlong g] [R.IsStableUnderBaseChangeAlong k] + [R.HasPullbacksAlong h] [R.HasPullbacksAlong f] [R.HasPullbacksAlong g] [R.HasPullbacksAlong k] + (sq : h ≫ g = f ≫ k) : + TwoSquare (MorphismProperty.Over.pullback R ⊤ f) (MorphismProperty.Over.map ⊤ rk) + (MorphismProperty.Over.map ⊤ rh) + (MorphismProperty.Over.pullback R ⊤ g) := + (mateEquiv (MorphismProperty.Over.mapPullbackAdj k rk trivial) + (MorphismProperty.Over.mapPullbackAdj h rh trivial)).symm <| + pullbackPullbackTwoSquare _ _ _ _ sq + +@[simp] +lemma pullbackMapTwoSquare_app_left {T : Type u} [Category.{v} T] (R : MorphismProperty T) + [R.IsStableUnderComposition] {X Y Z W : T} (h : X ⟶ Z) (f : X ⟶ Y) (g : Z ⟶ W) (k : Y ⟶ W) + (rk : R k) (rh : R h) (sq : h ≫ g = f ≫ k) + [R.IsStableUnderBaseChangeAlong h] [R.IsStableUnderBaseChangeAlong f] + [R.IsStableUnderBaseChangeAlong g] [R.IsStableUnderBaseChangeAlong k] + [R.HasPullbacksAlong h] [R.HasPullbacksAlong f] [R.HasPullbacksAlong g] [R.HasPullbacksAlong k] + (A : R.Over ⊤ Y) : + have : HasPullback (A.hom ≫ k) g := + HasPullbacksAlong.hasPullback (A.hom ≫ k) (R.comp_mem _ _ A.prop rk) + ((R.pullbackMapTwoSquare h f g k rk rh sq).app A).left = + pullback.map A.hom f (A.hom ≫ k) g (𝟙 _) (by cat_disch) k (by cat_disch) (by cat_disch) := by + have : HasPullback (A.hom ≫ k) g := + HasPullbacksAlong.hasPullback (A.hom ≫ k) (R.comp_mem _ _ A.prop rk) + apply pullback.hom_ext <;> simp [pullbackMapTwoSquare] + +theorem isCartesian_pullbackMapTwoSquare {T : Type u} [Category.{v} T] (R : MorphismProperty T) + [R.IsStableUnderComposition] + {X Y Z W : T} (h : X ⟶ Z) (f : X ⟶ Y) (g : Z ⟶ W) (k : Y ⟶ W) (rk : R k) (rh : R h) + [R.IsStableUnderBaseChangeAlong h] [R.IsStableUnderBaseChangeAlong f] + [R.IsStableUnderBaseChangeAlong g] [R.IsStableUnderBaseChangeAlong k] + [R.HasPullbacksAlong h] [R.HasPullbacksAlong f] [R.HasPullbacksAlong g] [R.HasPullbacksAlong k] + (sq : h ≫ g = f ≫ k) : (pullbackMapTwoSquare R h f g k rk rh sq).IsCartesian := by + intro A B t + apply Functor.reflect_isPullback (Over.forget _ _ _ ⋙ CategoryTheory.Over.forget _) + have (X : R.Over ⊤ Y) : HasPullback (X.hom ≫ k) g := + HasPullbacksAlong.hasPullback (X.hom ≫ k) (R.comp_mem _ _ X.prop rk) + rw [CategoryTheory.IsPullback.flip_iff] + fapply CategoryTheory.IsPullback.of_right (v₁₃ := t.left) + (h₁₂ := pullback.fst (A.hom ≫ k) g) (h₂₂ := (pullback.fst (B.hom ≫ k) g)) + · convert_to (CategoryTheory.IsPullback (pullback.fst A.hom f) + (pullback.lift (pullback.fst A.hom f ≫ t.left) (pullback.snd A.hom f) + (by simp[pullback.condition])) t.left (pullback.fst B.hom f)) + · simp + · simp + · apply CategoryTheory.IsPullback.of_bot _ (by simp) (IsPullback.of_hasPullback B.hom f) + convert_to (IsPullback (pullback.fst A.hom f) (pullback.snd A.hom f) A.hom f) + · simp + · simp + · exact (IsPullback.of_hasPullback A.hom f) + · ext <;> simp + · convert_to + (CategoryTheory.IsPullback + (pullback.fst (A.hom ≫ k) g) + (pullback.map (A.hom ≫ k) g (B.hom ≫ k) g t.left (𝟙 _) (𝟙 _) (by simp only [Functor.id_obj, + Functor.const_obj_obj, comp_id, CategoryTheory.Over.w_assoc]) (by simp)) t.left + (pullback.fst (B.hom ≫ k) g) ) + · simp [pullback.map] + · apply CategoryTheory.IsPullback.of_bot _ (by simp) (IsPullback.of_hasPullback (B.hom ≫ k) g) + convert_to (IsPullback (pullback.fst (A.hom ≫ k) g) + (pullback.snd (A.hom ≫ k) g) (A.hom ≫ k) g) + · simp + · simp + · exact (IsPullback.of_hasPullback (A.hom ≫ k) g) + +/-- +The Beck-Chevalley two-square `pushforwardPullbackTwoSquare` is a natural isomorphism +``` + map k + R.Over Y --------> R.Over W + | | + | | +pullback f ≅ pullback g + | | + v V + R.Over X --------> R.Over Z + map h +``` +when the commutativity +condition is strengthened to a pullback condition. +``` + Y - k → W + ∧ ∧ + f | (pb) | g + | | + X - h → Z +``` +-/ +instance pullbackMapTwoSquare_isIso {T : Type u} [Category.{v} T] (R : MorphismProperty T) + [R.HasPullbacks] [R.IsStableUnderBaseChange] [R.IsStableUnderComposition] + {X Y Z W : T} (h : X ⟶ Z) (f : X ⟶ Y) (g : Z ⟶ W) (k : Y ⟶ W) + (rk : R k) (rh : R h) (pb : IsPullback h f g k) : + IsIso <| pullbackMapTwoSquare R h f g k rk rh pb.w := by + apply (config := {allowSynthFailures:= true}) NatIso.isIso_of_isIso_app + intro A + have : HasPullback (A.hom ≫ k) g := + HasPullbacksAlong.hasPullback (A.hom ≫ k) (R.comp_mem _ _ A.prop rk) + apply (config := {allowSynthFailures:= true}) Functor.ReflectsIsomorphisms.reflects + (Over.forget _ _ _ ⋙ CategoryTheory.Over.forget _) + simp only [Functor.comp_obj, Comma.forget_obj, Over.forget_obj, Over.map_obj_left, + Over.pullback_obj_left, Over.map_obj_hom, Functor.comp_map, Comma.forget_map, Over.forget_map, + pullbackMapTwoSquare_app_left, Functor.id_obj, Functor.const_obj_obj] + apply CategoryTheory.IsPullback.pullback.map_isIso_of_pullback_right_of_comm_cube + · cat_disch + · assumption + +@[simps] +def _root_.CategoryTheory.ExponentiableMorphism.isPushforward + {T : Type u} [Category.{v} T] [HasPullbacks T] + {X Y : T} (f : X ⟶ Y) [ExponentiableMorphism f] (h : Over X) : + IsPushforward f h ((ExponentiableMorphism.pushforward f).obj h) where + homEquiv := ((ExponentiableMorphism.adj f).homEquiv _ _).symm + homEquiv_comp := by intros; simp [Adjunction.homEquiv_naturality_left_symm] + +def _root_.CategoryTheory.ExponentiableMorphism.hasPushforward + {T : Type u} [Category.{v} T] [HasPullbacks T] + {X Y : T} (f : X ⟶ Y) [ExponentiableMorphism f] (h : Over X) : + HasPushforward f h where + has_representation := ⟨(ExponentiableMorphism.pushforward f).obj h, + ⟨ExponentiableMorphism.isPushforward f h⟩⟩ + +attribute [local instance] ExponentiableMorphism.hasPushforward + +instance {T : Type u} [Category.{v} T] (R : MorphismProperty T) {X Y : T} (f : X ⟶ Y) + [HasPullbacksAlong f] [HasPushforwardsAlong f] : R.HasPushforwardsAlong f where + hasPushforward := inferInstance + +/-- Given an exponentiable morphism, global pushforward (defined using the +`ExponentiableMorphism` API) commutes with local pushforward +(defined using the `HasPushforward` API). -/ +def pushforwardCompForget' {T : Type u} [Category.{v} T] [HasFiniteWidePullbacks T] + {R : MorphismProperty T} {X Y : T} (f : X ⟶ Y) [ExponentiableMorphism f] + [R.IsStableUnderPushforwardsAlong f] : R.pushforward f ⋙ Over.forget R ⊤ Y ≅ + Over.forget R ⊤ X ⋙ ExponentiableMorphism.pushforward f := + calc R.pushforward f ⋙ Over.forget R ⊤ Y + _ ≅ R.pushforwardPartial f := pushforwardCompForget .. + _ ≅ pushforwardPartial.lift R f ⋙ ObjectProperty.ι _ ⋙ ExponentiableMorphism.pushforward f := + (Functor.isoWhiskerLeft _ + (Functor.isoPartialRightAdjoint _ _ (Functor.rightAdjoint.partialRightAdjoint _))).symm + _ ≅ Over.forget R ⊤ X ⋙ ExponentiableMorphism.pushforward f := Iso.refl _ + +def pullbackPostYonedaIso {T : Type u} [Category.{v} T] + {X Y : T} (f : X ⟶ Y) [HasPullbacksAlong f] : + CategoryTheory.Over.pullback f ⋙ Over.post yoneda ≅ + Over.post yoneda ⋙ CategoryTheory.Over.pullback ym(f) := + NatIso.ofComponents + (fun A => CategoryTheory.Over.isoMk (PreservesPullback.iso yoneda A.hom f)) + (fun {A B} g => by + apply (CategoryTheory.Over.forget _).map_injective + apply pullback.hom_ext <;> simp) + +def pullbackYonedaIso {T : Type u} [Category.{max u v} T] + (R : MorphismProperty T) [R.HasPullbacks] [R.IsStableUnderBaseChange] + {X Y : T} (f : X ⟶ Y) : Over.pullback R ⊤ f ⋙ Over.yoneda R X ≅ + Over.yoneda R Y ⋙ CategoryTheory.Over.pullback ym(f) := + NatIso.ofComponents + (fun A => CategoryTheory.Over.isoMk (PreservesPullback.iso yoneda A.hom f)) + (fun {A B} g => by + apply (CategoryTheory.Over.forget _).map_injective + apply pullback.hom_ext <;> simp) + +/-- The inclusions of `Over.yoneda` commute with pushforward. -/ +def pushforwardYonedaIso {T : Type u} [Category.{u} T] + (R : MorphismProperty T) [R.HasPullbacks] [R.IsStableUnderBaseChange] + {X Y : T} (f : X ⟶ Y) [HasPullbacksAlong f] + [R.HasPushforwardsAlong f] [R.IsStableUnderPushforwardsAlong f] : + R.pushforward f ⋙ Over.yoneda R Y ≅ + Over.yoneda R X ⋙ ExponentiableMorphism.pushforward ym(f) := + -- instead of proving directly that + -- `R.pushforward f ⋙ Over.yoneda R Y ≅ Over.yoneda R X ⋙ ExponentiableMorphism.pushforward ym(f)` + -- e.g. using the universal property of `ExponentiableMorphism.pushforward ym(f)` + -- which is universal among *all* objects of `Over y(Y)`, + -- we prove that both sides are universal among objects of `Over Y` + -- (rather, their images under `Over.post yoneda`). This is `Over.yonedaNatIsoMk` + Over.yonedaNatIsoMk <| + let postFF {X} := (Functor.FullyFaithful.ofFullyFaithful (Over.post (X := X) yoneda)).homIso + -- `Over y(Y) (Over.post yoneda (-), Over.yoneda (R.pushforward f (⋆)))` + calc (R.pushforward f ⋙ Over.yoneda R Y) ⋙ yoneda ⋙ + (Functor.whiskeringLeft _ _ _).obj (Over.post yoneda).op + _ ≅ R.pushforward f ⋙ Over.forget _ _ _ ⋙ Over.post yoneda ⋙ yoneda ⋙ + (Functor.whiskeringLeft _ _ _).obj (Over.post yoneda).op := + Functor.associator .. ≪≫ Functor.isoWhiskerLeft _ (Functor.associator ..) + -- `Over Y (-, Over.forget (R.pushforward f (⋆)))` + _ ≅ R.pushforward f ⋙ Over.forget _ _ _ ⋙ yoneda := + -- `Over.post yoneda` is fully faithful + (Functor.isoWhiskerLeft _ (Functor.isoWhiskerLeft _ postFF)).symm + -- `Over Y (pullback f (-), Over.forget (⋆))` + _ ≅ Over.forget _ _ _ ⋙ yoneda ⋙ + (Functor.whiskeringLeft _ _ _).obj (CategoryTheory.Over.pullback f).op := + -- homIso for partial adjunction `Over.pullback f ∂⊣ R.pushforward f` + pushforward.homIso.symm + -- `Over (y(Y)) (pullback f ⋙ Over.post yoneda (-), Over.forget ⋙ Over.post yoneda (⋆))` + _ ≅ Over.forget _ _ _ ⋙ (Over.post yoneda ⋙ yoneda ⋙ + (Functor.whiskeringLeft _ _ _).obj ((Over.post yoneda).op)) ⋙ + (Functor.whiskeringLeft _ _ _).obj (CategoryTheory.Over.pullback f).op := + -- `Over.post yoneda` is fully faithful + Functor.isoWhiskerLeft _ (Functor.isoWhiskerRight postFF _) + _ ≅ Over.forget _ _ _ ⋙ Over.post yoneda ⋙ yoneda ⋙ (Functor.whiskeringLeft _ _ _).obj + (CategoryTheory.Over.pullback f ⋙ Over.post yoneda).op := + Functor.isoWhiskerLeft _ (Functor.associator .. ≪≫ Functor.isoWhiskerLeft _ + (Functor.isoWhiskerLeft _ ((Functor.whiskeringLeftObjCompIso ..).symm ≪≫ + Functor.mapIso _ (Functor.opComp ..).symm))) + -- `Over (y(Y)) (pullback f ⋙ Over.post yoneda (-), Over.yoneda (⋆))` + _ ≅ Over.yoneda R X ⋙ yoneda ⋙ (Functor.whiskeringLeft _ _ _).obj + (CategoryTheory.Over.pullback f ⋙ Over.post yoneda).op := + (Functor.associator ..).symm + -- `Over (y(Y)) (pullback ym(f) (-), pushforward ym(f) (Over.yoneda (⋆)))` + _ ≅ Over.yoneda R X ⋙ yoneda ⋙ (Functor.whiskeringLeft _ _ _).obj + (Over.post yoneda ⋙ CategoryTheory.Over.pullback ym(f)).op := + -- `Over.post yoneda` preserves pullback + Functor.isoWhiskerLeft _ (Functor.isoWhiskerLeft _ (Functor.mapIso _ + (NatIso.op (pullbackPostYonedaIso ..).symm))) + _ ≅ Over.yoneda R X ⋙ yoneda ⋙ + (Functor.whiskeringLeft _ _ _).obj (CategoryTheory.Over.pullback ym(f)).op ⋙ + (Functor.whiskeringLeft _ _ _).obj (Over.post yoneda).op := + Functor.isoWhiskerLeft _ (Functor.isoWhiskerLeft _ + (Functor.mapIso _ (Functor.opComp ..) ≪≫ Functor.whiskeringLeftObjCompIso ..)) + -- `Over (y(Y)) (Over.post yoneda (-), pushforward ym(f) (Over.yoneda (⋆)))` + _ ≅ Over.yoneda R X ⋙ ExponentiableMorphism.pushforward ym(f) ⋙ yoneda ⋙ + (Functor.whiskeringLeft _ _ _).obj (Over.post yoneda).op := + -- by homIso for adjunction `pullback ym(f) ⊣ pushforward ym(f)` + Functor.isoWhiskerLeft _ ((Functor.associator ..).symm ≪≫ (Functor.isoWhiskerRight + (ExponentiableMorphism.adj ym(f)).homIso _) ≪≫ Functor.associator ..) + _ ≅ (Over.yoneda R X ⋙ ExponentiableMorphism.pushforward ym(f)) ⋙ yoneda ⋙ + (Functor.whiskeringLeft _ _ _).obj (Over.post yoneda).op := + (Functor.associator ..).symm + +/-- Fixing a pullback square, +``` + Z - g → W + ∧ ∧ + h | (pb) | k + | | + X - f → Y +``` +`pushforwardPullbackIso` is the Beck-Chevalley natural isomorphism for pushforwards between +the `MorphismProperty.Over` categories, +of type `pushforward g ⋙ pullback k ≅ pullback h ⋙ pushforward f`. +``` + R.Over ⊤ Z - pushforward g → R.Over ⊤ W + | | +pullback h | ↙≅ | pullback k + V V + R.Over ⊤ X - pushforward f → R.Over ⊤ Y +``` +-/ +def pushforwardPullbackIso {T : Type u} [Category.{u} T] {R : MorphismProperty T} + [R.HasPullbacks] [R.IsStableUnderBaseChange] + {X Y Z W : T} (h : X ⟶ Z) (f : X ⟶ Y) (g : Z ⟶ W) (k : Y ⟶ W) + [HasPullbacksAlong f] [HasPullbacksAlong g] + [R.HasPushforwardsAlong f] [R.IsStableUnderPushforwardsAlong f] + [R.HasPushforwardsAlong g] [R.IsStableUnderPushforwardsAlong g] + (pb : IsPullback h f g k) : + R.pushforward g ⋙ Over.pullback R ⊤ k ≅ Over.pullback R ⊤ h ⋙ R.pushforward f := + -- since `Over.yoneda R Y : R.Over ⊤ Y ⥤ Over y(Y)` is fully faithful, + -- it suffices to define an isomorphism between the post-composed functors + (Functor.FullyFaithful.whiskeringRight + (Functor.FullyFaithful.ofFullyFaithful (Over.yoneda R Y)) (R.Over ⊤ Z)).preimageIso <| + calc (R.pushforward g ⋙ Over.pullback R ⊤ k) ⋙ Over.yoneda R Y + _ ≅ R.pushforward g ⋙ Over.pullback R ⊤ k ⋙ Over.yoneda R Y := Functor.associator _ _ _ + _ ≅ R.pushforward g ⋙ Over.yoneda R W ⋙ CategoryTheory.Over.pullback ym(k) := + -- pullback commutes with `Over.yoneda` + Functor.isoWhiskerLeft _ (pullbackYonedaIso R k) + _ ≅ (R.pushforward g ⋙ Over.yoneda R W) ⋙ CategoryTheory.Over.pullback ym(k) := + (Functor.associator _ _ _).symm + _ ≅ (Over.yoneda R Z ⋙ ExponentiableMorphism.pushforward ym(g)) ⋙ + CategoryTheory.Over.pullback ym(k) := + -- pushforward commutes with `Over.yoneda` + Functor.isoWhiskerRight (pushforwardYonedaIso ..) _ + _ ≅ Over.yoneda R Z ⋙ ExponentiableMorphism.pushforward ym(g) ⋙ + CategoryTheory.Over.pullback ym(k) := Functor.associator _ _ _ + _ ≅ Over.yoneda R Z ⋙ CategoryTheory.Over.pullback ym(h) ⋙ + ExponentiableMorphism.pushforward ym(f) := + -- Beck-Chevalley isomorphism in `Psh T` + Functor.isoWhiskerLeft _ (pushforwardPullbackIsoSquare (Functor.map_isPullback _ pb)) + _ ≅ (Over.yoneda R Z ⋙ CategoryTheory.Over.pullback ym(h)) ⋙ + ExponentiableMorphism.pushforward ym(f) := (Functor.associator _ _ _).symm + _ ≅ (Over.pullback R ⊤ h ⋙ Over.yoneda R X) ⋙ ExponentiableMorphism.pushforward ym(f) := + -- pullback commutes with `Over.yoneda` + Functor.isoWhiskerRight (pullbackYonedaIso R h).symm _ + _ ≅ Over.pullback R ⊤ h ⋙ Over.yoneda R X ⋙ ExponentiableMorphism.pushforward ym(f) := + Functor.associator _ _ _ + _ ≅ Over.pullback R ⊤ h ⋙ R.pushforward f ⋙ Over.yoneda R Y := + -- pushforward commutes with `Over.yoneda` + Functor.isoWhiskerLeft _ (pushforwardYonedaIso ..).symm + _ ≅ (Over.pullback R ⊤ h ⋙ R.pushforward f) ⋙ Over.yoneda R Y := (Functor.associator _ _ _).symm + +/-- Fixing a commutative square, +``` + Z - g → W + ∧ ∧ + h | | k + | | + X - f → Y +``` +`pushforwardPullbackTwoSquare` is the Beck-Chevalley natural transformation for pushforwards between +the `MorphismProperty.Over` categories, +of type `pushforward g ⋙ pullback k ⟶ pullback h ⋙ pushforward f`. +``` + R.Over ⊤ Z - pushforward g → R.Over ⊤ W + | | +pullback h | ↙ | pullback k + V V + R.Over ⊤ X - pushforward f → R.Over ⊤ Y +``` +It is the mate of the square of pullback functors +`pullback k ⋙ pullback g ⟶ pullback f ⋙ pullback h`. +-/ +def pushforwardPullbackTwoSquare {T : Type u} [Category.{v} T] {R : MorphismProperty T} + [R.HasPullbacks] [R.IsStableUnderBaseChange] {X Y Z W : T} + (h : X ⟶ Z) (f : X ⟶ Y) (g : Z ⟶ W) (k : Y ⟶ W) (sq : h ≫ g = f ≫ k) + [HasPullbacksAlong f] [HasPullbacksAlong g] + [R.HasPushforwardsAlong f] [R.IsStableUnderPushforwardsAlong f] + [R.HasPushforwardsAlong g] [R.IsStableUnderPushforwardsAlong g] : + TwoSquare (pushforward R g) (Over.pullback R ⊤ h) (Over.pullback R ⊤ k) + (pushforward R f) := + mateEquiv (pullbackPushforwardAdjunction R g) (pullbackPushforwardAdjunction R f) + (pullbackPullbackTwoSquare _ _ _ _ sq) + +-- TODO: currently this theorem is unnecessary, +-- but it would be nice to show that these two definitions actually line up. +-- We have both definitions because +-- `pushforwardPullbackTwoSquare` can be defined under more general conditions, +-- without a pullback condition on the commuting square +-- but constructing an isomorphism directly `pushforwardPullbackIso` is easier +-- than showing `pushforwardPullbackTwoSquare` is an isomorphism. + +/- +/-- +The Beck-Chevalley two-square `pushforwardPullbackTwoSquare` is a natural isomorphism +``` + R.Over ⊤ Z - pushforward g → R.Over ⊤ W + | | +pullback h | ≅ | pullback k + V V + R.Over ⊤ X - pushforward f → R.Over ⊤ Y +``` +when the commutativity +condition is strengthened to a pullback condition. +``` + Z - g → W + ∧ ∧ + h | (pb) | k + | | + X - f → Y +``` +TODO: in what generality does this theorem hold? +NOTE: we know it holds when for π-clans with `R = Q = the π-clan` +([Joyal, Notes on Clans and Tribes, Cor 2.4.11](https://arxiv.org/pdf/1710.10238)). +NOTE: we also know it holds in a category with pullbacks with `R = ⊤` and `Q = ExponentiableMaps`. +-/ +theorem pushforwardPullbackTwoSquare_isIso {T : Type u} [Category.{u} T] + (R : MorphismProperty T) + [R.HasPullbacks] [R.IsStableUnderBaseChange] + {X Y Z W : T} (h : X ⟶ Z) (f : X ⟶ Y) (g : Z ⟶ W) (k : Y ⟶ W) + [HasPullbacksAlong f] [HasPullbacksAlong g] + [R.HasPushforwardsAlong f] [R.IsStableUnderPushforwardsAlong f] + [R.HasPushforwardsAlong g] [R.IsStableUnderPushforwardsAlong g] + (pb : IsPullback h f g k) : + IsIso (pushforwardPullbackTwoSquare (R := R) h f g k pb.w) := by + have eq : (pushforwardPullbackTwoSquare h f g k pb.w) = + (pushforwardPullbackIso (R := R) h f g k pb).hom := by + ext A : 1 + -- simp [pushforwardPullbackTwoSquare, pushforwardPullbackIso] + sorry + rw [eq] + infer_instance +-/ diff --git a/HoTTLean/ForMathlib/CategoryTheory/ClovenIsofibration.lean b/HoTTLean/ForMathlib/CategoryTheory/ClovenIsofibration.lean new file mode 100644 index 00000000..5155a053 --- /dev/null +++ b/HoTTLean/ForMathlib/CategoryTheory/ClovenIsofibration.lean @@ -0,0 +1,800 @@ +import Mathlib.CategoryTheory.FiberedCategory.HomLift +import Mathlib.CategoryTheory.FiberedCategory.Fiber +import HoTTLean.Grothendieck.Groupoidal.IsPullback +import HoTTLean.Grothendieck.Groupoidal.Basic +import HoTTLean.Groupoids.Pi + +universe w v u v₁ u₁ v₂ u₂ v₃ u₃ + +noncomputable section + +namespace CategoryTheory + +namespace Functor + +namespace Fiber +section + +variable {𝒮 : Type u₁} {𝒳 : Type u₂} [Category.{v₁} 𝒮] [Category.{v₂} 𝒳] +variable {p : 𝒳 ⥤ 𝒮} {S : 𝒮} + +@[simp] +lemma functor_obj_fiberInclusion_obj (a : Fiber p S) : + p.obj (Fiber.fiberInclusion.obj a) = S := + a.2 + +lemma functor_map_fiberInclusion_map {a b : Fiber p S} + (f : a ⟶ b) : + p.map (Fiber.fiberInclusion.map f) = eqToHom (by simp) := by + have H := f.2 + simpa using IsHomLift.fac' p (𝟙 S) f.1 + +lemma hext {S'} (hS : S' ≍ S) {a : Fiber p S} + {a' : Fiber p S'} (h : Fiber.fiberInclusion.obj a ≍ Fiber.fiberInclusion.obj a') : a ≍ a' := by + subst hS + simpa using Subtype.ext h.eq + +lemma hom_hext {S'} (hS : S' ≍ S) {a b : Fiber p S} + {a' b' : Fiber p S'} (ha : a ≍ a') (hb : b ≍ b') {φ : a ⟶ b} + {ψ : a' ⟶ b'} (h : Fiber.fiberInclusion.map φ ≍ Fiber.fiberInclusion.map ψ) : φ ≍ ψ := by + aesop_cat + +end + +variable {Γ : Type u} {E : Type u} [Groupoid.{v} Γ] [Groupoid.{v} E] {F : E ⥤ Γ} + +instance {X : Γ} : IsGroupoid (F.Fiber X) where + all_isIso f := { + out := + have := f.2 + ⟨Fiber.homMk F _ (CategoryTheory.inv f.1), by cat_disch, by cat_disch⟩ } + +instance {X : Γ} : Groupoid (F.Fiber X) := Groupoid.ofIsGroupoid + +end Fiber + +section + +structure ClovenIsofibration {C : Type u} {D : Type u₁} [Category.{v} C] [Category.{v₁} D] + (F : C ⥤ D) where + liftObj {X Y : D} (f : X ⟶ Y) [IsIso f] {X' : C} (hX' : F.obj X' = X) : C + liftIso {X Y : D} (f : X ⟶ Y) [IsIso f] {X' : C} (hX' : F.obj X' = X) : X' ⟶ liftObj f hX' + isHomLift {X Y : D} (f : X ⟶ Y) [IsIso f] {X' : C} (hX' : F.obj X' = X) : + F.IsHomLift f (liftIso f hX') + liftIso_IsIso {X Y : D} (f : X ⟶ Y) [IsIso f] {X' : C} (hX' : F.obj X' = X) : + IsIso (liftIso f hX') + +namespace ClovenIsofibration + +section + +variable {C : Type u} {D : Type u₁} [Category.{v} C] [Category.{v₁} D] {F : C ⥤ D} + (I : ClovenIsofibration F) + +instance {X Y : D} (f : X ⟶ Y) [IsIso f] {X' : C} (hX' : F.obj X' = X) : + F.IsHomLift f (I.liftIso f hX') := I.isHomLift f hX' + +instance {X Y : D} (f : X ⟶ Y) [IsIso f] {X' : C} (hX' : F.obj X' = X): + IsIso (ClovenIsofibration.liftIso I f hX') := ClovenIsofibration.liftIso_IsIso I f hX' + +@[simp] +lemma obj_liftObj {X Y : D} (f : X ⟶ Y) [IsIso f] + {X' : C} (hX' : F.obj X' = X) : F.obj (I.liftObj f hX') = Y := + IsHomLift.codomain_eq F f (I.liftIso f hX') + +lemma map_liftIso {X Y : D} (f : X ⟶ Y) [IsIso f] {X' : C} + (hX' : F.obj X' = X) : + eqToHom hX'.symm ≫ F.map (I.liftIso f hX') ≫ eqToHom (obj_liftObj ..) = f := by + have i : F.IsHomLift f (I.liftIso f hX') := I.isHomLift .. + symm + apply IsHomLift.fac + +lemma map_liftIso' {X Y : D} (f : X ⟶ Y) [IsIso f] {X' : C} + (hX' : F.obj X' = X) : F.map (I.liftIso f hX') = + eqToHom hX' ≫ f ≫ eqToHom (by simp[obj_liftObj]) := by + simp[← map_liftIso I f hX'] + +@[simp] +lemma liftObj_comp_aux {X Y : D} (f : X ⟶ Y) [IsIso f] {X' : C} + (hX' : F.obj X' = X) (Y' : C) (hY' : I.liftObj f hX' = Y') : F.obj Y' = Y := by + subst hY' + apply ClovenIsofibration.obj_liftObj I f + +lemma eqToHom_comp_liftIso {X Y : D} (f : X ⟶ Y) [IsIso f] {X' X'' : C} + (hX' : F.obj X' = X) (hX'' : X'' = X') : + eqToHom hX'' ≫ I.liftIso f hX' = + I.liftIso f (X' := X'') (by rw [hX'', hX']) ≫ eqToHom (by subst hX''; rfl) := by + subst hX'' + simp + +class IsSplit {C : Type u} {D : Type u₁} [Category.{v} C] [Category.{v₁} D] + {F : C ⥤ D} (I : ClovenIsofibration F) where + liftObj_id {X : D} {X' : C} (hX' : F.obj X' = X) : I.liftObj (𝟙 X) hX' = X' + liftIso_id {X : D} {X' : C} (hX' : F.obj X' = X) : I.liftIso (𝟙 X) hX' = + eqToHom (liftObj_id hX').symm + liftObj_comp {X Y Z : D} (f : X ⟶ Y) [IsIso f] (g : Y ⟶ Z) [IsIso g] {X' : C} + (hX' : F.obj X' = X) {Y' : C} (hY' : I.liftObj f hX' = Y') : I.liftObj (f ≫ g) hX' = + I.liftObj g (X' := Y') (I.liftObj_comp_aux f hX' Y' hY') + liftIso_comp {X Y Z : D} (f : X ⟶ Y) [IsIso f] (g : Y ⟶ Z) [IsIso g] {X' : C} + (hX' : F.obj X' = X) {Y' : C} (hY' : I.liftObj f hX' = Y') : I.liftIso (f ≫ g) hX' = + I.liftIso f hX' ≫ eqToHom hY' ≫ + I.liftIso g (X' := Y') (I.liftObj_comp_aux f hX' Y' hY') ≫ + eqToHom (liftObj_comp f g hX' hY').symm + +end + +open IsSplit + +@[simp] +lemma liftObj_eqToHom {C : Type u} {D : Type u₁} [Category.{v} C] [Category.{v₁} D] + {F : C ⥤ D} (I : ClovenIsofibration F) [IsSplit I] {X Y : D} (h : X = Y) {X' : C} + (hX' : F.obj X' = X) : I.liftObj (eqToHom h) hX' = X' := by + subst h + simp [IsSplit.liftObj_id] + +@[simp] +lemma liftIso_eqToHom {C : Type u} {D : Type u₁} [Category.{v} C] [Category.{v₁} D] (F : C ⥤ D) + (I : ClovenIsofibration F) [IsSplit I] {X Y : D} (h : X = Y) {X' : C} (hX' : F.obj X' = X) : + I.liftIso (eqToHom h) hX' = eqToHom (by simp) := by + subst h + simp [IsSplit.liftIso_id] + +section +variable {Γ : Type u} {E : Type u} [Groupoid.{v} Γ] [Groupoid.{v} E] {F : E ⥤ Γ} + (I : ClovenIsofibration F) + +def classifier.map.obj {X Y : Γ} (f : X ⟶ Y) (a : F.Fiber X) : F.Fiber Y := + ⟨I.liftObj f a.2, ClovenIsofibration.obj_liftObj ..⟩ + +def classifier.map.map {X Y} (f: X ⟶ Y) {a b : F.Fiber X} (m : a ⟶ b) : + map.obj I f a ⟶ map.obj I f b := + let i1 : a.1 ⟶ I.liftObj f a.2 := I.liftIso f a.2 + let i2 := I.liftIso f b.2 + let i := Groupoid.inv i1 ≫ Fiber.fiberInclusion.map m ≫ i2 + have e :𝟙 Y = eqToHom (by simp[obj_liftObj]) ≫ + F.map (CategoryTheory.inv i1 ≫ Fiber.fiberInclusion.map m ≫ i2) ≫ eqToHom (by simp[obj_liftObj]) + := by simp[i1, i2, Fiber.functor_map_fiberInclusion_map, Functor.map_inv,map_liftIso'] + have : F.IsHomLift (𝟙 Y) i := by + simp only[i, e] + apply IsHomLift.of_fac _ _ _ (ClovenIsofibration.obj_liftObj ..) + (ClovenIsofibration.obj_liftObj ..) + simp + Fiber.homMk F _ i + +lemma classifier.map.map_id {X Y} (f : X ⟶ Y) (a: F.Fiber X): + map.map I f (𝟙 a) = 𝟙 (map.obj I f a) := by + ext + simp only [map, Fiber.fiberInclusion_homMk, Groupoid.inv_eq_inv, Functor.map_id, + IsIso.inv_comp_eq] + simp [Fiber.fiberInclusion, classifier.map.obj] + +lemma classifier.map.map_comp {X Y} (f: X ⟶ Y) {a b c: F.Fiber X} (m1 : a ⟶ b) (m2: b ⟶ c): + map.map I f (m1 ≫ m2) = map.map I f m1 ≫ map.map I f m2 := by + ext + simp[classifier.map.map] + +@[simps] +def classifier.map {X Y} (f : X ⟶ Y) : F.Fiber X ⥤ F.Fiber Y where + obj := classifier.map.obj I f + map := classifier.map.map I f + map_id := classifier.map.map_id I f + map_comp := classifier.map.map_comp I f + +variable [IsSplit I] + +lemma classifier.map_id (X : Γ) : classifier.map I (𝟙 X) = 𝟙 (Grpd.of (F.Fiber X)) := by + fapply Functor.ext + · intro a + apply Subtype.ext + simp [map.obj, liftObj_id] + · intro a b f + simp + ext + simp [map.map, liftIso_id, eqToHom_map] + +lemma classifier.map_comp {X Y Z: Γ} (f : X⟶ Y) (g : Y ⟶ Z): + classifier.map I (f ≫ g) = classifier.map I f ⋙ classifier.map I g := by + fapply Functor.ext + · intro a + simp[map.obj, liftObj_comp] + · intro a b f + simp + ext + simp only [map.map, Fiber.fiberInclusion_homMk, Groupoid.inv_eq_inv, ← Category.assoc, + Functor.map_comp, eqToHom_map, ← heq_eq_eq, heq_comp_eqToHom_iff] + simp [liftIso_comp,← Category.assoc] + +/-- Any split isofibration of groupoids is classified up to isomorphism +as the (groupoidal) Grothendieck construction on the functor `classifier`. -/ +def classifier : Γ ⥤ Grpd.{v,u} where + obj X := Grpd.of (F.Fiber X) + map f := Grpd.homOf (classifier.map I f) + map_id _ := classifier.map_id .. + map_comp _ _ := classifier.map_comp .. + +@[simp] +lemma fiberInclusion_obj_classifier_map_obj {x y} (f : x ⟶ y) (p) : + Fiber.fiberInclusion.obj ((I.classifier.map f).obj p) = I.liftObj f p.2 := by + simp [classifier, classifier.map.obj, Fiber.fiberInclusion] + +open CategoryTheory.Functor.Groupoidal + +def grothendieckClassifierIso.hom.obj (pair: ∫ I.classifier) : E := pair.fiber.1 + +lemma grothendieckClassifierIso.hom.map_aux {X Y: Γ} (f: X ⟶ Y) (a: I.classifier.obj X) : + (I.classifier.map f).obj a = ⟨I.liftObj (X' := a.1) f a.2, obj_liftObj ..⟩ := by + simp[classifier,classifier.map.obj] + +lemma grothendieckClassifierIso.hom.map_aux2 + (X: Γ) (a: I.classifier.obj X) : F.obj a.1 = X := by + simp[classifier] at a + simp[a.2] + +def grothendieckClassifierIso.hom.map {p1 p2: ∫ I.classifier} (h: p1 ⟶ p2) : + (p1.fiber.1 ⟶ p2.fiber.1) := + I.liftIso h.base (hom.map_aux2 ..) ≫ + (eqToHom (by simp[grothendieckClassifierIso.hom.map_aux] )) ≫ h.fiber.1 + +def grothendieckClassifierIso.hom.map' {p1 p2: ∫ I.classifier} (h: p1 ⟶ p2) : + (p1.fiber.1 ⟶ p2.fiber.1) := + I.liftIso h.base (hom.map_aux2 ..) ≫ + (eqToHom (by simp[grothendieckClassifierIso.hom.map_aux,Fiber.fiberInclusion] )) ≫ + Fiber.fiberInclusion.map h.fiber ≫ (eqToHom (by simp[Fiber.fiberInclusion] )) + +lemma grothendieckClassifierIso.hom.map_id (X : ∫ I.classifier) : + hom.map I (𝟙 X) = 𝟙 _ := by + convert_to _ ≫ _ ≫ Fiber.fiberInclusion.map (Hom.fiber (𝟙 X)) = _ + simp [liftIso_id, eqToHom_map] + +lemma grothendieckClassifierIso.hom.map_comp {X Y Z: ∫ I.classifier} (f : X ⟶ Y) (g : Y ⟶ Z) : + hom.map' I (f ≫ g) = hom.map' I f ≫ hom.map' I g := by + simp [map', liftIso_comp, eqToHom_map, classifier, classifier.map.map] + +@[simps!] +def grothendieckClassifierIso.hom.hom {X Y} (f : X ⟶ Y) : + Fiber.fiberInclusion ⟶ I.classifier.map f ⋙ Fiber.fiberInclusion where + app _ := I.liftIso f .. + naturality := by + intro a b g + simp[Fiber.fiberInclusion,classifier,classifier.map.map,Fiber.homMk] + +def grothendieckClassifierIso.hom : ∫ I.classifier ⥤ E := + Groupoidal.functorFrom (fun x => Fiber.fiberInclusion) + (grothendieckClassifierIso.hom.hom I) + (by intro X; ext;simp[hom.hom,liftIso_id]) + (by intro X Y Z f g; ext; simp[hom.hom,liftIso_comp]) + +def grothendieckClassifierIso.inv.fibMap {X Y}(f : X ⟶ Y) : + ((F ⋙ I.classifier).map f).obj ⟨X,rfl⟩ ⟶ ⟨Y, rfl⟩ := by + refine @Fiber.homMk _ _ _ _ F (F.obj Y) _ _ ?_ ?_ + · exact CategoryTheory.inv (I.liftIso (F.map f) rfl) ≫ f + · simp + fapply IsHomLift.of_fac + · simp[ClovenIsofibration.obj_liftObj] + · rfl + · simp[Functor.map_inv,ClovenIsofibration.map_liftIso'] + +lemma grothendieckClassifierIso.inv.fibMap_id (x : E) : + inv.fibMap I (𝟙 x) = eqToHom (by simp) := by + apply Fiber.hom_ext + simp only [comp_obj, comp_map, fibMap, Fiber.fiberInclusion_homMk, Category.comp_id] + rw![Functor.map_id,liftIso_id] + simp[inv_eqToHom,eqToHom_map] + +lemma grothendieckClassifierIso.inv.fibMap_comp {x y z : E} (f : x ⟶ y) (g : y ⟶ z) : + inv.fibMap I (f ≫ g) = + eqToHom (by simp) ≫ + (I.classifier.map (F.map g)).map (inv.fibMap I f) ≫ inv.fibMap I g := by + simp only [comp_obj, comp_map, fibMap] + apply Fiber.hom_ext + rw! [Functor.map_comp] + simp [liftIso_comp, eqToHom_map,classifier,classifier.map.map] + +lemma ι_classifier_comp_forget {x} : ι I.classifier x ⋙ Groupoidal.forget = + Fiber.fiberInclusion ⋙ F := by + fapply Functor.ext + · intro p + exact p.2.symm + · intro p q f + simpa using IsHomLift.fac .. + +@[simp] +lemma liftObj_map_fiberInclusion_map {S} {X Y : Fiber F S} {X' : E} (f : X ⟶ Y) + [IsIso (F.map (Fiber.fiberInclusion.map f))] {hX' : X' = Fiber.fiberInclusion.obj X} : + I.liftObj (F.map (Fiber.fiberInclusion.map f)) (X' := X') (by simp [hX']) + = Fiber.fiberInclusion.obj X := by + rw! [Fiber.functor_map_fiberInclusion_map, liftObj_eqToHom, hX'] + +@[simp] +lemma liftIso_map_fiberInclusion_map {S} {X Y : Fiber F S} {X' : E} (f : X ⟶ Y) + [IsIso (F.map (Fiber.fiberInclusion.map f))] {hX' : X' = Fiber.fiberInclusion.obj X} : + I.liftIso (F.map (Fiber.fiberInclusion.map f)) (X' := X') (by simp [hX']) + = eqToHom (by simp [hX']) := by + rw! [Fiber.functor_map_fiberInclusion_map, liftIso_eqToHom] + +open grothendieckClassifierIso in +/-- A split isofibration `F : E ⥤ Γ` is classified by the functor `I.classifier : Γ ⥤ Grpd`. +This means that the (groupoidal) Grothendieck construction on `I.classifier` is isomorphic to +`E` over `Γ`. This isomorphism is called `grothendieckClassifierIso`. -/ +def grothendieckClassifierIso : ∫ I.classifier ≅≅ E := + Groupoidal.functorIsoFrom (fun x => Fiber.fiberInclusion) + (hom.hom I) (by intro X; ext; simp [liftIso_id]) + (by intro X Y Z f g; ext; simp [liftIso_comp]) + F (fun x => ⟨x, rfl⟩) (inv.fibMap I) (inv.fibMap_id I) (inv.fibMap_comp I) + (by simp [ι_classifier_comp_forget]) + (by + intro x p + simp only [comp_obj] + apply Subtype.hext HEq.rfl + · simp [Functor.Fiber.functor_obj_fiberInclusion_obj] + · simp [Fiber.fiberInclusion]) + (by + intro x p q f + simp only [inv.fibMap] + apply Fiber.hom_hext + any_goals apply Fiber.hext + all_goals simp [Fiber.functor_obj_fiberInclusion_obj q]) + (by intro x; simp [Fiber.fiberInclusion]) + (by + intro x y f + simp [inv.fibMap]) + (by simp) + (by simp [I.map_liftIso']) + (by + intro x y f p + simp only [inv.fibMap] + apply Fiber.hom_hext + any_goals apply Fiber.hext + any_goals simp + · rw! [map_liftIso', liftObj_comp _ _ _ rfl, liftObj_comp _ _ _ rfl] + simp [liftObj_eqToHom] + · rw! [map_liftIso', liftIso_comp _ _ _ rfl, liftIso_comp _ _ _ rfl] + simp only [liftIso_eqToHom, eqToHom_refl, eqToHom_trans, Category.id_comp, Category.assoc, + IsIso.inv_comp, inv_eqToHom, eqToHom_comp_liftIso, IsIso.inv_hom_id_assoc] + rw! [eqToHom_heq_id_cod] + apply eqToHom_heq_id + rw [liftObj_comp _ _ _ rfl, liftObj_comp _ _ _ rfl] + simp) + +lemma grothendieckClassifierIso.inv_comp_forget : + (grothendieckClassifierIso I).inv ⋙ Groupoidal.forget = F := + rfl + +lemma grothendieckClassifierIso.hom_comp_self : + (grothendieckClassifierIso I).hom ⋙ F = Groupoidal.forget := by + slice_lhs 2 3 => rw[← inv_comp_forget I (F := F)] + simp + +end + +@[simps!] +def iso {A : Type u} [Category.{v} A] {B : Type u₁} [Category.{v₁} B] (F : A ≅≅ B) : + ClovenIsofibration F.hom where + liftObj {b0 b1} f hf x hF := F.inv.obj b1 + liftIso {b0 b1} f hf x hF := eqToHom (by simp [← hF, ← Functor.comp_obj]) ≫ F.inv.map f + isHomLift f hf x hF := IsHomLift.of_fac' _ _ _ hF (by simp [← Functor.comp_obj]) + (by + simp only [map_comp, eqToHom_map, ← comp_map] + rw! (castMode := .all) [F.inv_hom_id]; + simp [← heq_eq_eq] + rfl) + liftIso_IsIso := by + intro X Y f i X' hX' + apply IsIso.comp_isIso + +instance {A : Type u} [Category.{v} A] {B : Type u₁} [Category.{v₁} B] (F : A ≅≅ B) : + IsSplit (iso F) where + liftObj_id h := by simp [← h, ← Functor.comp_obj] + liftIso_id := by simp + liftObj_comp := by simp + liftIso_comp := by simp + +@[simp] +abbrev iso_inv {A B : Type u} [Category.{v} A] [Category.{v} B] (F : A ≅≅ B) : + ClovenIsofibration F.inv := iso (F.symm) + +section + +variable {C : Type u₁} [Groupoid.{v₁,u₁} C] {F : C ⥤ Grpd.{v₂,u₂}} + +def forget.liftObj {X Y: C} (f : X ⟶ Y) + {X' : F.Groupoidal} (hX': Groupoidal.forget.obj X' = X) : F.Groupoidal := + Groupoidal.transport (C := C) (c := Y) X' (eqToHom (by subst hX'; simp) ≫ f) + +def forget.liftIso {X Y: C} (f : X ⟶ Y) {X' : F.Groupoidal} (hX': Groupoidal.forget.obj X' = X) : + X' ⟶ forget.liftObj f hX' := + Groupoidal.toTransport X' (eqToHom (by subst hX'; simp) ≫ f) + +lemma forget.isHomLift {X Y: C} (f : X ⟶ Y) {X' : F.Groupoidal} + (hX': Groupoidal.forget.obj X' = X) : Groupoidal.forget.IsHomLift f (forget.liftIso f hX') := by + apply IsHomLift.of_fac' (ha := hX') (hb := by simp[liftObj]) + simp[liftIso] + +def toTransport_IsIso (x : F.Groupoidal) {c : C} (t : x.base ⟶ c) : + IsIso (Groupoidal.toTransport x t) := + inferInstance + +variable (F) in +@[simps!] +def forget : ClovenIsofibration (Groupoidal.forget (F := F)) where + liftObj f := forget.liftObj f + liftIso f := forget.liftIso f + isHomLift f := forget.isHomLift f + liftIso_IsIso := inferInstance + +instance {X Y: C} (f : X ⟶ Y) [IsIso f] {X' : F.Groupoidal} + (hX': Groupoidal.forget.obj X' = X) : IsIso (forget.liftIso f hX') := by + apply toTransport_IsIso + +def forget.liftObj_id {X: C} {X' : F.Groupoidal} (hX': Groupoidal.forget.obj X' = X) : + forget.liftObj (𝟙 X) hX' = X' := by + simp [liftObj, Groupoidal.transport_eqToHom] + +def forget.liftIso_id {X: C} {X' : F.Groupoidal} (hX': Groupoidal.forget.obj X' = X) : + forget.liftIso (𝟙 X) hX' = eqToHom (by simp [forget.liftObj_id]) := by + dsimp [liftIso] + rw! (castMode :=.all)[Category.comp_id] + simp only [Groupoidal.toTransport_eqToHom, ← heq_eq_eq, eqRec_heq_iff_heq] + congr! + +lemma forget.liftObj_comp {X Y Z: C} (f : X ⟶ Y) (g : Y ⟶ Z) + {X' : F.Groupoidal} (hX' : X'.base = X) + {Y' : F.Groupoidal} (hY' : forget.liftObj f hX' = Y') : + forget.liftObj (f ≫ g) hX' = forget.liftObj g (liftObj_comp_aux (forget F) f hX' Y' hY') := by + simp only [liftObj,Groupoidal.transport_comp] + simp only [Groupoidal.transport, Grothendieck.transport, comp_obj, comp_map] + fapply Grothendieck.ext + · simp + simp only [Grpd.forgetToCat, Cat.of_α, id_eq, comp_obj, eqToHom_refl, comp_map, map_id, + Grpd.id_eq_id, id_obj] + congr! + simp only [← comp_obj,← Grpd.comp_eq_comp,← Functor.map_comp] + rw! [eqToHom_map] + subst hY' + simp [liftObj,Groupoidal.transport] + +lemma forget.liftIso_comp {X Y Z: C} (f : X ⟶ Y) (g : Y ⟶ Z) {X' : F.Groupoidal} + (hX' : X'.base = X) {Y' : F.Groupoidal} (hY' : forget.liftObj f hX' = Y') : + forget.liftIso (f ≫ g) hX' = forget.liftIso f hX' ≫ eqToHom hY' ≫ + forget.liftIso g (liftObj_comp_aux (forget F) f hX' Y' hY') ≫ + eqToHom (by symm; apply forget.liftObj_comp; assumption) := by + subst hX' hY' + simp only [liftIso, eqToHom_refl, Groupoidal.toTransport_comp, Groupoidal.toTransport_id, + Category.assoc, eqToHom_trans, Category.id_comp, eqToHom_trans_assoc] + congr 2 + simp only [liftObj, eqToHom_refl, ← Category.assoc, ← heq_eq_eq, heq_comp_eqToHom_iff, + heq_eqToHom_comp_iff, comp_eqToHom_heq_iff] + congr 1 + rw [Groupoidal.transport_congr ((X'.transport (𝟙 X'.base))) X' (by rw[Groupoidal.transport_id]) + f f (by simp), Groupoidal.transport_congr (X'.transport (𝟙 X'.base ≫ f)) (X'.transport f) _ + ((𝟙 (X'.transport (𝟙 X'.base ≫ f)).base)) (eqToHom (by simp))] + all_goals simp [Groupoidal.transport_id] + +instance : IsSplit (forget F) where + liftObj_id := forget.liftObj_id + liftIso_id := forget.liftIso_id + liftObj_comp _ _ _ _ := by apply forget.liftObj_comp + liftIso_comp _ _ _ _ := by apply forget.liftIso_comp + +end + +def id (A : Type u) [Category.{v} A] : ClovenIsofibration (𝟭 A) := + iso (Functor.Iso.refl _) + +instance (A : Type u) [Category.{v} A] : IsSplit (id A) := + inferInstanceAs <| IsSplit (iso (Functor.Iso.refl _)) + +section + +variable {A B C : Type*} [Category A] [Category B] [Category C] {F : A ⥤ B} + (IF : ClovenIsofibration F) {G : B ⥤ C} (IG : ClovenIsofibration G) + +def comp.liftObj {X Y: C} (f: X ⟶ Y) [IsIso f] {X': A} (hX': (F ⋙ G).obj X' = X) : A := + let f1 := IG.liftIso (X' := F.obj X') f (by simp at hX'; assumption) + IF.liftObj (X' := X') f1 rfl + +lemma comp.obj_liftObj {X Y: C} (f: X ⟶ Y) [IsIso f] {X': A} (hX': (F ⋙ G).obj X' = X) : + (F ⋙ G).obj (liftObj IF IG f hX') = Y := by + simp [liftObj] + +def comp.liftIso {X Y: C} (f: X ⟶ Y) [IsIso f] {X': A} (hX': (F ⋙ G).obj X' = X) : + X' ⟶ comp.liftObj IF IG f hX' := + let f1 := IG.liftIso (X' := F.obj X') f (by simp at hX'; assumption) + IF.liftIso (X' := X') f1 rfl + +lemma comp.isHomLift {X Y: C} (f: X ⟶ Y) [IsIso f] {X': A} (hX': (F ⋙ G).obj X' = X) : + (F ⋙ G).IsHomLift f (comp.liftIso IF IG f hX') := by + apply IsHomLift.of_fac + · let e := ClovenIsofibration.map_liftIso' (F := F) + simp only [comp_obj, liftIso, comp_map, e, eqToHom_refl, Category.id_comp, map_comp, + map_liftIso', eqToHom_map, Category.assoc, eqToHom_trans, eqToHom_trans_assoc] + rw![liftObj] + simp + · assumption + · simp [liftObj,ClovenIsofibration.obj_liftObj] + +/-- `IsMultiplicative` 1/2 -/ +@[simps!] +def comp : ClovenIsofibration (F ⋙ G) where + liftObj := comp.liftObj IF IG + liftIso := comp.liftIso IF IG + isHomLift := comp.isHomLift IF IG + liftIso_IsIso := by + intro X Y f i1 X' hX' + simp [comp.liftIso] + apply liftIso_IsIso + +lemma comp.liftIso_comp_aux {X Y Z : C} (f : X ⟶ Y) [IsIso f] (g : Y ⟶ Z) [IsIso g] {X' : A} + (hX' : (F ⋙ G).obj X' = X) (Y' : A) (hY' : comp.liftObj IF IG f hX' = Y') : + G.obj (F.obj Y') = Y := by + subst hY'; simp [comp.liftObj] + +variable [IsSplit IF] [IsSplit IG] + +lemma comp.liftObj_id {X: C} {X': A} (hX': (F ⋙ G).obj X' = X): + comp.liftObj IF IG (𝟙 X) hX' = X' := by + simp [comp.liftObj,liftIso_id] + +lemma comp.liftIso_id {X : C} {X' : A} (hX' : (F ⋙ G).obj X' = X) : + comp.liftIso IF IG (𝟙 X) hX' = eqToHom (by simp[comp.liftObj_id]) := by + dsimp [comp.liftIso] + rw! (castMode := .all) [IsSplit.liftIso_id] + simp only [liftIso_eqToHom, ← heq_eq_eq, eqRec_heq_iff_heq] + apply HEq.trans (eqToHom_heq_id_dom _ _ _) (eqToHom_heq_id_dom _ _ _).symm + +lemma comp.liftObj_comp {X Y Z : C} (f : X ⟶ Y) [IsIso f] (g : Y ⟶ Z) [IsIso g] {X' : A} + (hX' : (F ⋙ G).obj X' = X) : + comp.liftObj IF IG (f ≫ g) hX' = + comp.liftObj (X' := comp.liftObj IF IG f hX') IF IG g + (by simp only[comp.obj_liftObj]) := by + simp only [liftObj, liftIso_comp, eqToHom_refl, Category.id_comp, IsSplit.liftObj_comp, + liftObj_eqToHom] + congr! + simp + +lemma comp.liftIso_comp {X Y Z : C} (f : X ⟶ Y) [IsIso f] (g : Y ⟶ Z) [IsIso g] {X' : A} + (hX' : (F ⋙ G).obj X' = X) (Y' : A) + (hY' : comp.liftObj IF IG f hX' = Y') : + comp.liftIso IF IG (f ≫ g) hX' = comp.liftIso IF IG f hX' ≫ eqToHom hY' ≫ + comp.liftIso IF IG g (by subst hY';simp[liftObj]) ≫ + eqToHom (by subst hY'; simp[comp.liftObj_comp]) := by + subst hY' + simp only [liftObj, liftIso] + rw! [IsSplit.liftIso_comp (I := IG) f g hX' rfl, eqToHom_refl, Category.id_comp] + simp only [IsSplit.liftIso_comp, eqToHom_refl, liftIso_eqToHom, eqToHom_trans, Category.id_comp, + Category.assoc] + congr 1 + simp only [← heq_eq_eq, heq_comp_eqToHom_iff, comp_eqToHom_heq_iff] + congr! + simp + +instance : IsSplit (comp IF IG) where + liftObj_id := by + intro X X' hX' + apply comp.liftObj_id + liftIso_id := by + intro X X' hX' + apply comp.liftIso_id + liftObj_comp := by + intro X Y Z f i1 g i2 X' hX' Y' hY' + subst hY' + apply comp.liftObj_comp + liftIso_comp := by + intro X Y Z f i1 g i2 X' hX' Y' hY' + apply comp.liftIso_comp + +section isoComp + +@[simps] +def ofEq (F' : A ⥤ B) (hF' : F = F') : ClovenIsofibration F' where + liftObj f hf a ha := IF.liftObj f (by convert ha) + liftIso f hf a ha := IF.liftIso f (by convert ha) + isHomLift f hf a ha := by + subst hF' + apply IF.isHomLift + liftIso_IsIso := by + subst hF' + exact IF.liftIso_IsIso + +instance (F' : A ⥤ B) (hF' : F = F') : (ofEq IF F' hF').IsSplit := by + subst hF' + exact inferInstanceAs IF.IsSplit + +variable {A' : Type u₁} [Category.{v₁} A'] + (i : A' ≅≅ A) (F' : A' ⥤ B) (hF' : F' = i.hom ⋙ F) + +def isoComp : ClovenIsofibration F' := + ofEq (comp (iso ..) IF) F' hF'.symm + +instance : IsSplit (isoComp IF i F' hF') := + inferInstanceAs (ofEq ..).IsSplit + +end isoComp + +end + +def ofIsPullback {A B A' B' : Type u} [Groupoid.{v} A] [Groupoid.{v} B] [Groupoid.{v} A'] + [Groupoid.{v} B'] (top : A' ⥤ A) (F' : A' ⥤ B') (F : A ⥤ B) (bot : B' ⥤ B) + (isPullback : Functor.IsPullback top F' F bot) (IF : ClovenIsofibration F) [IsSplit IF] : + ClovenIsofibration F' := + let i : Functor.Groupoidal IF.classifier ≅≅ A := + Functor.ClovenIsofibration.grothendieckClassifierIso .. + have i_comp_F : i.hom ⋙ F = Groupoidal.forget := by + simp [i, grothendieckClassifierIso.hom_comp_self] + have eq1 : Groupoidal.pre IF.classifier bot ⋙ Groupoidal.forget = Groupoidal.forget ⋙ bot := by + simp [Groupoidal.pre_comp_forget] + have q1 : Functor.IsPullback (Groupoidal.pre IF.classifier bot ⋙ i.hom) + (Groupoidal.forget (F := (bot ⋙ IF.classifier))) F bot := + Functor.IsPullback.Paste.horiz eq1 (by simp [i_comp_F]) + (Functor.IsPullback.ofBotId i_comp_F.symm) + (Groupoidal.pre_isPullback ..) + let j : A' ≅≅ Functor.Groupoidal (F := bot ⋙ IF.classifier) := + Functor.IsPullback.isoIsPullback isPullback q1 + have e : F' = j.hom ⋙ (Groupoidal.forget (F := bot ⋙ IF.classifier)) := + (IsPullback.isoIsPullback.hom_comp_right isPullback q1 (hom := j.hom) (by simp[j])).symm + isoComp (Functor.ClovenIsofibration.forget ..) j _ e + +instance {A B A' B' : Type u} [Groupoid.{v} A] [Groupoid.{v} B] [Groupoid.{v} A'] + [Groupoid.{v} B'] (top : A' ⥤ A) (F' : A' ⥤ B') (F : A ⥤ B) (bot : B' ⥤ B) + (isPullback : Functor.IsPullback top F' F bot) (IF : ClovenIsofibration F) [IsSplit IF] : + IsSplit (ofIsPullback top F' F bot isPullback IF) := by + dsimp [ofIsPullback] + infer_instance + +section pushforward + +open CategoryTheory.Functor.Groupoidal GroupoidModel.FunctorOperation.pi.Over + +variable {C B A : Type u} [Groupoid.{u} C] [Groupoid.{u} B] [Groupoid.{u} A] {F : B ⥤ A} + (IF : ClovenIsofibration F) [IsSplit IF] (G : C ⥤ B) + +def pushforward.strictify : C ⥤ ∫ IF.classifier := + G ⋙ IF.grothendieckClassifierIso.inv + +@[simp] +lemma pushforward.strictify_comp_grothendieckClassifierIso_hom : + strictify IF G ⋙ IF.grothendieckClassifierIso.hom = G := by + simp [strictify, Functor.assoc] + +variable {G} (IG : ClovenIsofibration G) [IsSplit IG] + +def pushforward.strictifyClovenIsofibration : (strictify IF G).ClovenIsofibration := + ClovenIsofibration.comp IG (Functor.ClovenIsofibration.iso_inv ..) + +instance : (pushforward.strictifyClovenIsofibration IF IG).IsSplit := by + simp[pushforward.strictifyClovenIsofibration] + have h: (iso_inv IF.grothendieckClassifierIso).IsSplit := by + apply Functor.ClovenIsofibration.instIsSplitIso + apply CategoryTheory.Functor.ClovenIsofibration.instIsSplitComp + +/-- The object part (a groupoid) of the pushforward along `F`, of `G`, +defined as the Grothendieck construction applied to (unstructured) Pi-type construction +in the HoTTLean groupoid model. -/ +abbrev pushforward := ∫ GroupoidModel.FunctorOperation.pi (IF.classifier) + (pushforward.strictifyClovenIsofibration IF IG).classifier + +/-- `∫ σ.hom ⋙ hF.splitIsofibration.classifier` is the pullback of `F` along `σ`, +`∫ (splitIsofibration_strictify hF hG).classifier` is isomorphic to `G`. +So up to isomorphism this is the hom set bijection we want. -/ +@[simps] +def pushforward.homEquivAux1 {D : Type u} [Groupoid.{u} D] (σ : D ⥤ A) : + {M : D ⥤ pushforward IF IG // M ⋙ Groupoidal.forget = σ} ≃ + {N : ∫ σ ⋙ IF.classifier ⥤ ∫ (strictifyClovenIsofibration IF IG).classifier // + N ⋙ Functor.Groupoidal.forget = pre IF.classifier σ } where + toFun M := ⟨equivFun _ M.1 M.2, equivFun_comp_forget ..⟩ + invFun N := ⟨(equivInv (strictifyClovenIsofibration IF IG).classifier N.1 N.2), + equivInv_comp_forget (strictifyClovenIsofibration IF IG).classifier N.1 N.2⟩ + left_inv _ := by + ext + simp [equivInv_equivFun] + right_inv _ := by + ext + simp [equivFun_equivInv] + +@[simps!] +def pushforward.homEquivAux2 {D : Type u} [Groupoid.{u} D] (σ : D ⥤ A) : + {M : ∫ σ ⋙ IF.classifier ⥤ ∫ (strictifyClovenIsofibration IF IG).classifier // + M ⋙ Functor.Groupoidal.forget = pre IF.classifier σ } ≃ + {N : ∫ σ ⋙ IF.classifier ⥤ C // + N ⋙ G = pre IF.classifier σ ⋙ IF.grothendieckClassifierIso.hom } where + toFun M := ⟨(M.1 ⋙ ((strictifyClovenIsofibration IF IG)).grothendieckClassifierIso.hom), + by + conv => lhs ; rhs ; rw [← strictify_comp_grothendieckClassifierIso_hom IF G] + rw [Functor.assoc] + slice_lhs 2 3 => rw [← Functor.assoc, grothendieckClassifierIso.hom_comp_self] + slice_rhs 1 2 => rw [← M.2] + rw [Functor.assoc] ⟩ + invFun N := ⟨N.1 ⋙ ((strictifyClovenIsofibration IF IG)).grothendieckClassifierIso.inv, + by + dsimp [strictify] + rw [Functor.assoc, grothendieckClassifierIso.inv_comp_forget, ← Functor.assoc, N.2, + Functor.assoc, Iso.hom_inv_id', Functor.comp_id] ⟩ + left_inv := by + simp only [Function.LeftInverse, Subtype.forall, Subtype.mk.injEq] + intro a h + simp[Functor.assoc] + right_inv := by + simp[Function.RightInverse] + intro a + simp[Functor.assoc] + +open GroupoidModel.FunctorOperation.pi in +/-- The universal property of the pushforward, expressed as a (natural) bijection of hom sets. -/ +def pushforward.homEquiv {D : Type u} [Groupoid.{u} D] (σ : D ⥤ A) : + {M : D ⥤ pushforward IF IG // M ⋙ Groupoidal.forget = σ} ≃ + {N : ∫ σ ⋙ IF.classifier ⥤ C // + N ⋙ G = pre IF.classifier σ ⋙ IF.grothendieckClassifierIso.hom} := + calc {M : D ⥤ pushforward IF IG // M ⋙ Groupoidal.forget = σ} + _ ≃ {N : ∫ σ ⋙ IF.classifier ⥤ ∫ (strictifyClovenIsofibration IF IG).classifier // + N ⋙ Functor.Groupoidal.forget = pre IF.classifier σ } := + pushforward.homEquivAux1 .. + _ ≃ {N : ∫ σ ⋙ IF.classifier ⥤ C // + N ⋙ G = pre IF.classifier σ ⋙ IF.grothendieckClassifierIso.hom } := + pushforward.homEquivAux2 .. + +lemma pushforward.homEquiv_apply_coe {D : Type u} [Groupoid.{u} D] (σ : D ⥤ A) + (M : {M : D ⥤ pushforward IF IG // M ⋙ Groupoidal.forget = σ}) : + ((pushforward.homEquiv IF IG σ) M).1 = + equivFun (strictifyClovenIsofibration IF IG).classifier M M.2 ⋙ + (strictifyClovenIsofibration IF IG).grothendieckClassifierIso.hom := by + simp[pushforward.homEquiv] + simp[homEquivAux1] + simp[Trans.trans] + simp[homEquivAux2] + +/-- Naturality in the universal property of the pushforward. -/ +lemma pushforward.homEquiv_comp {D D' : Type u} [Groupoid.{u} D] [Groupoid.{u} D'] + (σ : D ⥤ A) (σ' : D' ⥤ A) (s : D' ⥤ D) (eq : σ' = s ⋙ σ) + (M : D ⥤ pushforward IF IG) (hM : M ⋙ Groupoidal.forget = σ) : + (pushforward.homEquiv IF IG σ' ⟨s ⋙ M, by rw [Functor.assoc, hM, eq]⟩).1 = + Groupoidal.map (eqToHom (by rw [eq, Functor.assoc])) ⋙ + pre _ s ⋙ (pushforward.homEquiv IF IG σ ⟨M, hM⟩).1 := by + subst eq + rw [pushforward.homEquiv_apply_coe, pushforward.homEquiv_apply_coe] + simp [← Functor.assoc, Functor.simpIdComp, equivFun_comp (hF:= hM), Groupoidal.map_id_eq] + +end pushforward + +def toDiscretePUnit + {X : Type*} [Category X] (F : X ⥤ Discrete.{u} PUnit) : Functor.ClovenIsofibration F where + liftObj {y1 y2} g i x e := x + liftIso {y1 y2} g i x e := 𝟙 x + isHomLift {y1 y2} g i x e := by + apply IsHomLift.of_fac _ _ _ + any_goals apply Discrete.ext + any_goals apply PUnit.ext + rfl + liftIso_IsIso {y1 y2} g i x e := CategoryTheory.IsIso.id .. + +instance toDiscretePUnit.IsSplit {X : Type*} [Category X] (F : X ⥤ Discrete.{u} PUnit) : + Functor.ClovenIsofibration.IsSplit (toDiscretePUnit F) where + liftObj_id := by simp[toDiscretePUnit] + liftIso_id := by simp[toDiscretePUnit] + liftObj_comp {y1 y2 y3} f hf g hg x1 hx1 x2 hx2 := by + subst hx2 + simp[toDiscretePUnit] + liftIso_comp {y1 y2 y3} f hf g hg x1 hx1 x2 hx2 := by + subst hx2 + simp[toDiscretePUnit] + +end ClovenIsofibration +end +end Functor +end CategoryTheory + +namespace GroupoidModel + +open CategoryTheory Functor.ClovenIsofibration + +def tpClovenIsofibration : (GroupoidModel.U.{u}.tp).ClovenIsofibration := + let i : U.{u}.Tm ≅≅ Functor.Groupoidal (F := Core.inclusion _ ⋙ AsSmall.down) := + Functor.IsPullback.isoIsPullback IsPullback.isPullbackCoreAsSmall' + (Functor.Groupoidal.isPullback (Core.inclusion _ ⋙ AsSmall.down)) + isoComp (Functor.ClovenIsofibration.forget _) i + _ (Functor.IsPullback.isoIsPullback.hom_comp_right _ _ rfl).symm + +instance : IsSplit tpClovenIsofibration := by + dsimp [tpClovenIsofibration] + infer_instance + +end GroupoidModel diff --git a/HoTTLean/ForMathlib/CategoryTheory/Comma/Over/Pushforward.lean b/HoTTLean/ForMathlib/CategoryTheory/Comma/Over/Pushforward.lean new file mode 100644 index 00000000..16f2fcc2 --- /dev/null +++ b/HoTTLean/ForMathlib/CategoryTheory/Comma/Over/Pushforward.lean @@ -0,0 +1,73 @@ +/- +Copyright (c) 2025 Joseph Hua. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Joseph Hua +-/ + +import Mathlib.CategoryTheory.Comma.Over.Pullback +import Mathlib.CategoryTheory.Adjunction.PartialAdjoint +import Mathlib.CategoryTheory.Limits.FunctorCategory.Basic + +noncomputable section + +universe v v₂ u u₂ + +namespace CategoryTheory + +open Category Limits Comonad + +variable {C : Type u} [Category.{v} C] (X : C) + +variable {S S' : C} (f : S ⟶ S') [inst_hasPullback : ∀ {W} (h : W ⟶ S'), HasPullback h f] + +/-- `Y` is the pushforward of `X` along `f` when it represents the presheaf +`Hom(pullback f (-), X)`. This expresses the universal property of the right adjoint to +pullback without requiring the existence of the entire adjoint. +See `Mathlib.CategoryTheory.Adjunction.PartialAdjoint`. -/ +abbrev IsPushforward (X : Over S) (Y : Over S') := + ((Over.pullback f).op ⋙ yoneda.obj X).RepresentableBy Y + +/-- An object `X` in the slice over `S` has a pushforward along morphism `f : S ⟶ S'` +when the partial right adjoint of pullback along `f` is well-defined on the object `X`. +This definition could be generalised to not require pullbacks, but such settings are rare. +-/ +abbrev HasPushforward (X : Over S) : Prop := + ((Over.pullback f).op ⋙ yoneda.obj X).IsRepresentable + +/-- Assuming the partial right adjoint of pullback along `f` is well-defined on `X`, +choose the image of `X` under the partial right adjoint. -/ +abbrev pushforward (X : Over S) [HasPushforward f X] : Over S' := + ((Over.pullback f).op ⋙ yoneda.obj X).reprX + +/-- The pushforward of an object satisfies the universal property of the pushforward. -/ +def pushforward.isPushforward (X : Over S) [HasPushforward f X] : + IsPushforward f X (pushforward f X) := + ((Over.pullback f).op ⋙ yoneda.obj X).representableBy + +/-- A morphism `f` has pushforwards (also called exponentiable) when there is a pushforward +along `f` for any map into its domain. -/ +abbrev HasPushforwardsAlong : Prop := ∀ (X : Over S), HasPushforward f X + +-- namespace Over + +-- variable [HasPushforwardsAlong f] + +-- lemma pullback_rightAdjointObjIsDefined_eq_top : +-- (Over.pullback f).rightAdjointObjIsDefined = ⊤ := by aesop_cat + +-- instance : (pullback f).IsLeftAdjoint := +-- Functor.isLeftAdjoint_of_rightAdjointObjIsDefined_eq_top +-- (pullback_rightAdjointObjIsDefined_eq_top f) + +-- /-- The left adjoint of pullback. -/ +-- def pushforward : Over S ⥤ Over S' := +-- (pullback f).rightAdjoint + +-- /-- The pullback-pushforward adjunction. -/ +-- def pullbackPushforwardAdjunction : pullback f ⊣ pushforward f := +-- Adjunction.ofIsLeftAdjoint (pullback f) + +-- end Over + +end CategoryTheory +end diff --git a/HoTTLean/ForMathlib/CategoryTheory/Comma/Presheaf/Basic.lean b/HoTTLean/ForMathlib/CategoryTheory/Comma/Presheaf/Basic.lean new file mode 100644 index 00000000..8b961679 --- /dev/null +++ b/HoTTLean/ForMathlib/CategoryTheory/Comma/Presheaf/Basic.lean @@ -0,0 +1,203 @@ +import Mathlib.CategoryTheory.Comma.Presheaf.Basic +import Mathlib.Tactic.DepRewrite +import HoTTLean.ForMathlib +import HoTTLean.ForMathlib.CategoryTheory.Adjunction.Basic +import HoTTLean.ForMathlib.CategoryTheory.Yoneda + +namespace CategoryTheory + +open Category Opposite + +universe w v u u₁ + +section + +attribute [local simp] CategoryTheory.Yoneda.fullyFaithful_preimage + +namespace costructuredArrowYonedaEquivOver + +variable {C : Type u} [Category.{v} C] {A : C} + +@[simps!] +def functor : CostructuredArrow yoneda (yoneda.obj A) ⥤ Over A where + obj X := Over.mk ((CategoryTheory.Yoneda.fullyFaithful).preimage X.hom) + map {X Y} f := Over.homMk f.left (by + have e : (yoneda.map f.left ≫ Y.hom).app (op X.left) (𝟙 X.left) = + (X.hom ≫ (Functor.fromPUnit (yoneda.obj A)).map f.right).app + (op X.left) (𝟙 X.left) := by simp [f.w] + simp [- CommaMorphism.w] at e + simpa) + +@[simps!] +def inverse : Over A ⥤ CostructuredArrow yoneda (yoneda.obj A) where + obj X := CostructuredArrow.mk (yoneda.map X.hom) + map {X Y} f := CostructuredArrow.homMk f.left + +@[simps!] +def unitIso : 𝟭 (CostructuredArrow yoneda (yoneda.obj A)) ≅ functor ⋙ inverse := + NatIso.ofComponents (fun X => Comma.isoMk (Iso.refl _) (Iso.refl _) + (by cat_disch)) + +@[simps!] +def counitIso : inverse ⋙ functor (A := A) ≅ 𝟭 _ := + NatIso.ofComponents (fun X => Over.isoMk (Iso.refl _)) + +end costructuredArrowYonedaEquivOver + +open costructuredArrowYonedaEquivOver + +variable {C : Type u} [Category.{v} C] {A : C} + +@[simps] +def costructuredArrowYonedaEquivOver : + CostructuredArrow yoneda (yoneda.obj A) ≌ CategoryTheory.Over A where + functor := functor + inverse := inverse + unitIso := unitIso + counitIso := counitIso + +def costructuredArrowYonedaEquivOver.inverseCompToOverIso : + inverse ⋙ CostructuredArrow.toOver yoneda (yoneda.obj A) ≅ Over.post yoneda := + Iso.refl _ + +def overYonedaEquivPresheafOver : + CategoryTheory.Over (yoneda.obj A) ≌ ((CategoryTheory.Over A)ᵒᵖ ⥤ Type v) := + (overEquivPresheafCostructuredArrow (yoneda.obj A)).trans + costructuredArrowYonedaEquivOver.op.congrLeft + +def overYonedaEquivPresheafOver.functorObjMkYonedaIso (B : Over A) : + overYonedaEquivPresheafOver.functor.obj (Over.mk (yoneda.map B.hom)) ≅ yoneda.obj B := + calc overYonedaEquivPresheafOver.functor.obj (Over.mk (yoneda.map B.hom)) + _ ≅ _ := Functor.isoWhiskerLeft inverse.op <| + (CostructuredArrow.toOverCompOverEquivPresheafCostructuredArrow (yoneda.obj A)).app + (.mk (yoneda.map B.hom)) + _ ≅ yoneda.obj B := NatIso.ofComponents (fun X => + costructuredArrowYonedaEquivOver.fullyFaithfulInverse.homEquiv.symm.toIso) + (fun {X Y} f => by + ext a + simp only [Equiv.toIso_hom, types_comp_apply] + erw [Functor.FullyFaithful.homEquiv_symm_apply, Functor.FullyFaithful.homEquiv_symm_apply] + simp) + +def overYonedaEquivPresheafOver.yonedaObjFunctorObjIso (X : Over y(A)) : + y(overYonedaEquivPresheafOver.functor.obj X) ≅ + overYonedaEquivPresheafOver.inverse.op ⋙ yoneda.obj X := + (overYonedaEquivPresheafOver.symm.toAdjunction.representableBy X).toIso + +def overYonedaEquivPresheafOver.postYonedaCompFunctorIso : + Over.post yoneda ⋙ (overYonedaEquivPresheafOver (A := A)).functor ≅ yoneda := + calc _ + _ ≅ (inverse ⋙ CostructuredArrow.toOver yoneda (yoneda.obj A)) ⋙ + (overYonedaEquivPresheafOver (A := A)).functor := + Functor.isoWhiskerRight inverseCompToOverIso _ + _ ≅ ((inverse ⋙ CostructuredArrow.toOver yoneda (yoneda.obj A)) ⋙ + (overEquivPresheafCostructuredArrow y(A)).functor) ⋙ + costructuredArrowYonedaEquivOver.op.congrLeft.functor := + (Functor.associator ..).symm + _ ≅ (inverse ⋙ (CostructuredArrow.toOver yoneda (yoneda.obj A)) ⋙ + (overEquivPresheafCostructuredArrow y(A)).functor) ⋙ + costructuredArrowYonedaEquivOver.op.congrLeft.functor := + Functor.isoWhiskerRight (Functor.associator ..) _ + _ ≅ (inverse ⋙ yoneda) ⋙ costructuredArrowYonedaEquivOver.op.congrLeft.functor := + Functor.isoWhiskerRight (Functor.isoWhiskerLeft _ + (CostructuredArrow.toOverCompOverEquivPresheafCostructuredArrow ..)) _ + _ ≅ inverse ⋙ yoneda ⋙ costructuredArrowYonedaEquivOver.op.congrLeft.functor := + Functor.associator .. + _ ≅ inverse ⋙ functor ⋙ yoneda := + Functor.isoWhiskerLeft _ costructuredArrowYonedaEquivOver.yonedaCompCongrLeftFunctorIso + _ ≅ 𝟭 _ ⋙ yoneda := + (Functor.associator ..).symm ≪≫ Functor.isoWhiskerRight counitIso _ + _ ≅ yoneda := + yoneda.leftUnitor + +def overYonedaEquivPresheafOver.yonedaCompInverseIso : + yoneda ⋙ (overYonedaEquivPresheafOver (A := A)).inverse ≅ Over.post yoneda := + (overYonedaEquivPresheafOver.isoCompInverse postYonedaCompFunctorIso).symm + +end + +section + +variable {C : Type u} [SmallCategory C] {A : C} {D : Type*} [Category D] + +open overYonedaEquivPresheafOver + +/- +noncomputable def Over.yonedaIsoMk {X Y : Over (yoneda.obj A)} + (α : (post yoneda).op ⋙ y(X) ≅ (post yoneda).op ⋙ y(Y)) : + X ≅ Y := + let β (X) : yoneda.op ⋙ y(overYonedaEquivPresheafOver.functor.obj X) ≅ + (Over.post yoneda).op ⋙ yoneda.obj X := + calc yoneda.op ⋙ y(overYonedaEquivPresheafOver.functor.obj X) + _ ≅ yoneda.op ⋙ overYonedaEquivPresheafOver.inverse.op ⋙ yoneda.obj X := + yoneda.op.isoWhiskerLeft (yonedaObjFunctorObjIso X) + _ ≅ (yoneda.op ⋙ overYonedaEquivPresheafOver.inverse.op) ⋙ yoneda.obj X := + (Functor.associator ..).symm + _ ≅ (yoneda ⋙ overYonedaEquivPresheafOver.inverse).op ⋙ yoneda.obj X := + Functor.isoWhiskerRight (Functor.opComp ..).symm _ + _ ≅ (Over.post yoneda).op ⋙ yoneda.obj X := + Functor.isoWhiskerRight (NatIso.op yonedaCompInverseIso.symm) _ + overYonedaEquivPresheafOver.functor.preimageIso + (NatIso.yonedaMk (β X ≪≫ α ≪≫ (β Y).symm)) +-/ + +/-- The natural hom-set bijection as an isomorphism of profunctors +``` + Psh(Over A) (y(-), overYonedaEquivPresheafOver.functor (⋆)) ≅ + Over (y(A)) (yoneda ⋙ inverse (-), ⋆) ≅ + Over (y(A)) (Over.post yoneda (-), ⋆) +``` +-/ +def overYonedaEquivPresheafOver.homIso : overYonedaEquivPresheafOver.functor ⋙ yoneda ⋙ + (Functor.whiskeringLeft (Over A)ᵒᵖ ((Over A)ᵒᵖ ⥤ Type u)ᵒᵖ (Type u)).obj yoneda.op ≅ + yoneda ⋙ (Functor.whiskeringLeft _ _ _).obj (Over.post yoneda).op := + calc overYonedaEquivPresheafOver.functor ⋙ yoneda ⋙ + (Functor.whiskeringLeft _ _ _).obj yoneda.op + -- `Psh(Over A) (y(-), functor (⋆))` + _ ≅ (overYonedaEquivPresheafOver.functor ⋙ yoneda) ⋙ + (Functor.whiskeringLeft _ _ _).obj yoneda.op := + (Functor.associator ..).symm + -- `Over (y(A)) (yoneda ⋙ inverse (-), ⋆)` + _ ≅ (yoneda ⋙ (Functor.whiskeringLeft _ _ _).obj overYonedaEquivPresheafOver.inverse.op) ⋙ + (Functor.whiskeringLeft _ _ _).obj yoneda.op := + Functor.isoWhiskerRight overYonedaEquivPresheafOver.symm.toAdjunction.homIso.symm _ + _ ≅ yoneda ⋙ (Functor.whiskeringLeft _ _ _).obj overYonedaEquivPresheafOver.inverse.op ⋙ + (Functor.whiskeringLeft _ _ _).obj yoneda.op := + Functor.associator .. + _ ≅ yoneda ⋙ (Functor.whiskeringLeft _ _ _).obj + (yoneda.op ⋙ overYonedaEquivPresheafOver.inverse.op) := + Functor.isoWhiskerLeft _ (Functor.whiskeringLeftObjCompIso ..).symm + _ ≅ yoneda ⋙ (Functor.whiskeringLeft _ _ _).obj + (yoneda ⋙ overYonedaEquivPresheafOver.inverse).op := + Functor.isoWhiskerLeft _ (Functor.mapIso _ (Functor.opComp ..).symm) + -- `Over (y(A)) (Over.post yoneda (-), ⋆)` + _ ≅ yoneda ⋙ (Functor.whiskeringLeft _ _ _).obj (Over.post yoneda).op := + Functor.isoWhiskerLeft _ (Functor.mapIso _ + (NatIso.op overYonedaEquivPresheafOver.yonedaCompInverseIso.symm)) + +/-- To show that `F ≅ G : D ⥤ Over y(A)` +it suffices to show the natural isomorphism of profunctors +`Over (y(A)) (Over.post yoneda (-), F(⋆)) ≅ Over (y(A)) (Over.post yoneda (-), G(⋆))` -/ +def Over.yonedaNatIsoMk {F G : D ⥤ Over (yoneda.obj A)} + (α : F ⋙ yoneda ⋙ (Functor.whiskeringLeft _ _ _).obj (Over.post yoneda).op ≅ + G ⋙ yoneda ⋙ (Functor.whiskeringLeft _ _ _).obj (Over.post yoneda).op) : + F ≅ G := + -- `Psh(Over A) (y(-), F ⋙ functor (⋆)) ≅ Over (y(A)) (Over.post yoneda (-), F(⋆))` + let β (F) : (F ⋙ (overYonedaEquivPresheafOver).functor) ⋙ + yoneda ⋙ (Functor.whiskeringLeft _ _ _).obj yoneda.op ≅ + F ⋙ yoneda ⋙ (Functor.whiskeringLeft _ _ _).obj (Over.post yoneda).op := + (Functor.associator ..).symm ≪≫ Functor.isoWhiskerLeft F overYonedaEquivPresheafOver.homIso + -- to show `F ≅ G : D ⥤ Over (yoneda.obj A)` + (overYonedaEquivPresheafOver.fullyFaithfulFunctor.whiskeringRight _).preimageIso + -- it suffices to compose with the equivalence + -- `overYonedaEquivPresheafOver : Over (y(A)) ≌ Psh (Over A)` and show + -- `F ⋙ overYonedaEquivPresheafOver.functor ≅ G ⋙ overYonedaEquivPresheafOver.functor` + (functorToPresheafIsoMk (β F ≪≫ α ≪≫ (β G).symm)) + -- an isomorphism `F ⋙ functor ≅ G ⋙ functor : Psh C` amounts to + -- an isomorphism `Psh(Over A) (y(-), F ⋙ functor (⋆)) ≅ Psh(Over A) (y(-), G ⋙ functor (⋆))` + -- amounts to + -- an isomorphism `Over (y(A)) (Over.post yoneda (-), F(⋆)) ≅ Over (y(A)) (Over.post yoneda (-), G(⋆))` + +end + +end CategoryTheory diff --git a/HoTTLean/ForMathlib/CategoryTheory/Functor/FullyFaithful.lean b/HoTTLean/ForMathlib/CategoryTheory/Functor/FullyFaithful.lean new file mode 100644 index 00000000..3c415bce --- /dev/null +++ b/HoTTLean/ForMathlib/CategoryTheory/Functor/FullyFaithful.lean @@ -0,0 +1,16 @@ +import Mathlib.CategoryTheory.Functor.FullyFaithful +import Mathlib.CategoryTheory.Yoneda + +universe v₁ v₂ u₁ u₂ + +namespace CategoryTheory +namespace Functor +namespace FullyFaithful + +variable {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₁} D] + +variable {F : C ⥤ D} (hF : F.FullyFaithful) + +/-- The natural isomorphism of hom-sets `C(-,⋆) ≅ D(F(-),F(⋆))`. -/ +def homIso : yoneda ≅ F ⋙ yoneda ⋙ (Functor.whiskeringLeft _ _ _).obj F.op := + NatIso.ofComponents (fun X => NatIso.ofComponents (fun Y => hF.homEquiv.toIso)) diff --git a/HoTTLean/ForMathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean b/HoTTLean/ForMathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean new file mode 100644 index 00000000..289f5fe1 --- /dev/null +++ b/HoTTLean/ForMathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean @@ -0,0 +1,16 @@ +import Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback +import Mathlib.CategoryTheory.Limits.Shapes.Pullback.CommSq + +noncomputable section + +open CategoryTheory + +universe w v₁ v₂ v u u₂ + +namespace CategoryTheory.Limits + +variable {C : Type u} [Category.{v} C] {W X Y Z : C} + +instance {X : C} : HasPullbacksAlong (𝟙 X) := by + intro W h + exact IsPullback.hasPullback (IsPullback.id_horiz h) diff --git a/HoTTLean/ForMathlib/CategoryTheory/MorphismProperty/Limits.lean b/HoTTLean/ForMathlib/CategoryTheory/MorphismProperty/Limits.lean new file mode 100644 index 00000000..7a6210e5 --- /dev/null +++ b/HoTTLean/ForMathlib/CategoryTheory/MorphismProperty/Limits.lean @@ -0,0 +1,82 @@ +/- +Copyright (c) 2022 Andrew Yang. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Andrew Yang, Joël Riou +-/ +import Mathlib.CategoryTheory.MorphismProperty.Limits + +/-! +# Relation of morphism properties with limits + +The following predicates are introduces for morphism properties `P`: +* `IsStableUnderBaseChange`: `P` is stable under base change if in all pullback + squares, the left map satisfies `P` if the right map satisfies it. +* `IsStableUnderCobaseChange`: `P` is stable under cobase change if in all pushout + squares, the right map satisfies `P` if the left map satisfies it. + +We define `P.universally` for the class of morphisms which satisfy `P` after any base change. + +We also introduce properties `IsStableUnderProductsOfShape`, `IsStableUnderLimitsOfShape`, +`IsStableUnderFiniteProducts`, and similar properties for colimits and coproducts. + +-/ + +universe w w' v u + +namespace CategoryTheory + +open Category Limits + +namespace MorphismProperty + +variable {C : Type u} [Category.{v} C] + +section + +variable (P : MorphismProperty C) + +/-- `P.HasPullbacksAlong f` states that for any morphism satifying `P` with the same codomain +as `f`, the pullback of that morphism along `f` exists. -/ +protected class HasPullbacksAlong {X Y : C} (f : X ⟶ Y) : Prop where + hasPullback {W} (g : W ⟶ Y) : P g → HasPullback g f + +instance {X Y : C} (f : X ⟶ Y) [HasPullbacksAlong f] : P.HasPullbacksAlong f where + hasPullback := inferInstance + +variable {P} + +theorem baseChange_map' [IsStableUnderBaseChange P] {S S' X Y : C} (f : S' ⟶ S) + {v₁₂ : X ⟶ S} {v₂₂ : Y ⟶ S} {g : X ⟶ Y} (hv₁₂ : v₁₂ = g ≫ v₂₂) [HasPullback v₁₂ f] + [HasPullback v₂₂ f] (H : P g) : P (pullback.lift (f := v₂₂) (g := f) (pullback.fst v₁₂ f ≫ g) + (pullback.snd v₁₂ f) (by simp [pullback.condition, ← hv₁₂])) := by + subst hv₁₂ + refine of_isPullback (f' := pullback.fst (g ≫ v₂₂) f) + (f := pullback.fst v₂₂ f) ?_ H + refine IsPullback.of_bot ?_ (by simp) (IsPullback.of_hasPullback v₂₂ f) + simpa using IsPullback.of_hasPullback (g ≫ v₂₂) f + +local instance {S X Y : C} {f : X ⟶ S} [HasPullbacksAlong f] {g : Y ⟶ S} : + HasPullback f g := hasPullback_symmetry g f + +instance [P.HasPullbacks] {X Y : C} {f : X ⟶ Y} : P.HasPullbacksAlong f where + hasPullback _ := hasPullback _ + +instance [P.IsStableUnderBaseChange] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) + [P.HasPullbacksAlong f] [P.HasPullbacksAlong g] : P.HasPullbacksAlong (f ≫ g) where + hasPullback h p := + have : HasPullback h g := HasPullbacksAlong.hasPullback h p + have : HasPullback (pullback.snd h g) f := HasPullbacksAlong.hasPullback (pullback.snd h g) + (P.pullback_snd h g p) + IsPullback.hasPullback (IsPullback.paste_horiz (IsPullback.of_hasPullback + (pullback.snd h g) f) (IsPullback.of_hasPullback h g)) + +/-- A morphism property satisfies `HasObjects` when any map `! : X ⟶ Y` to a terminal +object `Y` satisfies the morphism property. -/ +class HasObjects (P : MorphismProperty C) : Prop where + obj_mem {X Y} (f : X ⟶ Y) : Limits.IsTerminal Y → P f + +end + +end MorphismProperty + +end CategoryTheory diff --git a/HoTTLean/ForMathlib/CategoryTheory/MorphismProperty/OverAdjunction.lean b/HoTTLean/ForMathlib/CategoryTheory/MorphismProperty/OverAdjunction.lean new file mode 100644 index 00000000..50dbcd93 --- /dev/null +++ b/HoTTLean/ForMathlib/CategoryTheory/MorphismProperty/OverAdjunction.lean @@ -0,0 +1,495 @@ +/- +Copyright (c) 2024 Christian Merten. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Merten +-/ +import Mathlib.CategoryTheory.MorphismProperty.Comma +import HoTTLean.ForMathlib.CategoryTheory.MorphismProperty.Limits +import HoTTLean.ForMathlib.CategoryTheory.Comma.Over.Pushforward + +/-! +# Adjunction of pushforward and pullback in `P.Over Q X` + +Under suitable assumptions on `P`, `Q` and `f`, +a morphism `f : X ⟶ Y` defines two functors: + +- `Over.map`: post-composition with `f` +- `Over.pullback`: base-change along `f` + +such that `Over.map` is the left adjoint to `Over.pullback`. +-/ + +namespace CategoryTheory.MorphismProperty + +open Limits + +variable {T : Type*} [Category T] (P Q : MorphismProperty T) +variable {X Y Z : T} + +section Map + +lemma Over.forget_preimage {S} {X Y : P.Over ⊤ S} (g : X.toComma ⟶ Y.toComma) : + (Functor.FullyFaithful.ofFullyFaithful (Over.forget P ⊤ S)).preimage g = + Over.homMk g.left := by + simp [Functor.FullyFaithful.ofFullyFaithful] + apply (Over.forget P ⊤ S).map_injective + rw [Functor.map_preimage] + simp + +variable {P} [P.IsStableUnderComposition] [Q.IsMultiplicative] + +/-- If `P` is stable under composition and `f : X ⟶ Y` satisfies `P`, +this is the functor `P.Over Q X ⥤ P.Over Q Y` given by composing with `f`. -/ +@[simps! obj_left obj_hom map_left] +def Over.map {f : X ⟶ Y} (hPf : P f) : P.Over Q X ⥤ P.Over Q Y := + Comma.mapRight _ (Discrete.natTrans fun _ ↦ f) <| fun X ↦ P.comp_mem _ _ X.prop hPf + +lemma Over.map_comp {f : X ⟶ Y} (hf : P f) {g : Y ⟶ Z} (hg : P g) : + map Q (P.comp_mem f g hf hg) = map Q hf ⋙ map Q hg := by + fapply Functor.ext + · simp [map, Comma.mapRight, CategoryTheory.Comma.mapRight, Comma.lift] + · intro U V k + ext + simp + +/-- `Over.map` commutes with composition. -/ +@[simps! hom_app_left inv_app_left] +def Over.mapComp {f : X ⟶ Y} (hf : P f) {g : Y ⟶ Z} (hg : P g) [Q.RespectsIso] : + map Q (P.comp_mem f g hf hg) ≅ map Q hf ⋙ map Q hg := + NatIso.ofComponents (fun X ↦ Over.isoMk (Iso.refl _)) + +end Map + +section Pullback + +/-- A morphism property is `IsStableUnderBaseChangeAlong f` if the base change along `f` of such +a morphism still falls in the class. -/ +class IsStableUnderBaseChangeAlong {X S : T} (f : X ⟶ S) : Prop where + of_isPullback {Y Y' : T} {g : Y ⟶ S} {f' : Y' ⟶ Y} {g' : Y' ⟶ X} + (pb : IsPullback f' g' g f) (hg : P g) : P g' + +instance [P.IsStableUnderBaseChange] {X S : T} (f : X ⟶ S) : P.IsStableUnderBaseChangeAlong f where + of_isPullback := P.of_isPullback + +variable [Q.IsStableUnderBaseChange] [Q.IsMultiplicative] (f : X ⟶ Y) [P.HasPullbacksAlong f] + [P.IsStableUnderBaseChangeAlong f] + +instance (A : P.Over Q Y) : HasPullback A.hom f := + HasPullbacksAlong.hasPullback A.hom A.prop + +instance {X Y Z} (f : X ⟶ Y) (g : Y ⟶ Z) [P.HasPullbacksAlong f] + [P.IsStableUnderBaseChangeAlong g] [P.HasPullbacksAlong g] : P.HasPullbacksAlong (f ≫ g) where + hasPullback p hp := + have := HasPullbacksAlong.hasPullback (f := g) p hp + have right := IsPullback.of_hasPullback p g + have := HasPullbacksAlong.hasPullback (f := f) (pullback.snd p g) + (IsStableUnderBaseChangeAlong.of_isPullback right hp) + (IsPullback.paste_horiz (IsPullback.of_hasPullback (pullback.snd p g) f) right).hasPullback + +instance {X Y Z} (f : X ⟶ Y) (g : Y ⟶ Z) [P.IsStableUnderBaseChangeAlong f] + [P.IsStableUnderBaseChangeAlong g] [P.HasPullbacksAlong g] : + P.IsStableUnderBaseChangeAlong (f ≫ g) where + of_isPullback {_ _ p _ _} pb hp := + have := HasPullbacksAlong.hasPullback (f := g) p hp + have right := IsPullback.of_hasPullback p g + IsStableUnderBaseChangeAlong.of_isPullback (IsPullback.of_right' pb right) + (IsStableUnderBaseChangeAlong.of_isPullback right hp) + +instance {X Y Z} (f : X ⟶ Y) (g : Y ⟶ Z) [P.HasPullbacksAlong f] + [P.IsStableUnderBaseChangeAlong f] [P.HasPullbacksAlong g] [P.IsStableUnderBaseChangeAlong g] + (A : P.Over Q Z) : HasPullback (pullback.snd A.hom g) f := + HasPullbacksAlong.hasPullback (pullback.snd A.hom g) + (IsStableUnderBaseChangeAlong.of_isPullback (IsPullback.of_hasPullback A.hom g) A.prop) + +/-- If `P` and `Q` are stable under base change and pullbacks along `f` exist for morphisms in `P`, +this is the functor `P.Over Q Y ⥤ P.Over Q X` given by base change along `f`. -/ +@[simps! obj_left obj_hom map_left] +noncomputable def Over.pullback : + P.Over Q Y ⥤ P.Over Q X where + obj A := Over.mk Q (Limits.pullback.snd A.hom f) + (IsStableUnderBaseChangeAlong.of_isPullback (IsPullback.of_hasPullback A.hom f) A.prop) + map {A B} g := Over.homMk (pullback.lift (pullback.fst A.hom f ≫ g.left) + (pullback.snd A.hom f) (by simp [pullback.condition])) (by simp) + (baseChange_map' _ _ g.prop_hom_left) + +variable {P} {Q} (f : X ⟶ Y) [P.HasPullbacksAlong f] [P.IsStableUnderBaseChangeAlong f] + (g : Y ⟶ Z) [P.HasPullbacksAlong g] [P.IsStableUnderBaseChangeAlong g] + +/-- `Over.pullback` commutes with composition. -/ +@[simps! hom_app_left inv_app_left] +noncomputable def Over.pullbackComp [Q.RespectsIso] : + Over.pullback P Q (f ≫ g) ≅ + Over.pullback P Q g ⋙ Over.pullback P Q f := + NatIso.ofComponents + (fun X ↦ Over.isoMk ((pullbackLeftPullbackSndIso X.hom g f).symm) (by simp)) + +lemma Over.pullbackComp_left_fst_fst (A : P.Over Q Z) : + ((Over.pullbackComp f g).hom.app A).left ≫ pullback.fst (pullback.snd A.hom g) f ≫ + pullback.fst A.hom g = pullback.fst A.hom (f ≫ g) := by + simp + +variable {f} {g} + +/-- If `f = g`, then base change along `f` is naturally isomorphic to base change along `g`. -/ +@[simps!] +noncomputable def Over.pullbackCongr {g : X ⟶ Y} (h : f = g) : + have : P.HasPullbacksAlong g := by subst h; infer_instance + have : P.IsStableUnderBaseChangeAlong g := by subst h; infer_instance + Over.pullback P Q f ≅ Over.pullback P Q g := + have : P.HasPullbacksAlong g := by subst h; infer_instance + NatIso.ofComponents (fun _ ↦ Over.isoMk (pullback.congrHom rfl h)) + +end Pullback + +section Adjunction + +variable {P Q} [P.IsStableUnderComposition] [Q.IsMultiplicative] [Q.IsStableUnderBaseChange] + +/-- `P.Over.map` is left adjoint to `P.Over.pullback` if `f` satisfies `P` and `Q`. -/ +@[simps!] +noncomputable def Over.mapPullbackAdjHomEquiv (f : X ⟶ Y) [P.HasPullbacksAlong f] + [P.IsStableUnderBaseChangeAlong f] [Q.HasOfPostcompProperty Q] (hPf : P f) (hQf : Q f) + (A : P.Over Q X) (B : P.Over Q Y) : ((map Q hPf).obj A ⟶ B) ≃ (A ⟶ (pullback P Q f).obj B) := + { toFun g := Over.homMk (pullback.lift g.left A.hom <| by simp) (by simp) <| by + apply Q.of_postcomp (W' := Q) + · exact Q.pullback_fst B.hom f hQf + · simpa using g.prop_hom_left + invFun h := Over.homMk (h.left ≫ pullback.fst B.hom f) (by + simp only [map_obj_left, Functor.const_obj_obj, pullback_obj_left, Functor.id_obj, + Category.assoc, pullback.condition, map_obj_hom, ← pullback_obj_hom, Over.w_assoc]) + (Q.comp_mem _ _ h.prop_hom_left (Q.pullback_fst _ _ hQf)) + left_inv := by cat_disch + right_inv h := by + ext + dsimp + ext + · simp + · simpa using h.w.symm } + +/-- `P.Over.map` is left adjoint to `P.Over.pullback` if `f` satisfies `P` and `Q`. -/ +noncomputable def Over.mapPullbackAdj (f : X ⟶ Y) [P.HasPullbacksAlong f] + [P.IsStableUnderBaseChangeAlong f] [Q.HasOfPostcompProperty Q] (hPf : P f) (hQf : Q f) : + Over.map Q hPf ⊣ Over.pullback P Q f := + Adjunction.mkOfHomEquiv + { homEquiv A B := Over.mapPullbackAdjHomEquiv f hPf hQf A B } + +variable (f : X ⟶ Y) [P.HasPullbacksAlong f] [P.IsStableUnderBaseChangeAlong f] + [Q.HasOfPostcompProperty Q] (hPf : P f) (hQf : Q f) + (A : P.Over Q X) (B : P.Over Q Y) + +@[simp] +lemma Over.mapPullbackAdj_homEquiv_apply_left (g : (map Q hPf).obj A ⟶ B) : + ((Over.mapPullbackAdj f hPf hQf).homEquiv A B g).left = + pullback.lift g.left A.hom (by cat_disch) := by + simp [mapPullbackAdj] + +@[simp] +lemma Over.mapPullbackAdj_homEquiv_symm_apply_left (g) : + (((Over.mapPullbackAdj f hPf hQf).homEquiv A B).symm g).left = + g.left ≫ pullback.fst B.hom f := by + simp [mapPullbackAdj] + +@[simp] +lemma Over.mapPullbackAdj_unit_app_left (A) : ((Over.mapPullbackAdj f hPf hQf).unit.app A).left = + pullback.lift (𝟙 A.left) A.hom (by cat_disch) := + rfl + +@[simp] +lemma Over.mapPullbackAdj_counit_app_left (A) : ((Over.mapPullbackAdj f hPf hQf).counit.app A).left = + pullback.fst A.hom f := by + simp [mapPullbackAdj] + +end Adjunction + +/-- Pushforward along a morphism `f` (for which all pullbacks exist) exists relative to `P` +when pushforwards exist along `f` for all morphisms satisfying `P`. -/ +protected class HasPushforwardsAlong {S S' : T} (f : S ⟶ S') [hpb : HasPullbacksAlong f] where + hasPushforward : ∀ {W} (h : W ⟶ S), P h → HasPushforward f (.mk h) + +lemma hasPullbacksAlong_of_hasPullbacks {Q : MorphismProperty T} [Q.HasPullbacks] + {S S' : T} {q : S ⟶ S'} (hq : Q q) : HasPullbacksAlong q := + fun h => have := (Q.hasPullback h hq); hasPullback_symmetry q h + +variable {P Q} in +lemma hasPullbacksAlong_of_hasPullbacks' [Q.HasPullbacks] {S S' : T} {f : S ⟶ S'} (hf : Q f) : + P.HasPullbacksAlong f where + hasPullback g _ := hasPullbacksAlong_of_hasPullbacks hf g + +/-- Morphisms satisfying `P` have pushforwards along morphisms satisfying `Q`. +We require that `[H.HasPullbacks]` so that we can define the universal property of +pushforward along `p` relative to the pullback. +-/ +protected class HasPushforwards [Q.HasPullbacks] : Prop where + hasPushforwardsAlong : ∀ {S S' : T} (q : S ⟶ S') (hq : Q q), + have : HasPullbacksAlong q := hasPullbacksAlong_of_hasPullbacks hq + P.HasPushforwardsAlong q + +/-- Morphisms satisfying `P` are stable under pushforward along morphism `f` +if whenever pushforward along `f` exists it is in `P`. -/ +class IsStableUnderPushforwardsAlong {S S' : T} (q : S ⟶ S') [HasPullbacksAlong q] : Prop where + of_isPushforward {X Y : T} (f : X ⟶ S) (hf : P f) {g : Y ⟶ S'} + (isPushforward : IsPushforward q (.mk f) (.mk g)) : P g + +lemma IsStableUnderPushforwardsAlong.of_respectsIso [P.RespectsIso] {S S' : T} (q : S ⟶ S') + [HasPullbacksAlong q] (g : {X : T} → (f : X ⟶ S) → P f → Over S') + (pg : {X : T} → (f : X ⟶ S) → (pf : P f) → P (g f pf).hom) + (isPushforward : {X : T} → (f : X ⟶ S) → (pf : P f) → IsPushforward q (.mk f) (g f pf)) : + P.IsStableUnderPushforwardsAlong q where + of_isPushforward f pf g' isPushforward' := + have : g' = ((isPushforward f pf).uniqueUpToIso isPushforward').inv.left ≫ (g f pf).hom := + by cat_disch + this ▸ RespectsIso.precomp _ _ _ (pg ..) + +-- lemma IsStableUnderPushforwardsAlong.of_isLeftAdjoint [P.RespectsIso] {S S' : T} (q : S ⟶ S') +-- [HasPullbacksAlong q] [P.IsStableUnderBaseChangeAlong q] +-- [isLeftAdjoint : (Over.pullback P ⊤ q).IsLeftAdjoint] : +-- P.IsStableUnderPushforwardsAlong q where +-- of_isPushforward {X Y} f pf g isPushforward := +-- -- have : ((Over.pullback P ⊤ q).op ⋙ yoneda.obj (Over.mk ⊤ f pf)).RepresentableBy (Over.mk ⊤ g ) := sorry +-- -- have h := isPushforward.uniqueUpToIso +-- let i : CategoryTheory.Over.mk g ≅ +-- ((Over.pullback P ⊤ q).rightAdjoint.obj (Over.mk ⊤ f pf)).toComma := +-- sorry +-- have : g = i.hom.left ≫ ((Over.pullback P ⊤ q).rightAdjoint.obj (Over.mk ⊤ f pf)).hom := +-- sorry +-- this ▸ RespectsIso.precomp _ _ _ (Comma.prop ..) + +/-- Morphisms satisfying `P` are stable under pushforward along morphisms satisfying `Q` +if whenever pushforward along a morphism in `Q` exists it is in `P`. -/ +class IsStableUnderPushforwards [Q.HasPullbacks] : Prop where + of_isPushforward {S S' : T} (q : S ⟶ S') (hq : Q q) : + have : HasPullbacksAlong q := hasPullbacksAlong_of_hasPullbacks hq + IsStableUnderPushforwardsAlong P q + +noncomputable section + +abbrev pushforwardPartial.lift {S S' : T} (q : S ⟶ S') + [HasPullbacksAlong q] [P.HasPushforwardsAlong q] : + P.Over ⊤ S ⥤ (CategoryTheory.Over.pullback q).PartialRightAdjointSource := + ObjectProperty.lift _ (Over.forget P ⊤ S) + (fun X => HasPushforwardsAlong.hasPushforward X.hom X.prop) + +/-- If `P` has pushforwards along `q` then there is a partial left adjoint `P.Over ⊤ S ⥤ Over S'` +of the pullback functor `pullback q : Over S' ⥤ Over S`. +-/ +noncomputable def pushforwardPartial {S S' : T} (q : S ⟶ S') [HasPullbacksAlong q] + [P.HasPushforwardsAlong q] : P.Over ⊤ S ⥤ Over S' := + pushforwardPartial.lift P q ⋙ (CategoryTheory.Over.pullback q).partialRightAdjoint + +/-- When `P` has pushforwards along `Q` and is stable under pushforwards along `Q`, +the pushforward functor along any morphism `q` satisfying `Q` can be defined. -/ +noncomputable def pushforward {S S' : T} (q : S ⟶ S') [HasPullbacksAlong q] + [P.HasPushforwardsAlong q] [P.IsStableUnderPushforwardsAlong q] : + P.Over ⊤ S ⥤ P.Over ⊤ S' := + Comma.lift (pushforwardPartial P q) (fun X => + IsStableUnderPushforwardsAlong.of_isPushforward (q := q) X.hom X.prop + ((have : HasPushforward q X.toComma := HasPushforwardsAlong.hasPushforward _ X.prop + pushforward.isPushforward q (X.toComma)))) + (by simp) (by simp) + +def pushforwardCompForget {S S' : T} (q : S ⟶ S') [HasPullbacksAlong q] + [P.HasPushforwardsAlong q] [P.IsStableUnderPushforwardsAlong q] : + pushforward P q ⋙ Over.forget _ _ _ ≅ pushforwardPartial P q := + Iso.refl _ + +section homEquiv + +variable {P} {S S' : T} {q : S ⟶ S'} [HasPullbacksAlong q] + [P.HasPushforwardsAlong q] [P.IsStableUnderPushforwardsAlong q] + +/-- The pushforward functor is a partial right adjoint to pullback in the sense that +there is a natural bijection of hom-sets `T / S (pullback q X, Y) ≃ T / S' (X, pushforward q Y)`. -/ +def pushforward.homEquiv {X : Over S'} {Y : P.Over ⊤ S} : + (X ⟶ ((pushforward P q).obj Y).toComma) ≃ + ((CategoryTheory.Over.pullback q).obj X ⟶ Y.toComma) := + Functor.partialRightAdjointHomEquiv .. + +@[reassoc] +lemma pushforward.homEquiv_comp {X X' : Over S'} {Y : P.Over ⊤ S} + (f : X' ⟶ ((pushforward P q).obj Y).toComma) (g : X ⟶ X') : + pushforward.homEquiv (g ≫ f) = + (CategoryTheory.Over.pullback q).map g ≫ homEquiv f := + Functor.partialRightAdjointHomEquiv_comp .. + +@[reassoc] +lemma pushforward.homEquiv_map_comp {X : Over S'} {Y Y' : P.Over ⊤ S} + (f : X ⟶ ((pushforward P q).obj Y).toComma) (g : Y ⟶ Y') : + homEquiv (f ≫ Comma.Hom.hom ((P.pushforward q).map g)) = + homEquiv f ≫ Comma.Hom.hom g := + Functor.partialRightAdjointHomEquiv_map_comp .. + +@[reassoc] +lemma pushforward.homEquiv_symm_comp {X : Over S'} {Y Y' : P.Over ⊤ S} + (f : (CategoryTheory.Over.pullback q).obj X ⟶ Y.toComma) (g : Y ⟶ Y') : + homEquiv.symm f ≫ Comma.Hom.hom ((P.pushforward q).map g) = + homEquiv.symm (f ≫ Comma.Hom.hom g) := + Functor.partialRightAdjointHomEquiv_symm_comp .. + +@[reassoc] +lemma pushforward.homEquiv_comp_symm {X X' : Over S'} {Y : P.Over ⊤ S} + (f : (CategoryTheory.Over.pullback q).obj X' ⟶ Y.toComma) (g : X ⟶ X') : + g ≫ homEquiv.symm f = + homEquiv.symm ((CategoryTheory.Over.pullback q).map g ≫ f) := + Functor.partialRightAdjointHomEquiv_comp_symm .. + +def pushforward.homIso : Over.forget P ⊤ S ⋙ yoneda ⋙ (Functor.whiskeringLeft _ _ _).obj + (CategoryTheory.Over.pullback q).op ≅ P.pushforward q ⋙ Over.forget P ⊤ S' ⋙ yoneda := + (NatIso.ofComponents + (fun Y => NatIso.ofComponents (fun X => homEquiv.toIso) + (fun {X Y} f => by ext; simp [homEquiv_comp])) + (fun {X Y} f => by ext; simp [homEquiv_map_comp])).symm + +end homEquiv + +section + +open MorphismProperty.Over + +variable {P} [P.IsStableUnderBaseChange] {S S' : T} {f : S ⟶ S'} + [HasPullbacksAlong f] [P.HasPushforwardsAlong f] [P.IsStableUnderPushforwardsAlong f] + +instance : P.HasPullbacksAlong f where + hasPullback := inferInstance + +def pullbackPushforwardAdjunctionHomEquiv (X : P.Over ⊤ S') (Y : P.Over ⊤ S) : + ((Over.pullback P ⊤ f).obj X ⟶ Y) ≃ (X ⟶ (P.pushforward f).obj Y) := + calc ((pullback P ⊤ f).obj X ⟶ Y) + _ ≃ (((pullback P ⊤ f).obj X).toComma ⟶ Y.toComma) := + (Functor.FullyFaithful.ofFullyFaithful (Over.forget P ⊤ S)).homEquiv + _ ≃ (X.toComma ⟶ ((P.pushforward f).obj Y).toComma) := + pushforward.homEquiv.symm + _ ≃ _ := Iso.homCongr (Iso.refl X.toComma) (by exact Iso.refl _) + _ ≃ (X ⟶ (P.pushforward f).obj Y) := + (Functor.FullyFaithful.ofFullyFaithful (Over.forget P ⊤ S')).homEquiv.symm + +@[simp] +lemma pullbackPushforwardAdjunctionHomEquiv_apply {X : P.Over ⊤ S'} {Y : P.Over ⊤ S} + (g : (Over.pullback P ⊤ f).obj X ⟶ Y) : + (pullbackPushforwardAdjunctionHomEquiv X Y g).toCommaMorphism = + pushforward.homEquiv.symm (Comma.Hom.hom g) := by + simp only [pullbackPushforwardAdjunctionHomEquiv, Trans.trans, Comma.forget_obj, + Equiv.trans_apply, Iso.homCongr_apply, Iso.refl_inv, Iso.refl_hom, Category.comp_id, + Category.id_comp] + erw [Functor.FullyFaithful.homEquiv_apply, Functor.FullyFaithful.homEquiv_symm_apply] + simp [Over.forget_preimage] + rfl + +@[simp] +lemma pullbackPushforwardAdjunctionHomEquiv_symm_apply {X : P.Over ⊤ S'} {Y : P.Over ⊤ S} + (g : X ⟶ (P.pushforward f).obj Y) : + ((pullbackPushforwardAdjunctionHomEquiv X Y).symm g).toCommaMorphism = + pushforward.homEquiv (Comma.Hom.hom g) := by + simp only [pullbackPushforwardAdjunctionHomEquiv, Trans.trans, Comma.forget_obj, + Equiv.symm_trans_apply, Equiv.symm_symm, Iso.homCongr_symm, Iso.refl_symm, Iso.homCongr_apply, + Iso.refl_inv, Iso.refl_hom, Category.comp_id, Category.id_comp] + erw [Functor.FullyFaithful.homEquiv_apply, Functor.FullyFaithful.homEquiv_symm_apply] + simp [Over.forget_preimage] + rfl + +variable (P) (f) in +/-- The `pullback ⊣ pushforward` adjunction. -/ +def pullbackPushforwardAdjunction : Over.pullback P ⊤ f ⊣ pushforward P f := + Adjunction.mkOfHomEquiv { + homEquiv X Y := pullbackPushforwardAdjunctionHomEquiv X Y + homEquiv_naturality_left_symm g₁ g₂ := by + ext + simp only [pullback_obj_left, pullbackPushforwardAdjunctionHomEquiv_symm_apply, + Comma.comp_hom, CategoryTheory.Comma.comp_left, pullback_map_left] + rw [pushforward.homEquiv_comp] + simp + homEquiv_naturality_right g₁ g₂ := by + ext + simp only [pullbackPushforwardAdjunctionHomEquiv_apply, Comma.comp_hom, + CategoryTheory.Comma.comp_left] + convert_to _ = ((pushforward.homEquiv.symm (Comma.Hom.hom g₁)) ≫ + (Comma.Hom.hom ((P.pushforward f).map g₂))).left + rw [pushforward.homEquiv_symm_comp] } + +@[simp] +lemma pullbackPushforwardAdjunction_apply {X : P.Over ⊤ S'} {Y : P.Over ⊤ S} + (g : (Over.pullback P ⊤ f).obj X ⟶ Y) : + ((pullbackPushforwardAdjunction P f).homEquiv X Y g).toCommaMorphism = + pushforward.homEquiv.symm (Comma.Hom.hom g) := by + simp [pullbackPushforwardAdjunction, pullbackPushforwardAdjunctionHomEquiv_apply] + +@[simp] +lemma pullbackPushforwardAdjunction_symm_apply {X : P.Over ⊤ S'} {Y : P.Over ⊤ S} + (g : X ⟶ (P.pushforward f).obj Y) : + (((pullbackPushforwardAdjunction P f).homEquiv X Y).symm g).toCommaMorphism = + pushforward.homEquiv (Comma.Hom.hom g) := by + simp [pullbackPushforwardAdjunction, pullbackPushforwardAdjunctionHomEquiv_symm_apply] + +@[simp] +lemma pullbackPushforwardAdjunction_unit_app_toCommaMorphism {X : P.Over ⊤ S'} : + ((pullbackPushforwardAdjunction P f).unit.app X).toCommaMorphism = + pushforward.homEquiv.symm (𝟙 ((Over.pullback P ⊤ f).obj X).toComma) := by + simp [pullbackPushforwardAdjunction, pullbackPushforwardAdjunctionHomEquiv_apply] + +@[simp] +lemma pullbackPushforwardAdjunction_counit_app_toCommaMorphism {Y : P.Over ⊤ S} : + ((pullbackPushforwardAdjunction P f).counit.app Y).toCommaMorphism = + pushforward.homEquiv (𝟙 ((P.pushforward f).obj Y).toComma) := by + simp [pullbackPushforwardAdjunction, pullbackPushforwardAdjunctionHomEquiv_symm_apply] + +instance : (pullback P ⊤ f).IsLeftAdjoint := + Adjunction.isLeftAdjoint (pullbackPushforwardAdjunction P f) + +instance : (pushforward P f).IsRightAdjoint := + Adjunction.isRightAdjoint (pullbackPushforwardAdjunction P f) + +end + +section homEquiv + +variable {P} [P.HasPullbacks] [P.IsStableUnderBaseChange] {S S' : T} (i : S ⟶ S') + +/-- `MorphismProperty.Over.pullback P ⊤ f` is a partial right adjoint to `Over.map f`. -/ +@[simps!] +def pullback.homEquiv {X : Over S} {Y : P.Over ⊤ S'} : + (X ⟶ ((Over.pullback P ⊤ i).obj Y).toComma) ≃ + ((CategoryTheory.Over.map i).obj X ⟶ Y.toComma) where + toFun v := CategoryTheory.Over.homMk (v.left ≫ pullback.fst _ _) <| by + simp only [Category.assoc, pullback.condition, + CategoryTheory.Over.map_obj_hom] + erw [← CategoryTheory.Over.w v] + simp + invFun u := CategoryTheory.Over.homMk (pullback.lift u.left X.hom <| by simp) + left_inv v := by + ext; dsimp; ext + · simp + · simpa using (CategoryTheory.Over.w v).symm + right_inv u := by cat_disch + +lemma pullback.homEquiv_comp {X X' : Over S} {Y : P.Over ⊤ S'} + (f : X' ⟶ ((Over.pullback P ⊤ i).obj Y).toComma) (g : X ⟶ X') : + homEquiv i (g ≫ f) = + (CategoryTheory.Over.map i).map g ≫ homEquiv i f := by + ext; simp + +lemma pullback.homEquiv_map_comp {X : Over S} {Y Y' : P.Over ⊤ S'} + (f : X ⟶ ((Over.pullback P ⊤ i).obj Y).toComma) (g : Y ⟶ Y') : + homEquiv i (f ≫ Comma.Hom.hom ((Over.pullback P ⊤ i).map g)) = + homEquiv i f ≫ Comma.Hom.hom g := by + ext; simp + +lemma pullback.homEquiv_symm_comp {X : Over S} {Y Y' : P.Over ⊤ S'} + (f : (CategoryTheory.Over.map i).obj X ⟶ Y.toComma) (g : Y ⟶ Y') : + (homEquiv i).symm f ≫ Comma.Hom.hom ((Over.pullback P ⊤ i).map g) = + (homEquiv i).symm (f ≫ Comma.Hom.hom g) := by + ext; dsimp; ext + · simp + · simp + +lemma pullback.homEquiv_comp_symm {X X' : Over S} {Y : P.Over ⊤ S'} + (f : (CategoryTheory.Over.map i).obj X' ⟶ Y.toComma) (g : X ⟶ X') : + g ≫ (homEquiv i).symm f = + (homEquiv i).symm ((CategoryTheory.Over.map i).map g ≫ f) := by + ext; dsimp; ext + · simp + · simp + +end homEquiv + +end + +end CategoryTheory.MorphismProperty diff --git a/HoTTLean/ForMathlib/CategoryTheory/NatTrans.lean b/HoTTLean/ForMathlib/CategoryTheory/NatTrans.lean index aee6e9a4..c732d2a5 100644 --- a/HoTTLean/ForMathlib/CategoryTheory/NatTrans.lean +++ b/HoTTLean/ForMathlib/CategoryTheory/NatTrans.lean @@ -2,6 +2,7 @@ import Mathlib.CategoryTheory.NatTrans import Mathlib.CategoryTheory.Functor.TwoSquare import Mathlib.CategoryTheory.Limits.Shapes.Pullback.CommSq import HoTTLean.ForMathlib +import Poly.ForMathlib.CategoryTheory.NatTrans universe w v u v₁ u₁ v₂ u₂ v₃ u₃ @@ -46,3 +47,31 @@ instance {A : Type*} [Category A] {B : Type*} [Groupoid B] : comp_inv := NatTrans.vcomp_inv end CategoryTheory + +namespace CategoryTheory + +universe v' u' v₄ v₅ v₆ v₇ v₈ u₄ u₅ u₆ u₇ u₈ + +variable {J : Type v'} [Category.{u'} J] {C : Type u} [Category.{v} C] +variable {K : Type*} [Category K] {D : Type*} [Category D] + +namespace NatTrans +namespace IsCartesian + +open TwoSquare + +variable {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} + [Category.{v₁} C₁] [Category.{v₂} C₂] [Category.{v₃} C₃] [Category.{v₄} C₄] + {T : C₁ ⥤ C₂} {L : C₁ ⥤ C₃} {R : C₂ ⥤ C₄} {B : C₃ ⥤ C₄} +variable {C₅ : Type u₅} {C₆ : Type u₆} {C₇ : Type u₇} {C₈ : Type u₈} + [Category.{v₅} C₅] [Category.{v₆} C₆] [Category.{v₇} C₇] [Category.{v₈} C₈] + {T' : C₂ ⥤ C₅} {R' : C₅ ⥤ C₆} {B' : C₄ ⥤ C₆} {L' : C₃ ⥤ C₇} {R'' : C₄ ⥤ C₈} {B'' : C₇ ⥤ C₈} + +theorem vCompIsIso {w : TwoSquare T L R B} [IsIso w] {w' : TwoSquare B L' R'' B''} : + IsCartesian w' → IsCartesian (w ≫ᵥ w') := + fun cw' => + (isCartesian_of_isIso _).comp <| + (isCartesian_of_isIso _).comp <| + (isCartesian_of_isIso _).comp <| + (IsCartesian.whiskerLeft cw' _).comp + (isCartesian_of_isIso _) diff --git a/HoTTLean/ForMathlib/CategoryTheory/Polynomial.lean b/HoTTLean/ForMathlib/CategoryTheory/Polynomial.lean new file mode 100644 index 00000000..5bbaaf3e --- /dev/null +++ b/HoTTLean/ForMathlib/CategoryTheory/Polynomial.lean @@ -0,0 +1,1340 @@ +import HoTTLean.ForMathlib.CategoryTheory.Clan + +universe v u v₁ u₁ + +noncomputable section + +namespace CategoryTheory + +open Category Limits MorphismProperty + +variable {C : Type u} [Category.{u} C] + +namespace MorphismProperty + +open NatTrans MorphismProperty.Over in +/-- The counit of the adjunction `mapPullbackAdj` is a pullback square, +since it is the pullback computed by `P.Over.pullback`. -/ +lemma isCartesian_mapPullbackAdj_counit {P : MorphismProperty C} {X Y : C} {f : X ⟶ Y} + [P.IsStableUnderComposition] [P.IsStableUnderBaseChange] + [P.HasPullbacksAlong f] (hPf : P f) : IsCartesian (mapPullbackAdj (Q := ⊤) f hPf trivial).counit := by + intro A B U + apply (MorphismProperty.Over.forget P ⊤ Y).reflect_isPullback + apply (CategoryTheory.Over.forget Y).reflect_isPullback + apply IsPullback.flip + simp only [Functor.comp_obj, Comma.forget_obj, Over.forget_obj, map_obj_left, pullback_obj_left, + Functor.id_obj, mapPullbackAdj, Adjunction.mkOfHomEquiv, Equiv.invFun_as_coe, + Adjunction.mk'_counit, Comma.forget_map, Over.forget_map, + mapPullbackAdjHomEquiv_symm_apply_left, Comma.id_hom, CategoryTheory.Comma.id_left, id_comp, + Functor.comp_map, map_map_left, pullback_map_left, Functor.id_map] + apply IsPullback.of_bot (v₂₁ := (pullback.snd B.hom f)) (h₃₁ := f) (v₂₂ := B.hom) _ _ + (IsPullback.of_hasPullback B.hom f) + · convert IsPullback.of_hasPullback A.hom f <;> simp + · simp + +namespace PolynomialPartialAdjunction + +variable {T : Type u} [Category.{v} T] {R : MorphismProperty T} + [R.HasPullbacks] [R.IsStableUnderBaseChange] + {E I B : T} (i : E ⟶ I) (p : E ⟶ B) + [HasPullbacksAlong p] [R.HasPushforwardsAlong p] + [R.IsStableUnderPushforwardsAlong p] + +/-- The partial right adjoint representing a multivariate polynomial. -/ +abbrev partialRightAdjoint := Over.pullback R ⊤ i ⋙ pushforward R p + +/-- The left adjoint in the partial adjunction. -/ +abbrev leftAdjoint := CategoryTheory.Over.pullback p ⋙ CategoryTheory.Over.map i + +/-- `pullback R ⊤ i ⋙ pushforward R p` is a partial right adjoint to +`CategoryTheory.Over.pullback p.1 ⋙ CategoryTheory.Over.map i` + ``` + pullback i pushforward p + R.Over I ------> R.Over E -----> R.Over B + | | | + | ⊥ | ⊥ | + | | | + V V V + C/I <--------- C/E <------------ C/B + map i pullback p + ``` + +On paper this is written `C/B (X, p⁎ (i* Y)) ≃ C/I (i! (p* X), Y)`. +-/ +def homEquiv {X : Over B} {Y : R.Over ⊤ I} : + (X ⟶ ((partialRightAdjoint i p).obj Y).toComma) ≃ + ((leftAdjoint i p).obj X ⟶ Y.toComma) := + calc (X ⟶ ((R.pushforward p).obj ((Over.pullback R ⊤ i).obj Y)).toComma) + _ ≃ ((CategoryTheory.Over.pullback p).obj X ⟶ ((Over.pullback R ⊤ i).obj Y).toComma) := + pushforward.homEquiv + _ ≃ ((CategoryTheory.Over.map i).obj + ((CategoryTheory.Over.pullback p).obj X) ⟶ Y.toComma) := + pullback.homEquiv _ + +lemma homEquiv_comp {X X' : Over B} {Y : R.Over ⊤ I} + (f : X' ⟶ ((partialRightAdjoint i p).obj Y).toComma) (g : X ⟶ X') : + homEquiv i p (g ≫ f) = + (leftAdjoint i p).map g ≫ homEquiv i p f := by + unfold homEquiv + simp only [Functor.comp_obj, Equiv.trans_def, Equiv.trans_apply] + erw [pushforward.homEquiv_comp, pullback.homEquiv_comp] + rfl + +lemma homEquiv_map_comp {X : Over B} {Y Y' : R.Over ⊤ I} + (f : X ⟶ ((partialRightAdjoint i p).obj Y).toComma) (g : Y ⟶ Y') : + homEquiv i p (f ≫ Comma.Hom.hom ((partialRightAdjoint i p).map g)) = + homEquiv i p f ≫ Comma.Hom.hom g := by + unfold homEquiv + simp only [Functor.comp_obj, Equiv.trans_def, Equiv.trans_apply] + erw [pushforward.homEquiv_map_comp, pullback.homEquiv_map_comp] + rfl + +lemma homEquiv_symm_comp {X : Over B} {Y Y' : R.Over ⊤ I} + (f : (leftAdjoint i p).obj X ⟶ Y.toComma) (g : Y ⟶ Y') : + (homEquiv i p).symm f ≫ Comma.Hom.hom ((partialRightAdjoint i p).map g) = + (homEquiv i p).symm (f ≫ Comma.Hom.hom g) := by + unfold homEquiv + simp + erw [pushforward.homEquiv_symm_comp, pullback.homEquiv_symm_comp] + rfl + +lemma homEquiv_comp_symm {X X' : Over B} {Y : R.Over ⊤ I} + (f : (leftAdjoint i p).obj X' ⟶ Y.toComma) (g : X ⟶ X') : + g ≫ (homEquiv i p).symm f = + (homEquiv i p).symm ((leftAdjoint i p).map g ≫ f) := by + unfold homEquiv + simp + erw [pushforward.homEquiv_comp_symm, pullback.homEquiv_comp_symm] + rfl + +/-- The counit of the partial adjunction is given by evaluating the equivalence of +hom-sets at the identity. +On paper we write this as `counit : i! p* p∗ i* => Over.forget : R.Over ⊤ I ⥤ Over I` +-/ +def counit : + partialRightAdjoint i p ⋙ Over.forget R ⊤ B ⋙ leftAdjoint i p ⟶ Over.forget R ⊤ I where + app _ := homEquiv i p (𝟙 _) + naturality X Y f := by + apply (homEquiv i p).symm.injective + conv => left; erw [← homEquiv_comp_symm] + conv => right; erw [← homEquiv_symm_comp] + simp + +/-- A commutative diagram +``` + I + ↗ ↖ + i / \ i' + / ρ \ + E -------> E' + \ / + p \ / p' + ↘ ↙ + B +``` +induces a natural transformation `partialRightAdjoint i p ⟶ partialRightAdjoint i' p'` +obtained by pasting the following 2-cells +``` + pullback i' pushforward p' +R.Over ⊤ I ----> R.Over ⊤ E' ----> R.Over ⊤ B + ‖ | ‖ + ‖ | ‖ + ‖ ↙ |ρ* ↙ ‖ + ‖ | ‖ + ‖ V ‖ +R.Over ⊤ I ----> R.Over ⊤ E ----> R.Over ⊤ B + pullback i pushforward p +``` +-/ +def partialRightAdjointMap {E' : T} (i' : E' ⟶ I) (p' : E' ⟶ B) + [HasPullbacksAlong p'] [R.HasPushforwardsAlong p'] + [R.IsStableUnderPushforwardsAlong p'] (ρ) + (hi : i = ρ ≫ i') (hρ : p = ρ ≫ p') : + partialRightAdjoint (R := R) i' p' ⟶ partialRightAdjoint i p := + let cellLeftIso : Over.pullback R ⊤ i' ⋙ Over.pullback R ⊤ ρ ≅ Over.pullback R ⊤ i := + (Over.pullbackComp ρ i').symm ≪≫ eqToIso (by rw [hi]) + let cellLeft : TwoSquare (Over.pullback R ⊤ i') (𝟭 _) (Over.pullback R ⊤ ρ) (Over.pullback R ⊤ i) := + ((Over.pullbackComp ρ i').symm ≪≫ eqToIso (by simp [hi, Functor.id_comp])).hom + let cellRight := pushforwardPullbackTwoSquare (R := R) ρ p p' (𝟙 _) (by simp [← hρ]) + Functor.whiskerLeft (partialRightAdjoint i' p') (Over.pullbackId R ⊤ B).inv ≫ + cellLeft.hComp cellRight + +end PolynomialPartialAdjunction + +variable (P : MorphismProperty C) + +namespace Over + +@[simps] +def equivalenceOfHasObjects' (R : MorphismProperty C) [R.HasObjects] + {X : C} (hX : IsTerminal X) : R.Over ⊤ X ≌ Over X where + functor := MorphismProperty.Over.forget _ _ _ + inverse := Comma.lift (𝟭 _) (by intro; apply HasObjects.obj_mem _ hX) (by simp) (by simp) + unitIso := eqToIso rfl + counitIso := eqToIso rfl + functor_unitIso_comp := by simp + +@[simp] +def equivalenceOfHasObjects (R : MorphismProperty C) [R.HasObjects] + {X : C} (hX : IsTerminal X) : R.Over ⊤ X ≌ C := + (equivalenceOfHasObjects' R hX).trans (Over.equivalenceOfIsTerminal hX) + +variable {P : MorphismProperty C} {E B : C} + +@[simps] +def ofMorphismProperty {p : E ⟶ B} (hp : P p) : P.Over ⊤ B where + left := E + right := ⟨⟨⟩⟩ + hom := p + prop := hp + +@[simps] +def homMkTop {p q : P.Over ⊤ B} (left : p.left ⟶ q.left) (hleft : left ≫ q.hom = p.hom) : + p ⟶ q where + left := left + right := eqToHom (by simp) + w := by simp [hleft] + prop_hom_left := trivial + prop_hom_right := trivial + +/-- +Convert an object `p` in `R.Over ⊤ B` to a morphism in `R.Over ⊤ O` by composing with `o`. + p + E -----> B + \ / + \ /o + \ / + VV + O +-/ +@[simp] +def homOfMorphismProperty [P.IsStableUnderComposition] {O} (p : P.Over ⊤ B) {o : B ⟶ O} (ho : P o) : + (map ⊤ ho).obj p ⟶ Over.ofMorphismProperty ho := + Over.homMk p.hom (by simp) + +end Over + +end MorphismProperty + +open MorphismProperty.Over + +/-- `P : MvPoly R H I O` is a the signature for a multivariate polynomial functor, +consisting of the following maps +``` + p + E ---> B + i ↙ ↘ o + I O +``` +We can lazily read this as `∑ b : B, X ^ (E b)`, +for some `X` in the (`P`-restricted) slice over `I`. + +In full detail: +Viewing such an `X` as a series of variables `X_k` indexed by `k ∈ I`, +and `B` as a family of types `B_k` indexed by `j ∈ O` +this can be further viewed as `O`-many `I`-ary polynomials `∑ b : B_j, X_(i b) ^ (E b)` + +To explain the need for two morphism properties, +consider the following two use-cases: +1. `R = ⊤` is all maps and the category has all pullbacks. + `H` is the class of exponentiable maps - it follows from all maps having pullbacks that `H` + also has pullbacks. +2. `R = H` is a π-clan, [see Joyal, def 2.4.1](https://arxiv.org/pdf/1710.10238). + +This will typically be used with the following instances + +- For pullback of `R`-maps along `i`, `p` and `o` we need + `[R.IsStableUnderBaseChange] [R.HasPullbacks]` +- For the left adjoint to pullback for `o` we need `[R.IsStableUnderComposition]` +- For pushforward of `R`-maps along `p` we need + `[R.IsStableUnderPushforward H] [R.HasPushforwards H]` +- For pushforward of `R`-maps along `p` we also assume `[H.HasPullbacks]`. + This is useful - it makes the `R`-restricted pushforward of `R`-maps along `p` + a partial left adjoint to *global* pullback along `p`, + ``` + pushforward p + R.Over E -----> R.Over B + | | + | ⊥ | + | | + V V + C/E <--------- C/B + pullback p + ``` + which is strictly stronger than just having a left adjoint to `R`-restricted pullback + `(pullback : R.Over B ⥤ R.Over E) ⊣ (pushforward : R.Over E ⥤ R.Over B)`. +-/ +structure MvPoly (R : MorphismProperty C) (I O E B : C) where + (i : E ⟶ I) + (hi : R i) + (p : E ⟶ B) + (o : B ⟶ O) + (ho : R o) + +namespace MvPoly + +variable {R : MorphismProperty C} + +instance {B O : C} {i : B ⟶ O} (hi : R i) [R.HasPullbacks] [R.IsStableUnderBaseChange] + [R.IsStableUnderComposition] : (pullback R ⊤ i).IsRightAdjoint := + (mapPullbackAdj (Q := ⊤) i hi ⟨⟩).isRightAdjoint + +variable {I O E B : C} (P : MvPoly R I O E B) [R.HasPullbacks] [R.IsStableUnderBaseChange] + [HasPullbacksAlong P.p] [R.HasPushforwardsAlong P.p] [R.IsStableUnderPushforwardsAlong P.p] + +open PolynomialPartialAdjunction + +/-- (Ignoring the indexing from `i` and `o`) +This is the first projection morphism from `P @ X = ∑ b : B, X ^ (E b)` to `B`, +as an object in the `P`-restricted slice over `B`. -/ +abbrev fstProj (X : R.Over ⊤ I) : R.Over ⊤ B := + (partialRightAdjoint P.i P.p).obj X + +/-- The counit of the adjunction `pullback p ⋙ map i ⊣ pullback i ⋙ pushforward p` evaluated at `X`. +Ignoring the indexing from `i` and `o`, +this can be viewed as the second projection morphism from `P @ X = ∑ b : B, X ^ (E b)` +to `X^ (E b)`. + +``` + X ----------> I + ∧ ∧ + | | + sndProj | i + | | + • ----------> E + | | + | (pb) | + | |p + V fstProj V + P @ X --------> B + ⟍ | + ⟍ |o + ⟍ | + ↘ V + O +``` +-/ +def sndProj (X : R.Over ⊤ I) : + (leftAdjoint P.i P.p).obj (fstProj P X).toComma ⟶ X.toComma := + (counit P.i P.p).app X + +section + +variable {X Y : R.Over ⊤ I} (f : X ⟶ Y) + +@[reassoc (attr := simp)] +lemma map_fstProj : + ((partialRightAdjoint P.i P.p).map f).left ≫ (fstProj P Y).hom = (fstProj P X).hom := by + simp + +lemma sndProj_comp_hom : (sndProj P X).left ≫ X.hom = pullback.snd _ _ ≫ P.i := by + simp [sndProj] + +lemma sndProj_comp : (sndProj P X).left ≫ f.left = + pullback.map _ _ _ _ + ((partialRightAdjoint P.i P.p).map f).left (𝟙 _) (𝟙 _) (by simp) (by simp) ≫ + (sndProj P Y).left := by + have := congr_arg CommaMorphism.left <| (counit P.i P.p).naturality f + simpa [pullback.map] using this.symm + +end + +variable [R.IsStableUnderComposition] +/-- A multivariate polynomial signature +``` + p + E ---> B + i ↙ ↘ o + I O +``` +gives rise to a functor +``` + pushforward p + R.Over ⊤ E ---------> R.Over ⊤ B + pullback i ↗ ⟍ map o + ⟋ ⟍ + ⟋ ↘ + R.Over ⊤ I R.Over ⊤ O +``` +-/ +def functor : R.Over ⊤ I ⥤ R.Over ⊤ O := + pullback R ⊤ P.i ⋙ MorphismProperty.pushforward R P.p ⋙ map ⊤ P.ho + +/-- The action of a univariate polynomial on objects. -/ +def apply : R.Over ⊤ I → R.Over ⊤ O := (functor P).obj + +@[inherit_doc] +infix:90 " @ " => apply + +namespace Equiv + +variable {P} {Γ : Over O} {X : R.Over ⊤ I} + +def fst (pair : Γ ⟶ (P @ X).toComma) : Over B := Over.mk (pair.left ≫ (fstProj P X).hom) + +abbrev sndDom (pair : Γ ⟶ (P @ X).toComma) : Over I := (leftAdjoint P.i P.p).obj (fst pair) + +def snd (pair : Γ ⟶ (P @ X).toComma) : sndDom pair ⟶ X.toComma := + homEquiv P.i P.p (Over.homMk (pair.left)) + +lemma snd_eq (pair : Γ ⟶ (P @ X).toComma) : snd pair = + (leftAdjoint P.i P.p).map (Over.homMk (pair.left)) ≫ sndProj P X := by + erw [Equiv.apply_eq_iff_eq_symm_apply, ← homEquiv_comp_symm] + simp [sndProj, counit] + +def mk (f : Over B) (hf : Γ = (Over.map P.o).obj f) + (s : (leftAdjoint P.i P.p).obj f ⟶ X.toComma) : + Γ ⟶ (P @ X).toComma := + eqToHom hf ≫ (Over.map P.o).map ((homEquiv P.i P.p).symm s) + +@[simp] +lemma fst_mk (f : Over B) (hf : Γ = (Over.map P.o).obj f) + (s : (leftAdjoint P.i P.p).obj f ⟶ X.toComma) : fst (mk f hf s) = f := by + subst hf; simp [fst, mk] + +lemma snd_mk (f : Over B) (hf : Γ = (Over.map P.o).obj f) + (s : (leftAdjoint P.i P.p).obj f ⟶ X.toComma) : snd (mk f hf s) = + eqToHom (by simp) ≫ s := calc snd (mk f hf s) + _ = (leftAdjoint P.i P.p).map (eqToHom (fst_mk f hf s)) ≫ s := by + erw [Equiv.apply_eq_iff_eq_symm_apply, ← homEquiv_comp_symm] + ext + simp [mk] + _ = eqToHom _ ≫ s := by + simp only [eqToHom_map] + +@[simp] +lemma map_fst (pair : Γ ⟶ (P @ X).toComma) : (Over.map P.o).obj (fst pair) = Γ := by + have := pair.w + simp only [Functor.id_obj, Functor.const_obj_obj, Functor.id_map, + CostructuredArrow.right_eq_id, Functor.const_obj_map, comp_id] at this + simp [Over.map, Comma.mapRight, fst] + congr + +@[simp] +lemma eta (pair : Γ ⟶ (P @ X).toComma) : mk (fst pair) (by simp) (snd pair) = pair := by + ext + simp [mk, snd] + +end Equiv + +-- -- NOTE: please leave the commented out subgoals, it makes debugging this easier +-- instance (P : MvPoly R H I O E B) : PreservesLimitsOfShape WalkingCospan +-- (MorphismProperty.Over.pullback R ⊤ P.i ⋙ R.pushforward P.hp ⋙ +-- MorphismProperty.Over.map ⊤ P.ho) := +-- have : (MorphismProperty.Over.pullback R ⊤ P.i).IsRightAdjoint := +-- Adjunction.isRightAdjoint (MorphismProperty.Over.mapPullbackAdj R ⊤ P.i P.hi trivial) +-- -- have : PreservesLimitsOfShape WalkingCospan (MorphismProperty.Over.pullback R ⊤ P.i) := +-- -- inferInstance +-- -- have : PreservesLimitsOfShape WalkingCospan (R.pushforward P.hp) := +-- -- inferInstance +-- -- have : PreservesLimitsOfShape WalkingCospan (MorphismProperty.Over.map ⊤ P.ho) := +-- -- inferInstance +-- inferInstance + +-- instance (P : MvPoly R H I O E B) : +-- Limits.PreservesLimitsOfShape WalkingCospan (MvPoly.functor P) := by +-- dsimp [functor] +-- infer_instance + +/-- A commutative triangle +``` + I + ↗ ↖ +P.i/ \Q.i + / ρ \ + E -------> F + \ / +P.p\ / Q.p + ↘ ↙ + B +``` +induces a natural transformation `Q.functor ⟶ P.functor` when `Q.o = P.o`, +obtained by pasting the following 2-cells +``` + pullback Q.i pushforward Q.p.1 map Q.o.1 +R.Over ⊤ I ----> R.Over ⊤ F ----> R.Over ⊤ B -----> R.Over ⊤ O + ‖ | ‖ ‖ + ‖ | ‖ ‖ + ‖ ↙ |ρ* ↙ ‖ = ‖ + ‖ | ‖ ‖ + ‖ V ‖ ‖ +R.Over ⊤ I ----> R.Over ⊤ E ----> R.Over ⊤ B -----> R.Over ⊤ O + pullback P.i pushforward P.p.1 map P.o +``` +-/ +def verticalNatTrans {F : C} (P : MvPoly R I O E B) (Q : MvPoly R I O F B) + [HasPullbacksAlong P.p] [R.HasPushforwardsAlong P.p] [R.IsStableUnderPushforwardsAlong P.p] + [HasPullbacksAlong Q.p] [R.HasPushforwardsAlong Q.p] [R.IsStableUnderPushforwardsAlong Q.p] + (ρ : E ⟶ F) (hi : P.i = ρ ≫ Q.i) (hp : P.p = ρ ≫ Q.p) (ho : P.o = Q.o) : + Q.functor ⟶ P.functor := + (Functor.associator _ _ _).inv ≫ + ((PolynomialPartialAdjunction.partialRightAdjointMap P.i P.p Q.i Q.p ρ hi hp) ◫ + (eqToHom (by rw! [ho]))) ≫ + (Functor.associator _ _ _).hom + +section + +variable {F} (Q : MvPoly R I O F B) [HasPullbacksAlong Q.p] [R.HasPushforwardsAlong Q.p] + [R.IsStableUnderPushforwardsAlong Q.p] + (ρ : E ⟶ F) (hi : P.i = ρ ≫ Q.i) (hp : P.p = ρ ≫ Q.p) (ho : P.o = Q.o) + +lemma fst_verticalNatTrans_app {Γ} {X} (pair : Γ ⟶ (Q @ X).toComma) : + Equiv.fst (pair ≫ ((verticalNatTrans P Q ρ hi hp ho).app X).hom) = Equiv.fst pair := by + -- simp [verticalNatTrans, partialRightAdjointMap] + -- erw [Category.id_comp] + -- dsimp [Equiv.fst] + -- congr 1 + sorry + +-- lemma snd'_verticalNatTrans_app {Γ} {X} (pair : Γ ⟶ (Q @ X).toComma) : +-- Equiv.snd (pair ≫ ((verticalNatTrans P Q ρ hi hp ho).app X).hom) = +-- --(H.lift f' (g' ≫ ρ) (by simp [H'.w, h])) ≫ +-- sorry ≫ Equiv.snd pair := by +-- sorry + +-- lemma mk'_comp_verticalNatTrans_app {Γ : Over O} {X : R.Over ⊤ I} (f : Over B) +-- (hf : Γ = (Over.map Q.o.1).obj f) (s : (leftAdjoint Q.i.1 Q.p).obj f ⟶ X.toComma) : +-- Equiv.mk f hf s ≫ ((verticalNatTrans P Q ρ hi hp ho).app X).hom = +-- Equiv.mk f (sorry) sorry ≫ sorry +-- := +-- sorry + +end + +open TwoSquare + +/-- A cartesian map +``` + P.p + E --------> B + P.i ↙ | | ↘ P.o + I φ| (pb) | δ O + P'.i ↖ v v ↗ P'.o + E' --------> B' + P'.p +``` +induces a natural transformation between their associated functors obtained by pasting the following +2-cells +``` + pullback P'.i pushforward P'.p map P'.o +R.Over I ------ > R.Over E' --------> R.Over B' --------> R.Over O + ‖ | | ‖ + ‖ | | ‖ + ‖ ↗ pullback φ ↗ pullback δ ↗ ‖ + ‖ | | ‖ + ‖ v v ‖ +R.Over I ------ > R.Over E --------> R.Over B --------> R.Over O + pullback P.i pushforward P.p map P.o +``` +-/ +def cartesianNatTrans {E' B' : C} (P : MvPoly R I O E B) (P' : MvPoly R I O E' B') + [HasPullbacksAlong P.p] [R.HasPushforwardsAlong P.p] [R.IsStableUnderPushforwardsAlong P.p] + [HasPullbacksAlong P'.p] [R.HasPushforwardsAlong P'.p] [R.IsStableUnderPushforwardsAlong P'.p] + (δ : B ⟶ B') (φ : E ⟶ E') (hφ : P.i = φ ≫ P'.i) (pb : IsPullback φ P.p P'.p δ) + (hδ : δ ≫ P'.o = P.o) : + P.functor ⟶ P'.functor := + let cellLeft : TwoSquare (𝟭 (R.Over ⊤ I)) (MorphismProperty.Over.pullback R ⊤ P'.i) + (MorphismProperty.Over.pullback R ⊤ P.i) (MorphismProperty.Over.pullback R ⊤ φ) := + (eqToIso (by simp [hφ, Functor.id_comp]) ≪≫ (MorphismProperty.Over.pullbackComp φ P'.i)).hom + let cellMid : TwoSquare (MorphismProperty.Over.pullback R ⊤ φ) + (R.pushforward P'.p) (R.pushforward P.p) (MorphismProperty.Over.pullback R ⊤ δ) := + (pushforwardPullbackIso φ P.p P'.p δ pb).inv + let cellRight : TwoSquare (MorphismProperty.Over.pullback R ⊤ δ) + (MorphismProperty.Over.map ⊤ P'.ho) (MorphismProperty.Over.map ⊤ P.ho) (𝟭 _) := + (pullbackMapTwoSquare R P.o δ (𝟙 _) P'.o P'.ho P.ho (by simp [hδ])) ≫ + Functor.whiskerLeft _ (MorphismProperty.Over.pullbackId R ⊤ O).hom + cellLeft ≫ᵥ cellMid ≫ᵥ cellRight + +-- TODO: This name is not quite correct, because the functor is not cartesian +-- rather, it takes a commutative square in `R.Over I` that is a pullback in the (whole!) +-- over category `Over I` to +-- a commutative square that is a pullback in the over category `Over O` +-- This subtlety can be ignored when `R.Over I = Over I`, like in the π-clan `UvPoly` case. + +-- Here are some relevant facts: +-- 1. partial right adjoints preserve limits in the whole category of diagrams from the subcategory +-- whole limit also lands in the subcategory, +-- hence `pullback i : R.Over I -> R.Over E` and +-- `pushforward p : R.Over E -> R.Over B` both preserve pullbacks in `Over I` +-- that are from `R.Over I`. +-- 2. `map : R.Over E -> R.Over O` also has this pullback preservation property. + +open NatTrans in +theorem isCartesian_cartesianNatTrans {E' B' : C} (P : MvPoly R I O E B) (P' : MvPoly R I O E' B') + [HasPullbacksAlong P.p] [R.HasPushforwardsAlong P.p] [R.IsStableUnderPushforwardsAlong P.p] + [HasPullbacksAlong P'.p] [R.HasPushforwardsAlong P'.p] [R.IsStableUnderPushforwardsAlong P'.p] + (δ : B ⟶ B') (φ : E ⟶ E') (hφ : P.i = φ ≫ P'.i) (pb : IsPullback φ P.p P'.p δ) + (hδ : δ ≫ P'.o = P.o) : + (cartesianNatTrans P P' δ φ hφ pb hδ).IsCartesian := + IsCartesian.vCompIsIso <| + IsCartesian.vCompIsIso <| + IsCartesian.comp + (isCartesian_pullbackMapTwoSquare ..) + (IsCartesian.whiskerLeft (isCartesian_of_isIso _) _) + + -- dsimp [cartesianNatTrans] + -- repeat apply IsCartesian.vComp + -- · apply IsCartesian.comp + -- · apply isCartesian_of_isIso + -- · sorry --apply isCartesian_of_isIso + -- · apply isCartesian_of_isIso + -- · -- apply IsCartesian.whiskerLeft + -- sorry + + -- NOTE: this lemma could be extracted, but `repeat' apply IsCartesian.comp` will unfold past it. + -- have : NatTrans.IsCartesian + -- (pullbackMapTwoSquare R P.o δ (𝟙 _) P'.o.1 P'.o.2 P.ho (by simp [hδ])) := by + -- -- unfold pullbackMapTwoSquare + -- -- simp only [mateEquiv_symm_apply] + -- repeat' apply IsCartesian.comp + -- -- have (i j : R.Over ⊤ B') (f : j ⟶ i) : + -- -- PreservesLimit + -- -- (cospan ((mapPullbackAdj R ⊤ P'.o.fst P'.o.snd trivial).unit.app i) + -- -- ((MorphismProperty.Over.map ⊤ P'.o.2 ⋙ MorphismProperty.Over.pullback R ⊤ P'.o.fst).map f)) + -- -- (MorphismProperty.Over.pullback R ⊤ δ ⋙ MorphismProperty.Over.map ⊤ P.ho) := sorry + -- any_goals apply isCartesian_of_isIso + -- · sorry --refine IsCartesian.whiskerRight _ _ + -- · apply IsCartesian.whiskerLeft + -- apply isCartesian_mapPullbackAdj_counit + + -- repeat' apply IsCartesian.comp + -- any_goals apply isCartesian_of_isIso + -- apply IsCartesian.whiskerLeft + -- repeat' apply IsCartesian.comp + -- any_goals apply isCartesian_of_isIso + -- apply IsCartesian.whiskerLeft + -- repeat' apply IsCartesian.comp + -- any_goals apply isCartesian_of_isIso + -- · sorry -- apply IsCartesian.whiskerRight + -- · apply IsCartesian.whiskerLeft + -- apply isCartesian_mapPullbackAdj_counit + + +end MvPoly + +/-- `P : UvPoly R E B` is the type of signatures for polynomial functors + p + E ---> B + +We read this as `∑ b : B, X ^ (E b)`, +for some `R`-object `X` (meaning the unique map to the terminal object is in `R`). + +This notion of polynomial makes sense when `R` is a π-clan, +[see Joyal, def 2.4.1](https://arxiv.org/pdf/1710.10238). +Therefore it will typically be used with the following instances + +- For pullback of `R`-maps along `p` we need + `[R.IsStableUnderBaseChange] [R.HasPullbacks]` +- For the left adjoint to pullback along `B`, we assume `[R.IsStableUnderComposition]` + and `[R.HasObjects]`, meaning the unique map `B ⟶ ⊤_ C` is in `R`. + For this, we will also assume `[ChosenTerminal C]`. +- For pushforward of `R`-maps along `p` we need + `[R.IsStableUnderPushforward R] [R.HasPushforwards R]` +- For pushforward of `R`-maps along `p` we also assume `[R.HasPullbacks]`. + This is useful - it makes the `R`-restricted pushforward of `R`-maps along `p` + a partial left adjoint to *global* pullback along `p`, + ``` + pushforward p + R.Over E -----> R.Over B + | | + | ⊥ | + | | + V V + C/E <--------- C/B + pullback p + ``` + which is strictly stronger than just having a left adjoint to `R`-restricted pullback + `(pullback : R.Over B ⥤ R.Over E) ⊣ (pushforward : R.Over E ⥤ R.Over B)`. +-/ +structure UvPoly (R : MorphismProperty C) (E B : C) where + (p : E ⟶ B) + (morphismProperty : R p) + +namespace UvPoly + +section + +variable {R : MorphismProperty C} {E B : C} + +variable [ChosenTerminal C] + +open ChosenTerminal + +variable (P : UvPoly R E B) + [R.IsStableUnderComposition] [R.HasPullbacks] [R.IsStableUnderBaseChange] [R.HasObjects] + [HasPullbacksAlong P.p] [R.IsStableUnderPushforwardsAlong P.p] [R.HasPushforwardsAlong P.p] + +instance (P : UvPoly R E B) : HasPullbacksAlong P.p := + hasPullbacksAlong_of_hasPullbacks P.morphismProperty + +instance (P : UvPoly R E B) {Γ : C} (A : Γ ⟶ B) : HasPullback P.p A := + hasPullback_symmetry _ _ + +lemma isTerminal_from (X : C) : R (isTerminal.from X) := + HasObjects.obj_mem _ ChosenTerminal.isTerminal + +@[simp] +abbrev toOverTerminal : C ⥤ R.Over ⊤ (𝟭_ C) := + (equivalenceOfHasObjects R isTerminal).inverse + +@[simp] +abbrev fromOverTerminal : R.Over ⊤ (𝟭_ C) ⥤ C := + (equivalenceOfHasObjects R isTerminal).functor + +@[simps] +def mvPoly : MvPoly R (𝟭_ C) (𝟭_ C) E B where + i := isTerminal.from _ + hi := isTerminal_from _ + p := P.p + o := isTerminal.from _ + ho := isTerminal_from _ + +instance : HasPullbacksAlong P.mvPoly.p := + inferInstanceAs <| HasPullbacksAlong P.p + +instance : R.HasPushforwardsAlong P.mvPoly.p := + inferInstanceAs <| R.HasPushforwardsAlong P.p + +instance : R.IsStableUnderPushforwardsAlong P.mvPoly.p := + inferInstanceAs <| R.IsStableUnderPushforwardsAlong P.p + +def functor : C ⥤ C := + toOverTerminal ⋙ + MvPoly.functor P.mvPoly ⋙ + fromOverTerminal + +/-- The action of a univariate polynomial on objects. -/ +def apply [ChosenTerminal C] : C → C := P.functor.obj + +@[inherit_doc] +infix:90 " @ " => apply + +-- instance [ChosenTerminal C] (P : UvPoly R E B) : +-- Limits.PreservesLimitsOfShape WalkingCospan P.functor := by +-- unfold functor +-- infer_instance + +variable (B) + +/-- The identity polynomial functor in single variable. -/ +@[simps!] +def id (R : MorphismProperty C) [R.ContainsIdentities] (B) : UvPoly R B B := ⟨𝟙 B, R.id_mem _ ⟩ + +@[simps!] +def vcomp [R.IsStableUnderComposition] {A B C} (P : UvPoly R A B) (Q : UvPoly R B C) : + UvPoly R A C := + ⟨ P.p ≫ Q.p, R.comp_mem _ _ P.morphismProperty Q.morphismProperty ⟩ + +variable {B} + +/-- The fstProjection morphism from `∑ b : B, X ^ (E b)` to `B` again. -/ +def fstProj (X : C) : P @ X ⟶ B := + (P.mvPoly.fstProj (toOverTerminal.obj X)).hom + +@[reassoc (attr := simp)] +lemma map_fstProj {X Y : C} (f : X ⟶ Y) : + P.functor.map f ≫ fstProj P Y = fstProj P X := + P.mvPoly.map_fstProj (toOverTerminal.map f) + +/-- The second projection morphism from `P @ X = ∑ b : B, X ^ (E b)` to `X^ (E b)`. -/ +def sndProj (X : C) : + Limits.pullback (fstProj P X) P.p ⟶ X := + (P.mvPoly.sndProj (toOverTerminal.obj X)).left + +lemma sndProj_comp {X Y : C} (f : X ⟶ Y) : sndProj P X ≫ f = + pullback.map _ _ _ _ (P.functor.map f) (𝟙 _) (𝟙 _) (by simp) (by simp) ≫ sndProj P Y := + P.mvPoly.sndProj_comp (toOverTerminal.map f) + +open TwoSquare + +/-- A commutative triangle +``` + I + ↗ ↖ +P.i/ \Q.i + / ρ \ + E -------> F + \ / +P.p\ / Q.p + ↘ ↙ + B +``` +induces a natural transformation `Q.functor ⟶ P.functor ` obtained by pasting the following 2-cells +``` + Q.mvPoly.functor +C --- ≅ ---> R.Over ⊤ 1 ----> R.Over ⊤ 1 --- ≅ ---> C +‖ ‖ ‖ ‖ +‖ ‖ ‖ ‖ +‖ ‖ ↓ ‖ ‖ +‖ ‖ ‖ ‖ +‖ ‖ ‖ ‖ +C --- ≅ ---> R.Over ⊤ 1 ----> R.Over ⊤ 1 --- ≅ ---> C + P.mvPoly.functor +``` +-/ +def verticalNatTrans {F : C} (Q : UvPoly R F B) (ρ : E ⟶ F) + [R.IsStableUnderPushforwardsAlong Q.p] [R.HasPushforwardsAlong Q.p] + (h : P.p = ρ ≫ Q.p) : Q.functor ⟶ P.functor := + let mv : Q.mvPoly.functor ⟶ P.mvPoly.functor := + MvPoly.verticalNatTrans P.mvPoly Q.mvPoly ρ (isTerminal.hom_ext ..) h (isTerminal.hom_ext ..) + (toOverTerminal).whiskerLeft (Functor.whiskerRight mv fromOverTerminal) + +open TwoSquare + +/-- A cartesian map of polynomials +``` + φ + E --------> E' + | | + P.p | (pb) | P'.p + v v + B --------> B' + δ +``` +induces a natural transformation between their associated functors obtained by pasting the following +2-cells +``` + P'.p +C --- > R.Over E' ----> R.Over B' -----> C +‖ | | ‖ +‖ ↗ | φ* ≅ | δ* ↗ ‖ +‖ v v ‖ +C --- > R.Over E -----> R.Over B -----> C + P.p +``` +-/ +def cartesianNatTrans {E' B' : C} (P' : UvPoly R E' B') + [R.IsStableUnderPushforwardsAlong P'.p] [R.HasPushforwardsAlong P'.p] + (δ : B ⟶ B') (φ : E ⟶ E') (pb : IsPullback φ P.p P'.p δ) : P.functor ⟶ P'.functor := + let mv := P.mvPoly.cartesianNatTrans P'.mvPoly δ φ (isTerminal.hom_ext ..) + pb (isTerminal.hom_ext ..) + (toOverTerminal).whiskerLeft (Functor.whiskerRight mv fromOverTerminal) + +-- TODO: this is cartesian. Unlike with the MvPoly case there is no distinction between +-- `C` and `Over.terminal` and `R.Over terminal`, since `R` has objects. + +open NatTrans in +theorem isCartesian_cartesianNatTrans {D F : C} (Q : UvPoly R F D) + [R.IsStableUnderPushforwardsAlong Q.p] [R.HasPushforwardsAlong Q.p] + (δ : B ⟶ D) (φ : E ⟶ F) (pb : IsPullback φ P.p Q.p δ) : + (cartesianNatTrans P Q δ φ pb).IsCartesian := by + apply IsCartesian.whiskerLeft + apply IsCartesian.whiskerRight + apply MvPoly.isCartesian_cartesianNatTrans + +/-- A morphism from a polynomial `P` to a polynomial `Q` is a pair of morphisms `e : E ⟶ E'` +and `b : B ⟶ B'` such that the diagram +``` + E -- P.p -> B + ^ | + ρ | | + | ψ | + Pb --------> B + | | + φ | | δ + v v + F -- Q.p -> D +``` +is a pullback square. -/ +structure Hom {F D : C} (P : UvPoly R E B) (Q : UvPoly R F D) where + Pb : C + δ : B ⟶ D + φ : Pb ⟶ F + ψ : Pb ⟶ B + ρ : Pb ⟶ E + is_pb : IsPullback ψ φ δ Q.p + w : ρ ≫ P.p = ψ + +namespace Hom + +open IsPullback + +/-- The identity morphism in the category of polynomials. -/ +def id (P : UvPoly R E B) : Hom P P := ⟨E, 𝟙 B, 𝟙 _ , P.p , 𝟙 _, IsPullback.of_id_snd, by simp⟩ + +end Hom + +/-- The domain of the composition of two polynomial signatures. +See `UvPoly.comp`. -/ +def compDom {E' B' : C} (P' : UvPoly R E' B') + [R.IsStableUnderPushforwardsAlong P'.p] [R.HasPushforwardsAlong P'.p] : C := + Limits.pullback (sndProj P B') P'.p + +/-- +The composition of two polynomial signatures. See `UvPoly.comp`. +Note that this is not just composition in the category `C`, +instead it is functor composition in the category `C ⥤ C`, +meaning it satisfies `P.functor ⋙ P'.functor ≅ (comp P P').functor`. + + E' <---- compDom + | | +p' | (pb) | + | | + V V + B' <----- • -------> E + sndProj | | + | (pb) |p + | | + V V + P @ B' -----> B + fstProj +-/ +def comp {E' B' : C} (P' : UvPoly R E' B') + [R.IsStableUnderPushforwardsAlong P'.p] [R.HasPushforwardsAlong P'.p] : + UvPoly R (compDom P P') (P @ B') where + p := Limits.pullback.fst (sndProj P B') P'.p ≫ pullback.fst (fstProj P B') P.p + morphismProperty := R.comp_mem _ _ + (R.of_isPullback (IsPullback.of_hasPullback (sndProj P B') P'.p).flip P'.morphismProperty) + (R.of_isPullback (IsPullback.of_hasPullback (fstProj P B') P.p).flip P.morphismProperty) + +namespace Equiv + +variable {P} {Γ X Y : C} + +/-- Convert the morphism `pair` into a morphism in the over category `Over (𝟭_ C)` -/ +@[simp] +abbrev homMk (pair : Γ ⟶ P @ X) : Over.mk (isTerminal.from Γ) ⟶ + ((toOverTerminal ⋙ MvPoly.functor P.mvPoly).obj X).toComma := + Over.homMk pair (isTerminal.hom_ext ..) + +/-- +A morphism `pair : Γ ⟶ P @ X` is equivalent to a pair of morphisms +`fst : Γ ⟶ B` and `snd : pb ⟶ X` in the following diagram +``` + snd +B <---- pb ------> E + | | + | |p + | | + V V + Γ -------> B + fst +``` +The following API allows users to convert back and forth along this (natural) bijection. +-/ +def fst (pair : Γ ⟶ P @ X) : Γ ⟶ B := + (MvPoly.Equiv.fst (homMk pair)).hom + +lemma fst_eq (pair : Γ ⟶ P @ X) : fst pair = pair ≫ P.fstProj X := by + aesop_cat + +def snd (pair : Γ ⟶ P @ X) : Limits.pullback (fst pair) P.p ⟶ X := + (MvPoly.Equiv.snd (homMk pair)).left + +lemma snd_eq (pair : Γ ⟶ P @ X) : snd pair = + Limits.pullback.map (fst pair) P.p (P.fstProj X) P.p pair (𝟙 E) (𝟙 B) (by simp [fst_eq]) + (by simp) ≫ sndProj P X := by + simpa [Limits.pullback.map] using congrArg CommaMorphism.left (MvPoly.Equiv.snd_eq (homMk pair)) + +def snd' (pair : Γ ⟶ P @ X) {pb f g} (H : IsPullback (P := pb) f g (fst pair) P.p) : pb ⟶ X := + H.isoPullback.hom ≫ snd pair + +theorem snd_eq_snd' (pair : Γ ⟶ P @ X) : snd pair = snd' pair (.of_hasPullback ..) := + by simp [snd'] + +/-- Convert the morphism `x` into a morphism in the over category `Over (𝟭_ C)` -/ +@[simp] +abbrev mkAux (b : Γ ⟶ B) (x : pullback b P.p ⟶ X) : + (PolynomialPartialAdjunction.leftAdjoint P.mvPoly.i P.mvPoly.p).obj (Over.mk b) ⟶ + ((toOverTerminal (R := R)).obj X).toComma := + Over.homMk x (isTerminal.hom_ext ..) + +def mk (b : Γ ⟶ B) (x : pullback b P.p ⟶ X) : Γ ⟶ P @ X := + (MvPoly.Equiv.mk (P := P.mvPoly) (Γ := Over.mk (isTerminal.from Γ)) + (Over.mk b) (by congr; apply isTerminal.hom_ext) (mkAux b x)).left + +def mk' (b : Γ ⟶ B) {pb f g} (H : IsPullback (P := pb) f g b P.p) (x : pb ⟶ X) : Γ ⟶ P @ X := + mk b (H.isoPullback.inv ≫ x) + +theorem mk_eq_mk' (b : Γ ⟶ B) (x : pullback b P.p ⟶ X) : + mk b x = mk' b (.of_hasPullback ..) x := by simp [mk'] + +@[simp] +lemma fst_mk (b : Γ ⟶ B) (x : pullback b P.p ⟶ X) : + fst (mk b x) = b := by + simp only [fst, mk, Over.homMk_eta] + rw! (castMode := .all) [MvPoly.Equiv.fst_mk] + simp [← heq_eq_eq]; rfl + +@[simp] +lemma fst_mk' (b : Γ ⟶ B) {pb f g} (H : IsPullback (P := pb) f g b P.p) (x : pb ⟶ X) : + fst (mk' b H x) = b := by + simp [mk'] + +@[simp] +lemma mk'_comp_fstProj (b : Γ ⟶ B) {pb f g} (H : IsPullback (P := pb) f g b P.p) (x : pb ⟶ X) : + mk' b H x ≫ P.fstProj X = b := by + simp [← fst_eq] + +theorem fst_comp_left (pair : Γ ⟶ P @ X) {Δ} (f : Δ ⟶ Γ) : + fst (f ≫ pair) = f ≫ fst pair := by simp [fst_eq] + +theorem fst_comp_right (pair : Γ ⟶ P @ X) (f : X ⟶ Y) : + fst (pair ≫ P.functor.map f) = fst pair := by + simp [fst_eq] + +lemma snd'_eq (pair : Γ ⟶ P @ X) {pb f g} (H : IsPullback (P := pb) f g (fst pair) P.p) : + snd' pair H = pullback.lift (f ≫ pair) g (by simpa using H.w) ≫ sndProj P X := by + rw [snd', snd_eq, ← Category.assoc] + congr 1 + ext <;> simp + +/-- Switch the selected pullback `pb` used in `UvPoly.Equiv.snd'` with a different pullback `pb'`. -/ +lemma snd'_eq_snd' (pair : Γ ⟶ P @ X) {pb f g} (H : IsPullback (P := pb) f g (fst pair) P.p) + {pb' f' g'} (H' : IsPullback (P := pb') f' g' (fst pair) P.p) : + snd' pair H = (H.isoIsPullback _ _ H').hom ≫ snd' pair H' := by + simp [snd'_eq, ← Category.assoc] + congr 2 + ext <;> simp + +@[simp] +lemma snd_mk (b : Γ ⟶ B) (x : pullback b P.p ⟶ X) : snd (mk b x) = + eqToHom (by simp) ≫ x := by + have := MvPoly.Equiv.snd_mk (P := P.mvPoly) (Γ := Over.mk (isTerminal.from Γ)) + (Over.mk b) (by congr; apply isTerminal.hom_ext) (mkAux b x) + convert congr_arg CommaMorphism.left this + simp + +@[simp] +lemma snd'_mk' (b : Γ ⟶ B) {pb f g} (H : IsPullback (P := pb) f g b P.p) (x : pb ⟶ X) : + snd' (mk' b H x) (by rwa [fst_mk']) = x := by + simp only [snd', mk', snd_mk] + rw! [fst_mk] + simp + +@[simp] +lemma snd'_mk'' (b : Γ ⟶ B) {pb f g} (H : IsPullback (P := pb) f g b P.p) (x : pb ⟶ X) + {pb' f' g'} (H' : IsPullback (P := pb') f' g' (fst (mk' b H x)) P.p := by exact H) : + snd' (mk' b H x) H' = H.lift f' g' (by rw [fst_mk'] at H'; simp [H'.w]) ≫ x := by + simp only [snd', mk', snd_mk] + rw! [fst_mk] + simp [← Category.assoc] + congr 1 + apply H.hom_ext <;> simp + + +lemma snd_mk_heq (b : Γ ⟶ B) (x : pullback b P.p ⟶ X) : + snd (mk b x) ≍ x := by + simp + +theorem snd'_comp_left (pair : Γ ⟶ P @ X) + {pb f g} (H : IsPullback (P := pb) f g (fst pair) P.p) + {Δ} (σ : Δ ⟶ Γ) + {pb' f' g'} (H' : IsPullback (P := pb') f' g' (σ ≫ fst pair) P.p) : + snd' (σ ≫ pair) (by convert H'; rw [fst_comp_left]) = + H.lift (f' ≫ σ) g' (by simp [H'.w]) ≫ snd' pair H := by + simp only [snd'_eq, ← Category.assoc] + congr 2 + ext + · simp + · simp + +theorem snd'_comp_right (pair : Γ ⟶ P @ X) (f : X ⟶ Y) + {pb f1 f2} (H : IsPullback (P := pb) f1 f2 (fst pair) P.p) : + snd' (pair ≫ P.functor.map f) (by rwa [fst_comp_right]) = + snd' pair H ≫ f := by + simp only [snd'_eq, assoc] + conv => right; rw [sndProj_comp, ← Category.assoc] + congr 1 + ext <;> simp + +theorem snd_comp_right (pair : Γ ⟶ P @ X) (f : X ⟶ Y) : snd (pair ≫ P.functor.map f) = + eqToHom (by congr 1; apply fst_comp_right) ≫ snd pair ≫ f := by + simp only [snd_eq, assoc, sndProj_comp] + conv => right; simp only [← Category.assoc] + congr 1 + have : fst (pair ≫ P.functor.map f) = fst pair := by simp [fst_eq] + rw! [this] + ext <;> simp + +@[simp] +lemma eta (pair : Γ ⟶ P @ X) : + mk (fst pair) (snd pair) = pair := by + have := MvPoly.Equiv.eta (P := P.mvPoly) (Γ := Over.mk (isTerminal.from Γ)) (homMk pair) + exact congr_arg CommaMorphism.left this + +@[simp] +lemma eta' (pair : Γ ⟶ P @ X) + {pb f1 f2} (H : IsPullback (P := pb) f1 f2 (fst pair) P.p) : + mk' (fst pair) H (snd' pair H) = pair := by + simp only [mk', snd'] + simp + +lemma ext' {pair₁ pair₂ : Γ ⟶ P @ X} + {pb f g} (H : IsPullback (P := pb) f g (fst pair₁) P.p) + (h1 : fst pair₁ = fst pair₂) + (h2 : snd' pair₁ H = snd' pair₂ (by rwa [h1] at H)) : + pair₁ = pair₂ := by + rw [← eta' pair₁ H, ← eta' pair₂ (by rwa [h1] at H), h2] + rw! [h1] + +/-- Switch the selected pullback `pb` used in `UvPoly.Equiv.mk'` with a different pullback `pb'`. -/ +theorem mk'_eq_mk' (b : Γ ⟶ B) {pb f g} (H : IsPullback (P := pb) f g b P.p) (x : pb ⟶ X) + {pb' f' g'} (H' : IsPullback (P := pb') f' g' b P.p) : + mk' b H x = mk' b H' ((IsPullback.isoIsPullback _ _ H H').inv ≫ x) := by + apply ext' (R := R) (f := f) (g := g) (by convert H; simp) + · have : ∀ h, H'.lift f g h ≫ (IsPullback.isoIsPullback Γ E H H').inv = 𝟙 pb := by + intro ; apply H.hom_ext <;> simp + simp [← Category.assoc, this] + · simp + +lemma mk'_comp_right (b : Γ ⟶ B) {pb f1 f2} (H : IsPullback (P := pb) f1 f2 b P.p) (x : pb ⟶ X) + (f : X ⟶ Y) : mk' b H x ≫ P.functor.map f = mk' b H (x ≫ f) := by + refine .symm <| ext' (by rwa [fst_mk']) (by simp [fst_comp_right]) ?_ + rw [snd'_comp_right (H := by rwa [fst_mk'])]; simp + +lemma mk_comp_right (b : Γ ⟶ B) (x : pullback b P.p ⟶ X) (f : X ⟶ Y) : + mk b x ≫ P.functor.map f = mk b (x ≫ f) := by + simp [mk_eq_mk', mk'_comp_right] + +theorem mk'_comp_left {Δ} + (b : Γ ⟶ B) {pb f g} (H : IsPullback f g b P.p) (x : pb ⟶ X) (σ : Δ ⟶ Γ) + (σb) (eq : σ ≫ b = σb) + {pb' f' g'} (H' : IsPullback (P := pb') f' g' σb P.p) : + σ ≫ UvPoly.Equiv.mk' b H x = UvPoly.Equiv.mk' σb H' + (H.lift (f' ≫ σ) g' (by simp [eq, H'.w]) ≫ x) := by + apply ext' (f := f') (g := g') (H := by convert H'; simp [eq, fst_eq]) + · rw [snd'_comp_left (H := by convert H; rw [fst_mk']) (H' := by convert H'; rw [← eq, fst_mk'])] + simp + · simp [eq, fst_comp_left] + +theorem mk_comp_left {Δ} (b : Γ ⟶ B) (x : pullback b P.p ⟶ X) (σ: Δ ⟶ Γ) : + σ ≫ UvPoly.Equiv.mk b x = + UvPoly.Equiv.mk (σ ≫ b) + (pullback.map _ _ _ _ σ (𝟙 _) (𝟙 _) (by simp) (by simp) ≫ x) := by + simp only [mk_eq_mk'] + rw [mk'_comp_left (H := .of_hasPullback _ _) (H' := .of_hasPullback _ _) (eq := rfl)] + congr 2; ext <;> simp + +lemma mk'_comp_cartesianNatTrans_app {E' B' Γ X : C} {P' : UvPoly R E' B'} + [R.IsStableUnderPushforwardsAlong P'.p] [R.HasPushforwardsAlong P'.p] + (y : Γ ⟶ B) (pb f g) (H : IsPullback (P := pb) f g y P.p) + (x : pb ⟶ X) (e : E ⟶ E') (b : B ⟶ B') + (hp : IsPullback P.p e b P'.p) : + Equiv.mk' y H x ≫ (P.cartesianNatTrans P' b e hp.flip).app X = + Equiv.mk' (y ≫ b) (H.paste_vert hp) x := by + sorry + -- have : fst (Equiv.mk' y H x ≫ (P.cartesianNatTrans P' b e hp.flip).app X) = y ≫ b := by + -- rw [fst_eq, Category.assoc, cartesianNatTrans_fstProj, ← Category.assoc, mk'_comp_fstProj] + -- refine ext' _ _ (this ▸ H.paste_vert hp) (by simpa) ?_ + -- simp; rw [snd'_eq] + -- have := snd'_mk' P X y H x + -- rw [snd'_eq, ← fan_snd_map' _ _ X hp] at this + -- refine .trans ?_ this + -- simp only [← Category.assoc]; congr 1; ext <;> simp + +end Equiv + +namespace compDomEquiv + +variable {Γ E' B' : C} {P} {P' : UvPoly R E' B'} + [R.IsStableUnderPushforwardsAlong P'.p] [R.HasPushforwardsAlong P'.p] + +/- +``` + Γ + | + |triple + V + compDom + |⟍ + | ⟍ + | ⟍ + V ↘ + • -------> E + | | + | (pb) |p + | | + V V +P @ B' -----> B + fstProj +``` +This produces a map `fst : Γ ⟶ E`, +and a map `(triple ≫ P.comp P').p : Γ ⟶ P @ B'`, +which we can further break up using `UvPoly.Equiv.fst` and `UvPoly.Equiv.snd`. +``` + dependent +B <---- pb ------> E + | | + | |p + | | + V V + Γ -------> B + base +``` +-/ +def fst (triple : Γ ⟶ compDom P P') : Γ ⟶ E := + triple ≫ pullback.fst _ _ ≫ pullback.snd _ _ + +@[simp] +abbrev base (triple : Γ ⟶ compDom P P') : Γ ⟶ B := Equiv.fst (triple ≫ (P.comp P').p) + +theorem fst_comp_p (triple : Γ ⟶ compDom P P') : + fst triple ≫ P.p = base triple := by + simp [fst, Equiv.fst_eq, pullback.condition, comp] + +abbrev dependent (triple : Γ ⟶ compDom P P') {pb} (f : pb ⟶ Γ) (g : pb ⟶ E) + (H : IsPullback f g (fst triple ≫ P.p) P.p) : pb ⟶ B' := + Equiv.snd' (triple ≫ (P.comp P').p) (by convert H; simp only [fst_comp_p]) + +def snd (triple : Γ ⟶ compDom P P') : Γ ⟶ E' := + triple ≫ pullback.snd _ _ + +theorem snd_comp_p (triple : Γ ⟶ compDom P P') + {pb} (f : pb ⟶ Γ) (g : pb ⟶ E) (H : IsPullback f g (fst triple ≫ P.p) P.p) : + snd triple ≫ P'.p = + H.lift (𝟙 Γ) (fst triple) (by simp) ≫ dependent triple f g H := + calc (triple ≫ pullback.snd _ _) ≫ P'.p + _ = triple ≫ pullback.fst _ _ ≫ sndProj P B' := by + simp [pullback.condition] + _ = H.lift (𝟙 Γ) (fst triple) (by simp) ≫ dependent triple f g H := by + simp only [← assoc, dependent, comp, Equiv.snd'_eq] + congr 1 + ext <;> simp [fst] + +def mk (b : Γ ⟶ B) (e : Γ ⟶ E) (he : e ≫ P.p = b) + {pb} (f : pb ⟶ Γ) (g : pb ⟶ E) (H : IsPullback f g b P.p) + (b' : pb ⟶ B') (e' : Γ ⟶ E') (he' : e' ≫ P'.p = H.lift (𝟙 Γ) e (by simp [he]) ≫ b') : + Γ ⟶ P.compDom P' := + pullback.lift (pullback.lift (Equiv.mk' b H b') e) e' (by + have : b' = Equiv.snd' (Equiv.mk' b H b') (by convert H; simp) := by rw [Equiv.snd'_mk'] + conv => right; rw [he', this, Equiv.snd'_eq, ← Category.assoc] + congr 1 + ext <;> simp ) + +lemma mk_comp (b : Γ ⟶ B) (e : Γ ⟶ E) (he : e ≫ P.p = b) + {pb} (f : pb ⟶ Γ) (g : pb ⟶ E) (H : IsPullback f g b P.p) + (b' : pb ⟶ B') (e' : Γ ⟶ E') (he' : e' ≫ P'.p = H.lift (𝟙 Γ) e (by simp [he]) ≫ b') : + mk b e he f g H b' e' he' ≫ (P.comp P').p = Equiv.mk' b H b' := by + simp [mk, comp] + +@[simp] +lemma base_mk (b : Γ ⟶ B) (e : Γ ⟶ E) (he : e ≫ P.p = b) + {pb} (f : pb ⟶ Γ) (g : pb ⟶ E) (H : IsPullback f g b P.p) + (b' : pb ⟶ B') (e' : Γ ⟶ E') (he' : e' ≫ P'.p = H.lift (𝟙 Γ) e (by simp [he]) ≫ b') : + base (mk b e he f g H b' e' he') = b := by simp [mk, comp] + +@[simp] +lemma fst_mk (b : Γ ⟶ B) (e : Γ ⟶ E) (he : e ≫ P.p = b) + {pb} (f : pb ⟶ Γ) (g : pb ⟶ E) (H : IsPullback f g b P.p) + (b' : pb ⟶ B') (e' : Γ ⟶ E') (he' : e' ≫ P'.p = H.lift (𝟙 Γ) e (by simp [he]) ≫ b') : + fst (mk b e he f g H b' e' he') = e := by + simp [mk, fst] + +@[simp] +lemma dependent_mk (b : Γ ⟶ B) (e : Γ ⟶ E) (he : e ≫ P.p = b) + {pb} (f : pb ⟶ Γ) (g : pb ⟶ E) (H : IsPullback f g b P.p) + (b' : pb ⟶ B') (e' : Γ ⟶ E') (he' : e' ≫ P'.p = H.lift (𝟙 Γ) e (by simp [he]) ≫ b') + {pb'} (f' : pb' ⟶ Γ) (g' : pb' ⟶ E) + (H' : IsPullback f' g' (fst (mk b e he f g H b' e' he') ≫ P.p) P.p) : + dependent (mk b e he f g H b' e' he') f' g' H' = H.lift f' g' (by simp [← H'.w, he]) ≫ b' := by + simp [mk, dependent, comp] + +@[simp] +lemma snd_mk (b : Γ ⟶ B) (e : Γ ⟶ E) (he : e ≫ P.p = b) + {pb} (f : pb ⟶ Γ) (g : pb ⟶ E) (H : IsPullback f g b P.p) + (b' : pb ⟶ B') (e' : Γ ⟶ E') (he' : e' ≫ P'.p = H.lift (𝟙 Γ) e (by simp [he]) ≫ b') : + snd (mk b e he f g H b' e' he') = e' := by + simp [mk, snd] + +@[simp] +lemma eta (triple : Γ ⟶ compDom P P') {pb} (f : pb ⟶ Γ) (g : pb ⟶ E) + (H : IsPullback f g (base triple) P.p) (b' : pb ⟶ B') + (hbase' : b' = Equiv.snd' (triple ≫ (P.comp P').p) H) : + mk (base triple) (fst triple) (fst_comp_p ..) f g H b' (snd triple) (by + simp only [snd, assoc, ← pullback.condition, base, comp] + simp only [hbase', Equiv.snd'_eq, ← Category.assoc] + congr 1 + ext <;> simp [fst, comp]) = triple := by + apply pullback.hom_ext + · ext + · simp [mk] + conv => right; rw [← Equiv.eta' + (triple ≫ pullback.fst (P.sndProj B') P'.p ≫ pullback.fst (P.fstProj B') P.p) H] + congr + · simp [mk, fst] + · simp [mk, snd] + +lemma ext (triple triple' : Γ ⟶ compDom P P') + (hfst : fst triple = fst triple') + (hsnd : snd triple = snd triple') + {pb} (f : pb ⟶ Γ) (g : pb ⟶ E) + (H : IsPullback f g (fst triple ≫ P.p) P.p) + (hd : dependent triple f g H = dependent triple' f g (by rwa [← hfst])) : + triple = triple' := by + rw [← eta triple f g (by convert H; simp [fst_comp_p]) (dependent triple f g H) rfl, + ← eta triple' f g (by rwa [← fst_comp_p, ← hfst]) + (dependent triple' f g (by rwa [← hfst])) rfl] + have : base triple = base triple' := by + rw [← fst_comp_p, ← fst_comp_p, hfst] + rw! [hsnd, hd, hfst, this] + +lemma fst_comp {Δ} (σ : Δ ⟶ Γ) (triple : Γ ⟶ compDom P P') : + fst (σ ≫ triple) = σ ≫ fst triple := by + simp [fst] + +lemma snd_comp {Δ} (σ : Δ ⟶ Γ) (triple : Γ ⟶ compDom P P') : + snd (σ ≫ triple) = σ ≫ snd triple := by + simp [snd] + +lemma dependent_comp {Δ} (σ : Δ ⟶ Γ) (triple : Γ ⟶ compDom P P') + {pb'} (f' : pb' ⟶ Γ) (g' : pb' ⟶ E) (H' : IsPullback f' g' (fst triple ≫ P.p) P.p) + {pb} (f : pb ⟶ Δ) (g : pb ⟶ E) (H : IsPullback f g (fst (σ ≫ triple) ≫ P.p) P.p) : + dependent (σ ≫ triple) f g H = H'.lift (f ≫ σ) g (by simp [← H.w, fst_comp]) ≫ + dependent triple f' g' H' := by + simp only [dependent, comp, ← assoc, Equiv.snd'_eq] + congr + ext <;> simp + +lemma comp_mk {Δ} (σ : Δ ⟶ Γ) (b : Γ ⟶ B) (e : Γ ⟶ E) (he : e ≫ P.p = b) + {pb'} (f' : pb' ⟶ Γ) (g' : pb' ⟶ E) (H' : IsPullback f' g' b P.p) + {pb} (f : pb ⟶ Δ) (g : pb ⟶ E) (H : IsPullback f g (σ ≫ b) P.p) + (b' : pb' ⟶ B') (e' : Γ ⟶ E') (he' : e' ≫ P'.p = H'.lift (𝟙 Γ) e (by simp [he]) ≫ b') : + σ ≫ mk b e he f' g' H' b' e' he' = + mk (σ ≫ b) (σ ≫ e) (by simp [he]) f g H (H'.lift (f ≫ σ) g (by simp[← H.w]) ≫ b') (σ ≫ e') + (by simp [he']; simp [← assoc]; congr 1; apply H'.hom_ext <;> simp) := by + simp [mk] + apply pullback.hom_ext + · apply pullback.hom_ext + · simp only [assoc, limit.lift_π, PullbackCone.mk_pt, PullbackCone.mk_π_app] + rw [Equiv.mk'_comp_left] + rfl + · simp + · simp + +end compDomEquiv + +section + +variable {F : C} (Q : UvPoly R F B) + [R.HasPushforwardsAlong Q.p] [R.IsStableUnderPushforwardsAlong Q.p] + (ρ : E ⟶ F) (h : P.p = ρ ≫ Q.p) + +lemma fst_verticalNatTrans_app {Γ : C} (X : C) (pair : Γ ⟶ Q @ X) : + Equiv.fst (pair ≫ (verticalNatTrans P Q ρ h).app X) = Equiv.fst pair := by + dsimp [Equiv.fst] + sorry + +lemma snd'_verticalNatTrans_app {Γ : C} (X : C) (pair : Γ ⟶ Q @ X) {R f g} + (H : IsPullback (P := R) f g (Equiv.fst pair) Q.p) {R' f' g'} + (H' : IsPullback (P := R') f' g' (Equiv.fst pair) P.p) : + Equiv.snd' (pair ≫ (verticalNatTrans P Q ρ h).app X) (by + rw [← fst_verticalNatTrans_app P Q] at H' + exact H') = + (H.lift f' (g' ≫ ρ) (by simp [H'.w, h])) ≫ + Equiv.snd' pair H := + sorry + +lemma mk'_comp_verticalNatTrans_app {Γ : C} (X : C) (b : Γ ⟶ B) {R f g} + (H : IsPullback (P := R) f g b Q.p) (x : R ⟶ X) {R' f' g'} + (H' : IsPullback (P := R') f' g' b P.p) : + Equiv.mk' b H x ≫ (verticalNatTrans P Q ρ h).app X = Equiv.mk' b H' + (H.lift f' (g' ≫ ρ) (by simp [H'.w, h]) ≫ x) := + sorry + +end + +-- instance preservesPullbacks (P : UvPoly R E B) {Pb X Y Z : C} (fst : Pb ⟶ X) (snd : Pb ⟶ Y) +-- (f : X ⟶ Z) (g : Y ⟶ Z) (h: IsPullback fst snd f g) : +-- IsPullback (P.functor.map fst) (P.functor.map snd) (P.functor.map f) (P.functor.map g) := +-- P.functor.map_isPullback h diff --git a/HoTTLean/ForMathlib/CategoryTheory/Yoneda.lean b/HoTTLean/ForMathlib/CategoryTheory/Yoneda.lean index f95ab0f8..028c8df7 100644 --- a/HoTTLean/ForMathlib/CategoryTheory/Yoneda.lean +++ b/HoTTLean/ForMathlib/CategoryTheory/Yoneda.lean @@ -1,4 +1,7 @@ import Mathlib.CategoryTheory.Yoneda +import HoTTLean.ForMathlib.CategoryTheory.Adjunction.Basic + +universe v₁ u₁ v₂ u₂ v₃ u₃ /-! Notation for the Yoneda embedding. -/ @@ -27,4 +30,72 @@ def Functor.map.unexpand : Unexpander throw () | _ => throw () +variable {C : Type u₁} [SmallCategory C] {F G : Cᵒᵖ ⥤ Type u₁} + (app : ∀ {X : C}, (yoneda.obj X ⟶ F) → (yoneda.obj X ⟶ G)) + (naturality : ∀ {X Y : C} (f : X ⟶ Y) (α : yoneda.obj Y ⟶ F), + app (yoneda.map f ≫ α) = yoneda.map f ≫ app α) + +variable (F) in + +/-- + A presheaf `F` on a small category `C` is isomorphic to + the hom-presheaf `Hom(y(•),F)`. +-/ +def yonedaIso : yoneda.op ⋙ yoneda.obj F ≅ F := + NatIso.ofComponents (fun _ => Equiv.toIso yonedaEquiv) + (fun f => by ext : 1; dsimp; rw [yonedaEquiv_naturality']) + +/-- Build natural transformations between presheaves on a small category + by defining their action when precomposing by a morphism with + representable domain -/ +def NatTrans.yonedaMk : F ⟶ G := + (yonedaIso F).inv ≫ .mk (fun _ => by exact app) ≫ (yonedaIso G).hom + +@[deprecated (since := "2025-11-20")] alias yonedaIsoMap := NatTrans.yonedaMk + +theorem NatTrans.yonedaMk_app {X : C} (α : yoneda.obj X ⟶ F) : + α ≫ yonedaMk app naturality = app α := by + rw [← yonedaEquiv.apply_eq_iff_eq, yonedaEquiv_comp] + simp [yonedaMk, yonedaIso] + +example : yoneda.op ⋙ y(F) ≅ F := curriedYonedaLemma'.app F + +example {D : Type*} [Category D] (S : D ⥤ Cᵒᵖ ⥤ Type u₁) := + S.isoWhiskerLeft curriedYonedaLemma' + +def NatIso.yonedaMk (α : yoneda.op ⋙ y(F) ≅ yoneda.op ⋙ y(G)) : F ≅ G := + (curriedYonedaLemma'.app F).symm ≪≫ α ≪≫ curriedYonedaLemma'.app G + +def NatIso.yonedaMk' (app : ∀ {X : C}, (yoneda.obj X ⟶ F) ≃ (yoneda.obj X ⟶ G)) + (naturality : ∀ {X Y : C} (f : X ⟶ Y) (α : yoneda.obj Y ⟶ F), + app (yoneda.map f ≫ α) = yoneda.map f ≫ app α) : F ≅ G := + (yonedaIso F).symm ≪≫ NatIso.ofComponents (fun A => by exact Equiv.toIso app) ≪≫ (yonedaIso G) + +/-- To show that `S ≅ T : D ⥤ Psh C` it suffices to prove the bijection + `Psh C (y(c), S d) ≅ Psh C (y(c), T d)`, + natural in both `c : Cᵒᵖ` and `d : D`. -/ +def functorToPresheafIsoMk {D : Type*} [Category D] {S T : D ⥤ Cᵒᵖ ⥤ Type u₁} + (α : S ⋙ yoneda ⋙ (Functor.whiskeringLeft Cᵒᵖ (Cᵒᵖ ⥤ Type u₁)ᵒᵖ (Type u₁)).obj yoneda.op ≅ + T ⋙ yoneda ⋙ (Functor.whiskeringLeft Cᵒᵖ (Cᵒᵖ ⥤ Type u₁)ᵒᵖ (Type u₁)).obj yoneda.op) : + S ≅ T := + (S.isoWhiskerLeft curriedYonedaLemma').symm ≪≫ α ≪≫ T.isoWhiskerLeft curriedYonedaLemma' + +namespace Equivalence + +variable {C : Type u₁} [Category.{v₁} C] {D : Type u₁} [Category.{v₁} D] + +def yonedaCompCongrLeftInverseIso (e : C ≌ D) : yoneda ⋙ (congrLeft e.op).inverse ≅ + e.inverse ⋙ yoneda := + NatIso.ofComponents + (fun _ => NatIso.ofComponents + (fun _ => Equiv.toIso (e.toAdjunction.homEquiv _ _)) + (fun _ => by ext; simp [Adjunction.homEquiv_naturality_left])) + (fun _ => by ext; simp [Adjunction.homEquiv_naturality_right]) + +def yonedaCompCongrLeftFunctorIso (e : C ≌ D) : yoneda ⋙ (congrLeft e.op).functor ≅ + e.functor ⋙ yoneda := + e.symm.yonedaCompCongrLeftInverseIso + +end Equivalence + end CategoryTheory diff --git a/HoTTLean/Model/Structured/StructuredUniverse.lean b/HoTTLean/Model/Structured/StructuredUniverse.lean new file mode 100644 index 00000000..740567bc --- /dev/null +++ b/HoTTLean/Model/Structured/StructuredUniverse.lean @@ -0,0 +1,923 @@ +import Mathlib.CategoryTheory.Limits.Shapes.KernelPair +import HoTTLean.ForMathlib +import HoTTLean.ForMathlib.Tactic.CategoryTheory.FunctorMap +import HoTTLean.ForMathlib.CategoryTheory.RepPullbackCone +import HoTTLean.ForMathlib.CategoryTheory.WeakPullback +import HoTTLean.ForMathlib.CategoryTheory.Polynomial +import HoTTLean.Model.Unstructured.UnstructuredUniverse + +universe v u + +noncomputable section + +open CategoryTheory Limits Opposite + +namespace Model + +/-- A natural model with support for dependent types (and nothing more). +The data is a natural transformation with representable fibers, +stored as a choice of representative for each fiber. -/ +structure StructuredUniverse {Ctx : Type u} [Category Ctx] (R : MorphismProperty Ctx) + extends UnstructuredUniverse Ctx where + morphismProperty : R tp + +namespace StructuredUniverse + +open Model.UnstructuredUniverse + +variable {Ctx : Type u} [Category Ctx] {R : MorphismProperty Ctx} (M : StructuredUniverse R) + [R.HasPullbacks] [R.IsStableUnderBaseChange] + +instance {Γ : Ctx} (A : Γ ⟶ M.Ty) : HasPullback A M.tp := + have := MorphismProperty.HasPullbacks.hasPullback A M.morphismProperty + hasPullback_symmetry _ _ + +@[simps! hom inv] +def pullbackIsoExt {Γ : Ctx} (A : Γ ⟶ M.Ty) : + pullback A M.tp ≅ (M.ext A) := + IsPullback.isoPullback (M.disp_pullback A).flip |>.symm + +/-! ## Pullback of representable natural transformation -/ + +/-- Pull a natural model back along a type. -/ +protected def pullback {Γ : Ctx} (A : Γ ⟶ M.Ty) : StructuredUniverse R where + __ := UnstructuredUniverse.pullback M.toUnstructuredUniverse A + morphismProperty := R.of_isPullback (disp_pullback ..) M.morphismProperty + +/-- + Given the pullback square on the right, + with a natural model structure on `tp : Tm ⟶ Ty` + giving the outer pullback square. + + Γ.A -.-.- var -.-,-> E ------ toTm ------> Tm + | | | + | | | + M.disp π tp + | | | + V V V + Γ ------- A -------> U ------ toTy ------> Ty + + construct a natural model structure on `π : E ⟶ U`, + by pullback pasting. +-/ +def ofIsPullback {U E : Ctx} {π : E ⟶ U} + {toTy : U ⟶ M.Ty} {toTm : E ⟶ M.Tm} + (pb : IsPullback toTm π M.tp toTy) : + StructuredUniverse R where + __ := UnstructuredUniverse.ofIsPullback M.toUnstructuredUniverse pb + morphismProperty := R.of_isPullback pb M.morphismProperty + +/-! ## Polynomial functor on `tp` + +Specializations of results from the `Poly` package to natural models. -/ + +abbrev uvPolyTp : UvPoly R M.Tm M.Ty := ⟨M.tp, M.morphismProperty⟩ + +variable [ChosenTerminal Ctx] [R.HasObjects] [R.IsMultiplicative] + [R.HasPushforwards R] [R.IsStableUnderPushforwards R] + +instance : R.HasPushforwardsAlong M.uvPolyTp.p := + MorphismProperty.HasPushforwards.hasPushforwardsAlong M.tp M.morphismProperty + +instance : R.IsStableUnderPushforwardsAlong M.uvPolyTp.p := + MorphismProperty.IsStableUnderPushforwards.of_isPushforward M.tp M.morphismProperty + +def Ptp : Ctx ⥤ Ctx := M.uvPolyTp.functor + +namespace PtpEquiv + +variable {Γ : Ctx} {X : Ctx} + +/-- +A map `(AB : Γ ⟶ M.Ptp.obj X)` is equivalent to a pair of maps +`A : Γ ⟶ M.Ty` and `B : (M.ext (fst M AB)) ⟶ X`, +thought of as a dependent pair `A : Type` and `B : A ⟶ Type`. +`PtpEquiv.fst` is the `A` in this pair. +-/ +def fst (AB : Γ ⟶ M.Ptp.obj X) : Γ ⟶ M.Ty := + UvPoly.Equiv.fst AB + +/-- +A map `(AB : Γ ⟶ M.Ptp.obj X)` is equivalent to a pair of maps +`A : Γ ⟶ M.Ty` and `B : (M.ext (fst M AB)) ⟶ X`, +thought of as a dependent pair `A : Type` and `B : A ⟶ Type` +`PtpEquiv.snd` is the `B` in this pair. +-/ +def snd (AB : Γ ⟶ M.Ptp.obj X) (A := fst M AB) (eq : fst M AB = A := by rfl) : M.ext A ⟶ X := + UvPoly.Equiv.snd' AB (by rw [← fst, eq]; exact (M.disp_pullback _).flip) + +/-- +A map `(AB : Γ ⟶ M.Ptp.obj X)` is equivalent to a pair of maps +`A : Γ ⟶ M.Ty` and `B : (M.ext (fst M AB)) ⟶ X`, +thought of as a dependent pair `A : Type` and `B : A ⟶ Type` +`PtpEquiv.mk` constructs such a map `AB` from such a pair `A` and `B`. +-/ +def mk (A : Γ ⟶ M.Ty) (B : M.ext A ⟶ X) : Γ ⟶ M.Ptp.obj X := + UvPoly.Equiv.mk' A (M.disp_pullback _).flip B + +@[simp] +lemma fst_mk (A : Γ ⟶ M.Ty) (B : M.ext A ⟶ X) : + fst M (mk M A B) = A := by + simp [fst, mk] + +@[simp] +lemma snd_mk (A : Γ ⟶ M.Ty) (B : M.ext A ⟶ X) : + snd M (mk M A B) _ (fst_mk ..) = B := by + dsimp only [snd, mk] + rw! [UvPoly.Equiv.snd'_mk' (P := M.uvPolyTp)] + +section +variable {Δ : Ctx} {σ : Δ ⟶ Γ} {AB : Γ ⟶ M.Ptp.obj X} + +theorem fst_comp_left (σ : Δ ⟶ Γ) : fst M (σ ≫ AB) = σ ≫ fst M AB := + UvPoly.Equiv.fst_comp_left .. + +@[simp] +theorem fst_comp_right {Y} (σ : X ⟶ Y) : fst M (AB ≫ M.Ptp.map σ) = fst M AB := + UvPoly.Equiv.fst_comp_right .. + +theorem snd_comp_right {Y} (σ : X ⟶ Y) {A} (eq : fst M AB = A) : + snd M (AB ≫ M.Ptp.map σ) _ (by simpa) = snd M AB _ eq ≫ σ := by + simp only [snd, Ptp] + rw [UvPoly.Equiv.snd'_comp_right (P := M.uvPolyTp)] + +theorem snd_comp_left {A} (eqA : fst M AB = A) {σA} (eqσ : σ ≫ A = σA) : + snd M (σ ≫ AB) σA (by simp [fst_comp_left, eqA, eqσ]) = + (M.substWk σ _ _ eqσ) ≫ snd M AB _ eqA := by + have H1 : IsPullback (M.disp A) (M.var A) (UvPoly.Equiv.fst AB) M.tp := by + rw [← fst, eqA]; exact (M.disp_pullback _).flip + have H2 : IsPullback (M.disp σA) (M.var σA) + (σ ≫ UvPoly.Equiv.fst AB) M.tp := by + rw [← fst, eqA, eqσ]; exact (M.disp_pullback _).flip + convert UvPoly.Equiv.snd'_comp_left AB H1 _ H2 + apply H1.hom_ext <;> simp [substWk] + +theorem mk_comp_left {Δ Γ : Ctx} (M : StructuredUniverse R) (σ : Δ ⟶ Γ) + {X : Ctx} (A : Γ ⟶ M.Ty) (σA) (eq : σ ≫ A = σA) (B : (M.ext A) ⟶ X) : + σ ≫ PtpEquiv.mk M A B = PtpEquiv.mk M σA ((M.substWk σ A _ eq) ≫ B) := by + dsimp [PtpEquiv.mk] + have h := UvPoly.Equiv.mk'_comp_left (P := M.uvPolyTp) A (f := M.disp A) (g := M.var A) + (by convert (M.disp_pullback A).flip) B σ σA eq (M.disp_pullback σA).flip + convert h + apply (M.disp_pullback _).hom_ext + · simp + · simp [substWk_disp] + +theorem mk_comp_right {Γ : Ctx} (M : StructuredUniverse R) + {X Y : Ctx} (σ : X ⟶ Y) (A : Γ ⟶ M.Ty) (B : (M.ext A) ⟶ X) : + PtpEquiv.mk M A B ≫ M.Ptp.map σ = PtpEquiv.mk M A (B ≫ σ) := + UvPoly.Equiv.mk'_comp_right .. + +theorem ext {AB AB' : Γ ⟶ M.Ptp.obj X} (A := fst M AB) (eq : fst M AB = A := by rfl) + (h1 : fst M AB = fst M AB') (h2 : snd M AB A eq = snd M AB' A (h1 ▸ eq)) : + AB = AB' := UvPoly.Equiv.ext' _ h1 h2 + +theorem eta (AB : Γ ⟶ M.Ptp.obj X) : mk M (fst M AB) (snd M AB) = AB := + .symm <| ext _ _ rfl (by simp) (by simp) + +end + +end PtpEquiv + +@[reassoc] +theorem PtpEquiv.mk_map {Γ : Ctx} {X Y : Ctx} + (A : Γ ⟶ M.Ty) (x : (M.ext A) ⟶ X) (α : X ⟶ Y) : + mk M A x ≫ M.Ptp.map α = mk M A (x ≫ α) := by + simp [mk, Ptp, UvPoly.Equiv.mk'_comp_right] + +/-! ## Polynomial composition `M.tp ▸ N.tp` -/ + +abbrev compDom (M N : StructuredUniverse R) : Ctx := M.uvPolyTp.compDom N.uvPolyTp + +abbrev compP (M N : StructuredUniverse R) : M.compDom N ⟶ M.uvPolyTp @ N.Ty := + (M.uvPolyTp.comp N.uvPolyTp).p + +namespace compDomEquiv +open UvPoly + +variable {M N : StructuredUniverse R} {Γ Δ : Ctx} (σ : Δ ⟶ Γ) + +/-- Universal property of `compDom`, decomposition (part 1). + +A map `ab : Γ ⟶ M.uvPolyTp.compDom N.uvPolyTp` is equivalently three maps +`fst, dependent, snd` such that `fst_tp` and `snd_tp`. The map `fst : Γ ⟶ M.Tm` +is the `(a : A)` in `(a : A) × (b : B a)`. +-/ +abbrev fst (ab : Γ ⟶ M.uvPolyTp.compDom N.uvPolyTp) : Γ ⟶ M.Tm := + UvPoly.compDomEquiv.fst ab + +/-- Computation of `comp` (part 1). + +`fst_tp` is (part 1) of the computation that + (α, B, β, h) + Γ ⟶ compDom + \ | + \ | comp +(α ≫ tp, B) | + \ V + > P_tp Ty +Namely the first projection `α ≫ tp` agrees. +-/ +theorem fst_tp (ab : Γ ⟶ M.uvPolyTp.compDom N.uvPolyTp) : + fst ab ≫ M.tp = PtpEquiv.fst M (ab ≫ M.compP N) := + UvPoly.compDomEquiv.fst_comp_p .. + +@[reassoc] +theorem fst_comp (ab : Γ ⟶ M.uvPolyTp.compDom N.uvPolyTp) (σ : Δ ⟶ Γ) : + fst (σ ≫ ab) = σ ≫ fst ab := + UvPoly.compDomEquiv.fst_comp .. + +/-- Universal property of `compDom`, decomposition (part 2). + +A map `ab : Γ ⟶ M.uvPolyTp.compDom N.uvPolyTp` is equivalently three maps +`fst, dependent, snd` such that `fst_tp` and `snd_tp`. +The map `dependent : (M.ext (fst N ab ≫ M.tp)) ⟶ M.Ty` +is the `B : A ⟶ Type` in `(a : A) × (b : B a)`. +Here `A` is implicit, derived by the typing of `fst`, or `(a : A)`. +-/ +def dependent (ab : Γ ⟶ M.uvPolyTp.compDom N.uvPolyTp) + (A := fst ab ≫ M.tp) (eq : fst ab ≫ M.tp = A := by rfl) : + (M.ext A) ⟶ N.Ty := + UvPoly.compDomEquiv.dependent ab (M.disp A) (M.var A) <| by + simpa [eq] using (M.disp_pullback A).flip + +lemma dependent_eq (ab : Γ ⟶ M.uvPolyTp.compDom N.uvPolyTp) + (A := fst ab ≫ M.tp) (eq : fst ab ≫ M.tp = A := by rfl) : + dependent ab A eq = PtpEquiv.snd M (ab ≫ M.compP N) A (by simp [← eq, fst_tp]) := by + simp [dependent, UvPoly.compDomEquiv.dependent, PtpEquiv.snd] + +theorem comp_dependent (ab : Γ ⟶ M.uvPolyTp.compDom N.uvPolyTp) + {A} (eq1 : fst ab ≫ M.tp = A) + {σA} (eq2 : σ ≫ A = σA) : + (M.substWk σ _ _ eq2) ≫ dependent ab A eq1 = + dependent (σ ≫ ab) σA (by simp [fst_comp, eq1, eq2]) := by + dsimp [dependent] + rw [UvPoly.compDomEquiv.dependent_comp σ ab (M.disp A) (M.var A) + (by simpa [eq1] using (M.disp_pullback A).flip)] + · congr 1 + simp [substWk, substCons] + apply (M.disp_pullback A).hom_ext <;> simp + +/-- Universal property of `compDom`, decomposition (part 3). + +A map `ab : Γ ⟶ M.uvPolyTp.compDom N.uvPolyTp` is equivalently three maps +`fst, dependent, snd` such that `fst_tp` and `snd_tp`. +The map `snd : Γ ⟶ M.Tm` +is the `(b : B a)` in `(a : A) × (b : B a)`. +-/ +abbrev snd (ab : Γ ⟶ M.uvPolyTp.compDom N.uvPolyTp) : Γ ⟶ N.Tm := + UvPoly.compDomEquiv.snd ab + +@[reassoc] +theorem snd_comp (ab : Γ ⟶ M.uvPolyTp.compDom N.uvPolyTp) (σ : Δ ⟶ Γ) : + snd (σ ≫ ab) = σ ≫ snd ab := + UvPoly.compDomEquiv.snd_comp .. + +/-- Universal property of `compDom`, decomposition (part 4). + +A map `ab : Γ ⟶ M.uvPolyTp.compDom N.uvPolyTp` is equivalently three maps +`fst, dependent, snd` such that `fst_tp` and `snd_tp`. +The equation `snd_tp` says that the type of `b : B a` agrees with +the expression for `B a` obtained solely from `dependent`, or `B : A ⟶ Type`. +-/ +theorem snd_tp (ab : Γ ⟶ M.uvPolyTp.compDom N.uvPolyTp) + {A} (eq : fst ab ≫ M.tp = A := by rfl) : + snd ab ≫ N.tp = (M.sec _ (fst ab) eq) ≫ dependent ab A eq := by + rw [UvPoly.compDomEquiv.snd_comp_p ab (M.disp A) (M.var A) <| by + simpa [eq] using (M.disp_pullback A).flip] + congr 1 + apply (disp_pullback ..).hom_ext + · simp + · simp + +/-- Universal property of `compDom`, constructing a map into `compDom`. -/ +def mk (α : Γ ⟶ M.Tm) {A} (eq : α ≫ M.tp = A) (B : M.ext A ⟶ N.Ty) (β : Γ ⟶ N.Tm) + (h : β ≫ N.tp = M.sec _ α eq ≫ B) : Γ ⟶ M.uvPolyTp.compDom N.uvPolyTp := + UvPoly.compDomEquiv.mk _ α eq (M.disp A) (M.var A) (M.disp_pullback A).flip B β (by + convert h + apply (disp_pullback ..).hom_ext <;> simp) + +@[simp] +theorem fst_mk (α : Γ ⟶ M.Tm) {A} (eq : α ≫ M.tp = A := by rfl) (B : (M.ext A) ⟶ N.Ty) + (β : Γ ⟶ N.Tm) (h : β ≫ N.tp = (M.sec _ α eq) ≫ B) : fst (mk α eq B β h) = α := by + simp [mk, fst] + +@[simp] +theorem dependent_mk (α : Γ ⟶ M.Tm) {A A'} (eq : α ≫ M.tp = A) (hA' : A' = A) + (B : M.ext A ⟶ N.Ty) (β : Γ ⟶ N.Tm) + (h : β ≫ N.tp = (M.sec _ α eq) ≫ B) : + dependent (mk α eq B β h) A' (by simp [hA', fst_mk, eq]) = eqToHom (by rw [hA']) ≫ B := by + subst hA' + simp [mk, dependent] + +@[simp] +theorem snd_mk (α : Γ ⟶ M.Tm) {A} (eq : α ≫ M.tp = A) (B : (M.ext A) ⟶ N.Ty) (β : Γ ⟶ N.Tm) + (h : β ≫ N.tp = (M.sec _ α eq) ≫ B) : snd (mk α eq B β h) = β := by + simp [mk, snd] + +theorem ext {ab₁ ab₂ : Γ ⟶ M.uvPolyTp.compDom N.uvPolyTp} + {A} (eq : fst ab₁ ≫ M.tp = A) + (h1 : fst ab₁ = fst ab₂) + (h2 : dependent ab₁ A eq = dependent ab₂ A (h1 ▸ eq)) + (h3 : snd ab₁ = snd ab₂) : ab₁ = ab₂ := by + apply UvPoly.compDomEquiv.ext ab₁ ab₂ h1 h3 (M.disp _) (M.var _) (M.disp_pullback _).flip + dsimp only [dependent] at * + subst eq + rw! [h2] + +theorem comp_mk (α : Γ ⟶ M.Tm) {A} (e1 : α ≫ M.tp = A) (B : (M.ext A) ⟶ N.Ty) + (β : Γ ⟶ N.Tm) (e2 : β ≫ N.tp = (M.sec A α e1) ≫ B) (σ : Δ ⟶ Γ) {σA} (e3 : σ ≫ A = σA) : + σ ≫ mk α e1 B β e2 = + mk (σ ≫ α) (by simp [e1, e3]) + ((M.substWk σ A _ e3) ≫ B) (σ ≫ β) + (by simp [e2]; rw [← Category.assoc, comp_sec]; simp; congr!) := by + dsimp only [mk] + rw [UvPoly.compDomEquiv.comp_mk (P := M.uvPolyTp) (P' := N.uvPolyTp) σ _ α e1 (M.disp _) + (M.var _) (M.disp_pullback _).flip (M.disp _) (M.var _) (M.disp_pullback _).flip] + subst e1 e3 + congr 2 + apply (disp_pullback ..).hom_ext <;> simp [substWk_disp] + +@[reassoc] +lemma mk_comp (α : Γ ⟶ M.Tm) {A} (e1 : α ≫ M.tp = A) (B : (M.ext A) ⟶ N.Ty) + (β : Γ ⟶ N.Tm) (e2 : β ≫ N.tp = (M.sec A α e1) ≫ B) : + mk α e1 B β e2 ≫ M.compP N = PtpEquiv.mk M A B := by + erw [PtpEquiv.mk, UvPoly.compDomEquiv.mk_comp (P := M.uvPolyTp) (P' := N.uvPolyTp)] + +theorem eta (ab : Γ ⟶ M.uvPolyTp.compDom N.uvPolyTp) + {A} (eq : fst ab ≫ M.tp = A) : + mk (fst ab) eq (dependent ab A eq) (snd ab) (snd_tp ab eq) = ab := by + symm; apply ext (eq := eq) <;> simp + +end compDomEquiv + +/-! ## Pi types -/ + +/-- The structure on three universes that for +`A : Γ ⟶ U0.Ty` and `B : Γ.A ⟶ U1.Ty` constructs a Π-type `Π_A B : Γ ⟶ U2.Ty`. +-/ +structure PolymorphicPi (U0 U1 U2 : StructuredUniverse R) where + Pi : U0.Ptp.obj U1.Ty ⟶ U2.Ty + lam : U0.Ptp.obj U1.Tm ⟶ U2.Tm + Pi_pullback : IsPullback lam (U0.Ptp.map U1.tp) U2.tp Pi + +set_option linter.dupNamespace false in +/-- A universe `M` has Π-type structure. This is the data of a pullback square +``` + lam +Ptp Tm ------> Tm + | | +Ptp tp |tp + | | + V V +Ptp Ty ------> Ty + Pi +``` +-/ +protected abbrev Pi := PolymorphicPi M M M + +namespace PolymorphicPi + +variable {U0 U1 U2 : StructuredUniverse R} {Γ : Ctx} + +section +variable (P : PolymorphicPi U0 U1 U2) + +/-- +``` +Γ ⊢₀ A Γ.A ⊢₁ B +----------------- +Γ ⊢₂ ΠA. B +``` -/ +def mkPi {Γ : Ctx} (A : Γ ⟶ U0.Ty) (B : U0.ext A ⟶ U1.Ty) : Γ ⟶ U2.Ty := + PtpEquiv.mk U0 A B ≫ P.Pi + +theorem comp_mkPi {Δ Γ : Ctx} (σ : Δ ⟶ Γ) + (A : (Γ) ⟶ U0.Ty) (σA) (eq : (σ) ≫ A = σA) + (B : (U0.ext A) ⟶ U1.Ty) : + (σ) ≫ P.mkPi A B = P.mkPi σA ((U0.substWk σ A _ eq) ≫ B) := by + simp [mkPi, ← Category.assoc, PtpEquiv.mk_comp_left (eq := eq)] + +/-- +``` +Γ ⊢₀ A Γ.A ⊢₁ t : B +------------------------- +Γ ⊢₂ λA. t : ΠA. B +``` -/ +def mkLam {Γ : Ctx} (A : (Γ) ⟶ U0.Ty) (t : (U0.ext A) ⟶ U1.Tm) : (Γ) ⟶ U2.Tm := + PtpEquiv.mk U0 A t ≫ P.lam + +@[simp] +theorem mkLam_tp {Γ : Ctx} (A : (Γ) ⟶ U0.Ty) (B : (U0.ext A) ⟶ U1.Ty) + (t : (U0.ext A) ⟶ U1.Tm) (t_tp : t ≫ U1.tp = B) : + P.mkLam A t ≫ U2.tp = P.mkPi A B := by + simp [mkLam, mkPi, P.Pi_pullback.w, PtpEquiv.mk_map_assoc, t_tp] + +theorem comp_mkLam {Δ Γ : Ctx} (σ : Δ ⟶ Γ) + (A : (Γ) ⟶ U0.Ty) (σA) (eq : (σ) ≫ A = σA) (t : (U0.ext A) ⟶ U1.Tm) : + (σ) ≫ P.mkLam A t = P.mkLam σA ((U0.substWk σ A _ eq) ≫ t) := by + simp [mkLam, ← Category.assoc, PtpEquiv.mk_comp_left (eq := eq)] + + +/-- +``` +Γ ⊢₀ A Γ ⊢₂ f : ΠA. B +----------------------------- +Γ.A ⊢₁ unlam f : B +``` -/ +def unLam {Γ : Ctx} (A : (Γ) ⟶ U0.Ty) (B : (U0.ext A) ⟶ U1.Ty) + (f : (Γ) ⟶ U2.Tm) (f_tp : f ≫ U2.tp = P.mkPi A B) : + (U0.ext A) ⟶ U1.Tm := by + let total : (Γ) ⟶ U0.Ptp.obj U1.Tm := + P.Pi_pullback.lift f (PtpEquiv.mk U0 A B) f_tp + refine PtpEquiv.snd U0 total _ ?_ + have eq : total ≫ U0.Ptp.map U1.tp = PtpEquiv.mk U0 A B := + (P.Pi_pullback).lift_snd .. + apply_fun PtpEquiv.fst U0 at eq + rw [PtpEquiv.fst_comp_right] at eq + simpa using eq + +@[simp] +theorem unLam_tp {Γ : Ctx} (A : (Γ) ⟶ U0.Ty) (B : (U0.ext A) ⟶ U1.Ty) + (f : (Γ) ⟶ U2.Tm) (f_tp : f ≫ U2.tp = P.mkPi A B) : + P.unLam A B f f_tp ≫ U1.tp = B := by + rw [unLam, ← PtpEquiv.snd_comp_right] + convert PtpEquiv.snd_mk U0 A B using 2; simp + +theorem comp_unLam {Δ Γ : Ctx} (σ : Δ ⟶ Γ) + (A : (Γ) ⟶ U0.Ty) (σA) (eq : (σ) ≫ A = σA) (B : (U0.ext A) ⟶ U1.Ty) + (f : (Γ) ⟶ U2.Tm) (f_tp : f ≫ U2.tp = P.mkPi A B) : + (U0.substWk σ A _ eq) ≫ P.unLam A B f f_tp = + P.unLam σA ((U0.substWk σ A _ eq) ≫ B) + ((σ) ≫ f) (by simp [eq, f_tp, comp_mkPi]) := by + simp [unLam] + rw [← PtpEquiv.snd_comp_left] + simp [PtpEquiv.snd, UvPoly.Equiv.snd'_eq]; congr 1 + apply pullback.hom_ext <;> simp; congr 1 + apply (P.Pi_pullback).hom_ext <;> simp + rw [PtpEquiv.mk_comp_left] + +/-- +``` +Γ ⊢₂ f : ΠA. B Γ ⊢₀ a : A +--------------------------------- +Γ ⊢₁ f a : B[id.a] +``` -/ +def mkApp {Γ : Ctx} (A : (Γ) ⟶ U0.Ty) (B : (U0.ext A) ⟶ U1.Ty) + (f : (Γ) ⟶ U2.Tm) (f_tp : f ≫ U2.tp = P.mkPi A B) + (a : (Γ) ⟶ U0.Tm) (a_tp : a ≫ U0.tp = A) : (Γ) ⟶ U1.Tm := + (U0.sec A a a_tp) ≫ P.unLam A B f f_tp + +@[simp] +theorem mkApp_tp {Γ : Ctx} (A : (Γ) ⟶ U0.Ty) (B : (U0.ext A) ⟶ U1.Ty) + (f : (Γ) ⟶ U2.Tm) (f_tp : f ≫ U2.tp = P.mkPi A B) + (a : (Γ) ⟶ U0.Tm) (a_tp : a ≫ U0.tp = A) : + P.mkApp A B f f_tp a a_tp ≫ U1.tp = (U0.sec A a a_tp) ≫ B := by + simp [mkApp] + +theorem comp_mkApp {Δ Γ : Ctx} (σ : Δ ⟶ Γ) + (A : Γ ⟶ U0.Ty) (σA) (eq : σ ≫ A = σA) (B : (U0.ext A) ⟶ U1.Ty) + (f : Γ ⟶ U2.Tm) (f_tp : f ≫ U2.tp = P.mkPi A B) + (a : Γ ⟶ U0.Tm) (a_tp : a ≫ U0.tp = A) : + σ ≫ P.mkApp A B f f_tp a a_tp = + P.mkApp σA (U0.substWk σ A _ eq ≫ B) + (σ ≫ f) (by simp [f_tp, comp_mkPi (eq := eq)]) + (σ ≫ a) (by simp [a_tp, eq]) := by + unfold mkApp; rw [← Category.assoc, + comp_sec (eq := eq), Category.assoc, comp_unLam (eq := eq)] + +@[simp] +theorem mkLam_unLam {Γ : Ctx} (A : Γ ⟶ U0.Ty) (B : (U0.ext A) ⟶ U1.Ty) + (f : Γ ⟶ U2.Tm) (f_tp : f ≫ U2.tp = P.mkPi A B) : + P.mkLam A (P.unLam A B f f_tp) = f := by + let total : Γ ⟶ U0.Ptp.obj U1.Tm := + (P.Pi_pullback).lift f (PtpEquiv.mk U0 A B) f_tp + simp only [mkLam, unLam] + have : PtpEquiv.fst U0 total = A := by + simp only [PtpEquiv.fst, UvPoly.Equiv.fst_eq, total] + rw [← U0.uvPolyTp.map_fstProj U1.tp] + slice_lhs 1 2 => apply (P.Pi_pullback).lift_snd + apply PtpEquiv.fst_mk + slice_lhs 1 1 => equals total => + apply PtpEquiv.ext _ (A := A) (by simp) (by simp [this]) (by simp [total]) + apply (P.Pi_pullback).lift_fst + +@[simp] +theorem unLam_mkLam {Γ : Ctx} (A : Γ ⟶ U0.Ty) (B : U0.ext A ⟶ U1.Ty) + (t : U0.ext A ⟶ U1.Tm) (t_tp : t ≫ U1.tp = B) + (lam_tp : P.mkLam A t ≫ U2.tp = P.mkPi A B) : + P.unLam A B (P.mkLam A t) lam_tp = t := by + simp [mkLam, unLam] + convert PtpEquiv.snd_mk U0 A t using 2 + apply (P.Pi_pullback).hom_ext <;> simp + rw [PtpEquiv.mk_comp_right, t_tp] + +/-- +``` +Γ ⊢₂ f : ΠA. B +-------------------------------------- +Γ ⊢₂ λA. f[↑] v₀ : ΠA. B +``` +-/ +def etaExpand {Γ : Ctx} (A : (Γ) ⟶ U0.Ty) (B : (U0.ext A) ⟶ U1.Ty) + (f : Γ ⟶ U2.Tm) (f_tp : f ≫ U2.tp = P.mkPi A B) : + (Γ) ⟶ U2.Tm := + P.mkLam A <| + P.mkApp + (U0.disp A ≫ A) (U0.substWk .. ≫ B) (U0.disp A ≫ f) + (by simp [f_tp, comp_mkPi]) + (U0.var A) (U0.var_tp A) + +theorem etaExpand_eq {Γ : Ctx} (A : (Γ) ⟶ U0.Ty) (B : (U0.ext A) ⟶ U1.Ty) + (f : Γ ⟶ U2.Tm) (f_tp : f ≫ U2.tp = P.mkPi A B) : + P.etaExpand A B f f_tp = f := by + simp [etaExpand] + convert P.mkLam_unLam A B f f_tp using 2 + simp [mkApp]; rw [← comp_unLam (f_tp := f_tp), ← Category.assoc] + conv_rhs => rw [← Category.id_comp (P.unLam ..)] + congr 2 + apply (U0.disp_pullback A).hom_ext <;> simp + +/-- +``` +Γ ⊢₀ A Γ.A ⊢₁ t : B Γ ⊢₀ a : A +-------------------------------- +Γ.A ⊢₁ (λA. t) a ≡ t[a] : B[a] +``` -/ +@[simp] +theorem mkApp_mkLam {Γ : Ctx} (A : (Γ) ⟶ U0.Ty) (B : (U0.ext A) ⟶ U1.Ty) + (t : (U0.ext A) ⟶ U1.Tm) (t_tp : t ≫ U1.tp = B) + (lam_tp : P.mkLam A t ≫ U2.tp = P.mkPi A B) + (a : (Γ) ⟶ U0.Tm) (a_tp : a ≫ U0.tp = A) : + P.mkApp A B (P.mkLam A t) lam_tp a a_tp = (U0.sec A a a_tp) ≫ t := by + rw [mkApp, unLam_mkLam] + assumption + +def toUnstructured : + UnstructuredUniverse.PolymorphicPi U0.toUnstructuredUniverse + U1.toUnstructuredUniverse U2.toUnstructuredUniverse where + Pi := P.mkPi _ + Pi_comp _ _ _ _ _ := (P.comp_mkPi ..).symm + lam _ b _ := P.mkLam _ b + lam_comp σ A σA eq _ b _ := (P.comp_mkLam σ A σA eq b).symm + lam_tp B b b_tp := P.mkLam_tp _ B b b_tp + unLam := P.unLam _ + unLam_tp B f f_tp := P.unLam_tp _ B f f_tp + unLam_lam B b b_tp := P.unLam_mkLam _ B b b_tp _ + lam_unLam B := P.mkLam_unLam _ B + +end + +namespace ofUnstructured + +variable {U0 U1 U2 : StructuredUniverse R} + (P : UnstructuredUniverse.PolymorphicPi U0.toUnstructuredUniverse + U1.toUnstructuredUniverse U2.toUnstructuredUniverse) + +def PiApp (AB : Γ ⟶ U0.uvPolyTp @ U1.Ty) : Γ ⟶ U2.Ty := + P.Pi (PtpEquiv.snd U0 AB) + +lemma Pi_naturality {Δ Γ} (σ : Δ ⟶ Γ) (AB) : + PiApp P (σ ≫ AB) = σ ≫ PiApp P AB := by + simp only [PiApp, PtpEquiv.fst_comp_left, PtpEquiv.snd_comp_left, ← P.Pi_comp] + rw! [PtpEquiv.fst_comp_left] + +def Pi : U0.uvPolyTp @ U1.Ty ⟶ U2.Ty := + ofYoneda (PiApp P) (Pi_naturality P) + +def lamApp (b : Γ ⟶ U0.uvPolyTp @ U1.Tm) : Γ ⟶ U2.Tm := + P.lam _ (PtpEquiv.snd U0 b) rfl + +lemma lam_naturality {Δ Γ} (σ : Δ ⟶ Γ) (ab) : + lamApp P (σ ≫ ab) = σ ≫ lamApp P ab := by + simp only [lamApp, PtpEquiv.fst_comp_left, PtpEquiv.snd_comp_left, ← P.lam_comp] + rw! [PtpEquiv.fst_comp_left] + simp + +def lam : U0.uvPolyTp @ U1.Tm ⟶ U2.Tm := + ofYoneda (lamApp P) (lam_naturality P) + +lemma lamApp_tp (b : Γ ⟶ U0.uvPolyTp @ U1.Tm) : + lamApp P b ≫ U2.tp = PiApp P (b ≫ U0.Ptp.map U1.tp) := by + simp only [lamApp, PiApp, PtpEquiv.fst_comp_right, PtpEquiv.snd_comp_right] + rw! [P.lam_tp, PtpEquiv.fst_comp_right] + +def lift (f : Γ ⟶ U2.Tm) (AB : Γ ⟶ U0.uvPolyTp @ U1.Ty) + (f_tp : f ≫ U2.tp = PiApp P AB) : Γ ⟶ U0.uvPolyTp @ U1.Tm := + PtpEquiv.mk _ (PtpEquiv.fst _ AB) (P.unLam (PtpEquiv.snd _ AB) f f_tp) + +lemma lamApp_lift (f : Γ ⟶ U2.Tm) (AB : Γ ⟶ U0.uvPolyTp @ U1.Ty) + (f_tp : f ≫ U2.tp = PiApp P AB) : + lamApp P (lift P f AB f_tp) = f := by + dsimp only [lamApp, lift] + rw! (castMode := .all) [PtpEquiv.fst_mk, PtpEquiv.snd_mk, P.unLam_tp, P.lam_unLam] + +lemma lift_Ptp_map_tp (f : Γ ⟶ U2.Tm) (AB : Γ ⟶ U0.uvPolyTp @ U1.Ty) + (f_tp : f ≫ U2.tp = PiApp P AB) : + ofUnstructured.lift P f AB f_tp ≫ U0.Ptp.map U1.tp = AB := by + dsimp [lift] + rw [PtpEquiv.mk_comp_right, P.unLam_tp, PtpEquiv.eta] + +lemma lift_uniq (f : Γ ⟶ U2.Tm) (AB : Γ ⟶ U0.uvPolyTp @ U1.Ty) + (f_tp : f ≫ U2.tp = PiApp P AB) (m : Γ ⟶ U0.Ptp.obj U1.Tm) + (hl : lamApp P m = f) (hr : m ≫ U0.Ptp.map U1.tp = AB) : + m = lift P f AB f_tp := by + fapply PtpEquiv.ext _ + · calc PtpEquiv.fst _ m + _ = PtpEquiv.fst _ (m ≫ U0.Ptp.map U1.tp) := by rw [PtpEquiv.fst_comp_right] + _ = _ := by simp [hr, lift] + · subst hl hr + dsimp only [lift, lamApp] + rw! [PtpEquiv.fst_comp_right, PtpEquiv.snd_mk, PtpEquiv.snd_comp_right, P.unLam_lam] + +end ofUnstructured + +def ofUnstructured (P : UnstructuredUniverse.PolymorphicPi U0.toUnstructuredUniverse + U1.toUnstructuredUniverse U2.toUnstructuredUniverse) : PolymorphicPi U0 U1 U2 where + Pi := ofUnstructured.Pi P + lam := ofUnstructured.lam P + Pi_pullback := ofYoneda_isPullback _ _ _ _ _ _ (ofUnstructured.lamApp_tp P) + (ofUnstructured.lift P) + (ofUnstructured.lamApp_lift P) + (ofUnstructured.lift_Ptp_map_tp P) + (ofUnstructured.lift_uniq P) + +end PolymorphicPi + +/-! ## Sigma types -/ + +/-- The structure on three universes that for +`A : Γ ⟶ U0.Ty` and `B : Γ.A ⟶ U1.Ty` constructs a Π-type `Σ_A B : Γ ⟶ U2.Ty`. -/ +structure PolymorphicSigma (U0 U1 U2 : StructuredUniverse R) where + Sig : U0.Ptp.obj U1.Ty ⟶ U2.Ty + pair : U0.compDom U1 ⟶ U2.Tm + Sig_pullback : IsPullback pair (U0.compP U1) U2.tp Sig + +/-- A universe `M` has Σ-type structure. This is the data of a pullback square +``` + Sig +compDom ------> Tm + | | + compP |tp + | | + V V +Ptp Ty ------> Ty + pair +``` +-/ +protected abbrev Sigma := PolymorphicSigma M M M + +namespace PolymorphicSigma + +variable {U0 U1 U2 : StructuredUniverse R} {Γ : Ctx} + +section +variable (S : PolymorphicSigma U0 U1 U2) + +/-- +``` +Γ ⊢₀ A Γ.A ⊢₁ B +----------------- +Γ ⊢₂ ΣA. B +``` -/ +def mkSig {Γ : Ctx} (A : Γ ⟶ U0.Ty) (B : U0.ext A ⟶ U1.Ty) : + Γ ⟶ U2.Ty := + PtpEquiv.mk U0 A B ≫ S.Sig + +theorem comp_mkSig {Δ Γ : Ctx} (σ : Δ ⟶ Γ) (A : Γ ⟶ U0.Ty) (B : U0.ext A ⟶ U1.Ty) : + σ ≫ S.mkSig A B = + S.mkSig (σ ≫ A) ((U0.substWk σ A) ≫ B) := by + simp [mkSig, ← Category.assoc, PtpEquiv.mk_comp_left] + +/-- +``` +Γ ⊢₀ t : A Γ ⊢₁ u : B[t] +-------------------------- +Γ ⊢₂ ⟨t, u⟩ : ΣA. B +``` -/ +def mkPair {Γ : Ctx} (A : Γ ⟶ U0.Ty) (B : U0.ext A ⟶ U1.Ty) + (t : Γ ⟶ U0.Tm) (t_tp : t ≫ U0.tp = A) + (u : Γ ⟶ U1.Tm) (u_tp : u ≫ U1.tp = U0.sec A t t_tp ≫ B) : + (Γ) ⟶ U2.Tm := + compDomEquiv.mk t t_tp B u u_tp ≫ S.pair + +theorem comp_mkPair {Δ Γ : Ctx} (σ : Δ ⟶ Γ) + (A : Γ ⟶ U0.Ty) (B : U0.ext A ⟶ U1.Ty) + (t : Γ ⟶ U0.Tm) (t_tp : t ≫ U0.tp = A) + (u : Γ ⟶ U1.Tm) (u_tp : u ≫ U1.tp = U0.sec A t t_tp ≫ B) : + σ ≫ S.mkPair A B t t_tp u u_tp = + S.mkPair (σ ≫ A) ((U0.substWk σ A) ≫ B) + (σ ≫ t) (by simp [t_tp]) + (σ ≫ u) (by simp [u_tp, comp_sec_assoc]) := by + simp only [← Category.assoc, mkPair]; rw [compDomEquiv.comp_mk] + +@[simp] +theorem mkPair_tp {Γ : Ctx} (A : Γ ⟶ U0.Ty) (B : U0.ext A ⟶ U1.Ty) + (t : Γ ⟶ U0.Tm) (t_tp : t ≫ U0.tp = A) + (u : Γ ⟶ U1.Tm) (u_tp : u ≫ U1.tp = U0.sec A t t_tp ≫ B) : + S.mkPair A B t t_tp u u_tp ≫ U2.tp = S.mkSig A B := by + simp [mkPair, Category.assoc, S.Sig_pullback.w, mkSig, compDomEquiv.mk_comp_assoc] + +def mkFst {Γ : Ctx} (A : Γ ⟶ U0.Ty) (B : U0.ext A ⟶ U1.Ty) + (p : Γ ⟶ U2.Tm) (p_tp : p ≫ U2.tp = S.mkSig A B) : + Γ ⟶ U0.Tm := + compDomEquiv.fst (S.Sig_pullback.lift p (PtpEquiv.mk _ A B) p_tp) + +@[simp] +theorem mkFst_tp {Γ : Ctx} (A : Γ ⟶ U0.Ty) (B : U0.ext A ⟶ U1.Ty) + (p : Γ ⟶ U2.Tm) (p_tp : p ≫ U2.tp = S.mkSig A B) : + S.mkFst A B p p_tp ≫ U0.tp = A := by + simp [mkFst, compDomEquiv.fst_tp] + +@[simp] +theorem mkFst_mkPair {Γ : Ctx} (A : Γ ⟶ U0.Ty) (B : U0.ext A ⟶ U1.Ty) + (t : Γ ⟶ U0.Tm) (t_tp : t ≫ U0.tp = A) + (u : Γ ⟶ U1.Tm) (u_tp : u ≫ U1.tp = U0.sec A t t_tp ≫ B) : + S.mkFst A B (S.mkPair A B t t_tp u u_tp) (by simp) = t := by + simp [mkFst, mkPair] + convert compDomEquiv.fst_mk t t_tp B u u_tp using 2 + apply (S.Sig_pullback).hom_ext <;> simp [compDomEquiv.mk_comp] + +theorem comp_mkFst {Δ Γ : Ctx} (σ : Δ ⟶ Γ) + (A : Γ ⟶ U0.Ty) (B : U0.ext A ⟶ U1.Ty) + (p : Γ ⟶ U2.Tm) (p_tp : p ≫ U2.tp = S.mkSig A B) : + (σ) ≫ S.mkFst A B p p_tp = + S.mkFst (σ ≫ A) (U0.substWk σ A ≫ B) (σ ≫ p) + (by simp [p_tp, comp_mkSig]) := by + simp [mkFst] + rw [← compDomEquiv.fst_comp]; congr 1 + apply S.Sig_pullback.hom_ext <;> simp [PtpEquiv.mk_comp_left] + +def mkSnd {Γ : Ctx} (A : Γ ⟶ U0.Ty) (B : U0.ext A ⟶ U1.Ty) + (p : Γ ⟶ U2.Tm) (p_tp : p ≫ U2.tp = S.mkSig A B) : + Γ ⟶ U1.Tm := + compDomEquiv.snd (S.Sig_pullback.lift p (PtpEquiv.mk _ A B) p_tp) + +@[simp] +theorem mkSnd_mkPair {Γ : Ctx} (A : Γ ⟶ U0.Ty) (B : U0.ext A ⟶ U1.Ty) + (t : Γ ⟶ U0.Tm) (t_tp : t ≫ U0.tp = A) + (u : Γ ⟶ U1.Tm) (u_tp : u ≫ U1.tp = U0.sec A t t_tp ≫ B) : + S.mkSnd A B (S.mkPair A B t t_tp u u_tp) (by simp) = u := by + simp [mkSnd, mkPair] + convert compDomEquiv.snd_mk t t_tp B u u_tp using 2 + apply (S.Sig_pullback).hom_ext <;> simp [compDomEquiv.mk_comp] + +protected theorem dependent_eq {Γ : Ctx} (A : Γ ⟶ U0.Ty) (B : U0.ext A ⟶ U1.Ty) + (p : Γ ⟶ U2.Tm) (p_tp : p ≫ U2.tp = S.mkSig A B) : + compDomEquiv.dependent ((S.Sig_pullback).lift p (PtpEquiv.mk U0 A B) p_tp) A + (by simp [compDomEquiv.fst_tp]) = B := by + convert PtpEquiv.snd_mk U0 A B using 2 + simp only [compDomEquiv.dependent, UvPoly.compDomEquiv.dependent, PtpEquiv.snd_mk] + simp [PtpEquiv.mk] + +@[simp] +theorem mkSnd_tp {Γ : Ctx} (A : Γ ⟶ U0.Ty) (B : U0.ext A ⟶ U1.Ty) + (p : Γ ⟶ U2.Tm) (p_tp : p ≫ U2.tp = S.mkSig A B) : + S.mkSnd A B p p_tp ≫ U1.tp = + (U0.sec A (S.mkFst A B p p_tp) (by simp)) ≫ B := by + generalize_proofs h + simp [mkSnd, compDomEquiv.snd_tp (eq := h), S.dependent_eq]; rfl + +theorem comp_mkSnd {Δ Γ : Ctx} (σ : Δ ⟶ Γ) + (A : Γ ⟶ U0.Ty) (B : U0.ext A ⟶ U1.Ty) + (p : Γ ⟶ U2.Tm) (p_tp : p ≫ U2.tp = S.mkSig A B) : + σ ≫ S.mkSnd A B p p_tp = + S.mkSnd (σ ≫ A) (U0.substWk σ A ≫ B) (σ ≫ p) + (by simp [p_tp, comp_mkSig]) := by + simp [mkSnd, ← compDomEquiv.snd_comp]; congr 1 + apply (S.Sig_pullback).hom_ext <;> simp + rw [PtpEquiv.mk_comp_left] + +@[simp] +theorem mkPair_mkFst_mkSnd {Γ : Ctx} (A : Γ ⟶ U0.Ty) (B : U0.ext A ⟶ U1.Ty) + (p : Γ ⟶ U2.Tm) (p_tp : p ≫ U2.tp = S.mkSig A B) : + S.mkPair A B + (S.mkFst A B p p_tp) (by simp) + (S.mkSnd A B p p_tp) (by simp) = p := by + simp [mkFst, mkSnd, mkPair] + have := compDomEquiv.eta ((S.Sig_pullback).lift p (PtpEquiv.mk _ A B) p_tp) + (eq := by rw [← mkFst.eq_def, mkFst_tp]) + conv at this => enter [1, 3]; apply S.dependent_eq + simp [this] + +end + +namespace ofUnstructured + +variable {U0 U1 U2 : StructuredUniverse R} + (S : UnstructuredUniverse.PolymorphicSigma U0.toUnstructuredUniverse + U1.toUnstructuredUniverse U2.toUnstructuredUniverse) + +def SigApp (AB : Γ ⟶ U0.Ptp.obj U1.Ty) : Γ ⟶ U2.Ty := + S.Sig (PtpEquiv.snd U0 AB) + +lemma Sig_naturality {Δ Γ} (σ : Δ ⟶ Γ) (AB) : + SigApp S (σ ≫ AB) = σ ≫ SigApp S AB := by + simp only [SigApp, PtpEquiv.fst_comp_left, PtpEquiv.snd_comp_left, ← S.Sig_comp] + rw! [PtpEquiv.fst_comp_left] + +def Sig : U0.Ptp.obj U1.Ty ⟶ U2.Ty := + ofYoneda (SigApp S) (Sig_naturality S) + +def pairApp (ab : Γ ⟶ U0.compDom U1) : Γ ⟶ U2.Tm := + S.pair (compDomEquiv.dependent ab) (compDomEquiv.fst ab) + (by rw [compDomEquiv.fst_tp]) (compDomEquiv.snd ab) (by rw [compDomEquiv.snd_tp]) + +lemma pair_naturality {Δ Γ} (σ : Δ ⟶ Γ) (ab) : + pairApp S (σ ≫ ab) = σ ≫ pairApp S ab := by + dsimp [pairApp] + simp only [← S.pair_comp, compDomEquiv.comp_dependent, compDomEquiv.fst_comp, + compDomEquiv.snd_comp] + rw! [compDomEquiv.fst_comp, Category.assoc] + +def pair : U0.compDom U1 ⟶ U2.Tm := + ofYoneda (pairApp S) (pair_naturality S) + +lemma pair_tp (ab : Γ ⟶ U0.compDom U1) : + pairApp S ab ≫ U2.tp = SigApp S (ab ≫ U0.compP U1) := by + dsimp [pairApp, SigApp] + rw! [S.pair_tp, compDomEquiv.dependent_eq, compDomEquiv.fst_tp] + +def lift (ab : Γ ⟶ U2.Tm) (AB : Γ ⟶ U0.uvPolyTp @ U1.Ty) + (ab_tp : ab ≫ U2.tp = SigApp S AB) : + Γ ⟶ U0.compDom U1 := + let B := PtpEquiv.snd U0 AB + compDomEquiv.mk (S.fst B ab ab_tp) (S.fst_tp ..) B (S.snd B ab ab_tp) (S.snd_tp ..) + +lemma fst_lift (ab : Γ ⟶ U2.Tm) (AB : Γ ⟶ U0.uvPolyTp @ U1.Ty) + (ab_tp : ab ≫ U2.tp = SigApp S AB) : + compDomEquiv.fst (lift S ab AB ab_tp) = + S.fst (PtpEquiv.snd U0 AB) ab ab_tp := by + rw [lift, compDomEquiv.fst_mk _ _] + +lemma snd_lift (ab : Γ ⟶ U2.Tm) (AB : Γ ⟶ U0.uvPolyTp @ U1.Ty) + (ab_tp : ab ≫ U2.tp = SigApp S AB) : + compDomEquiv.snd (lift S ab AB ab_tp) = + S.snd (PtpEquiv.snd U0 AB) ab ab_tp := by + rw [lift, compDomEquiv.snd_mk] + +lemma dependent_lift (ab : Γ ⟶ U2.Tm) (AB : Γ ⟶ U0.uvPolyTp @ U1.Ty) + (ab_tp : ab ≫ U2.tp = SigApp S AB) : + compDomEquiv.dependent (lift S ab AB ab_tp) (PtpEquiv.fst U0 AB) (by rw [fst_lift, S.fst_tp]) = + PtpEquiv.snd U0 AB (PtpEquiv.fst U0 AB) := by + simp [lift, compDomEquiv.dependent_mk] + +lemma pairApp_lift (ab : Γ ⟶ U2.Tm) (AB : Γ ⟶ U0.uvPolyTp @ U1.Ty) + (ab_tp : ab ≫ U2.tp = ofUnstructured.SigApp S AB) : + ofUnstructured.pairApp S (ofUnstructured.lift S ab AB ab_tp) = ab := by + dsimp [pairApp] + rw! [fst_lift, S.fst_tp, fst_lift, snd_lift, dependent_lift] + rw [S.pair_fst_snd] + +lemma lift_compP (ab : Γ ⟶ U2.Tm) (AB : Γ ⟶ U0.uvPolyTp @ U1.Ty) + (ab_tp : ab ≫ U2.tp = SigApp S AB) : + lift S ab AB ab_tp ≫ U0.compP U1 = AB := by + dsimp [lift] + rw [compDomEquiv.mk_comp, PtpEquiv.eta] + +lemma lift_uniq (ab : Γ ⟶ U2.Tm) (AB : Γ ⟶ U0.uvPolyTp @ U1.Ty) + (ab_tp : ab ≫ U2.tp = SigApp S AB) (m : Γ ⟶ U0.compDom U1) + (hl : pairApp S m = ab) (hr : m ≫ U0.compP U1 = AB) : + m = lift S ab AB ab_tp := by + rw! [← compDomEquiv.eta m] + fapply compDomEquiv.ext (A := PtpEquiv.fst U0 AB) + · rw [compDomEquiv.fst_mk, compDomEquiv.fst_tp, hr] + · rw [fst_lift, compDomEquiv.fst_mk _] + calc compDomEquiv.fst m + _ = S.fst (compDomEquiv.dependent m) (pairApp S m) (S.pair_tp ..) := by + dsimp [pairApp] + rw [S.fst_pair] + S.fst (compDomEquiv.dependent m) (pairApp S m) (S.pair_tp ..) = + S.fst (PtpEquiv.snd U0 AB) ab ab_tp := by + subst hl hr + rw! [compDomEquiv.dependent_eq, compDomEquiv.fst_tp] + · subst hr + rw [compDomEquiv.dependent_mk, dependent_lift, compDomEquiv.dependent_eq] + rw! [compDomEquiv.fst_tp, eqToHom_refl, Category.id_comp, compDomEquiv.fst_tp] + · simp [snd_lift] + calc compDomEquiv.snd m + _ = S.snd (compDomEquiv.dependent m) (pairApp S m) (S.pair_tp ..) := by + dsimp [pairApp] + rw [S.snd_pair] + S.snd (compDomEquiv.dependent m) (pairApp S m) (S.pair_tp ..) = + S.snd (PtpEquiv.snd U0 AB) ab ab_tp := by + subst hl hr + rw! [compDomEquiv.dependent_eq, compDomEquiv.fst_tp] + +end ofUnstructured + +def ofUnstructured {U0 U1 U2 : StructuredUniverse R} + (S : UnstructuredUniverse.PolymorphicSigma U0.toUnstructuredUniverse + U1.toUnstructuredUniverse U2.toUnstructuredUniverse) : + PolymorphicSigma U0 U1 U2 where + Sig := ofUnstructured.Sig S + pair := ofUnstructured.pair S + Sig_pullback := ofYoneda_isPullback _ _ _ _ _ _ (ofUnstructured.pair_tp S) + (ofUnstructured.lift S) + (ofUnstructured.pairApp_lift S) + (ofUnstructured.lift_compP S) + (ofUnstructured.lift_uniq S) + +end PolymorphicSigma + +end StructuredUniverse diff --git a/lake-manifest.json b/lake-manifest.json index 930c29a9..49a6fda3 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -11,11 +11,11 @@ "inputRev": null, "inherited": false, "configFile": "lakefile.lean"}, - {"url": "https://github.com/sinhp/Poly", + {"url": "https://github.com/Jlh18/Poly.git", "type": "git", "subDir": null, "scope": "", - "rev": "aedee22f07d681d845bcbe4a1fb9aa10f95c9977", + "rev": "e662604d050f054deb14c8849c0c5c644058b7b7", "name": "Poly", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "32bd6c7c8ca4a4be1c71bc04df0c9cf929d04818", + "rev": "a79df06b3d23fb6a3c42fb65a949009dc241862d", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null, @@ -75,7 +75,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "1fa48c6a63b4c4cda28be61e1037192776e77ac0", + "rev": "ca519018e8bdc34d7bb4ecf0c8d39634a8c15300", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -95,7 +95,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "c44068fa1b40041e6df42bd67639b690eb2764ca", + "rev": "5a4e38939564f38cef2c55051ea24567df6030ad", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/lakefile.lean b/lakefile.lean index 2807a875..067b7178 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -1,7 +1,7 @@ import Lake open Lake DSL -require Poly from git "https://github.com/sinhp/Poly" @ "master" +require Poly from git "https://github.com/Jlh18/Poly.git" @ "master" require checkdecls from git "https://github.com/PatrickMassot/checkdecls.git"