From 116d8138d088dd3af20682feddf2fd22ca019d12 Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Thu, 18 Sep 2025 22:33:09 +0200 Subject: [PATCH 1/4] feat: adjoint triangle theorem --- .../Distributivity.lean | 252 +++++++++++++++++- Poly/UvPoly/Basic.lean | 82 +++++- 2 files changed, 323 insertions(+), 11 deletions(-) diff --git a/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Distributivity.lean b/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Distributivity.lean index 3078438..6da44f2 100644 --- a/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Distributivity.lean +++ b/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Distributivity.lean @@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Sina Hazratpour, Emily Riehl -/ import Mathlib.CategoryTheory.Limits.Shapes.Pullback.CommSq +import Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory +import Mathlib.CategoryTheory.Adjunction.Opposites import Poly.ForMathlib.CategoryTheory.LocallyCartesianClosed.Basic import Poly.ForMathlib.CategoryTheory.NatTrans import Poly.ForMathlib.CategoryTheory.LocallyCartesianClosed.BeckChevalley @@ -54,11 +56,253 @@ def exponentiableMorphism : ExponentiableMorphism (g f u) := by infer_instance namespace ExponentiableMorphism +structure IsCoequalizer {C} [Category C] {A B L : C} (f g : A ⟶ B) {L} (π : B ⟶ L) : Prop where + w : f ≫ π = g ≫ π + isColimit : Nonempty (IsColimit (Cofork.ofπ π w)) + +def CategoryTheory.Adjunction.cofork {C D} [Category C] [Category D] + {F : C ⥤ D} {U : D ⥤ C} (adj : F ⊣ U) : + Cofork (whiskerLeft (U ⋙ F) adj.counit) (whiskerRight adj.counit (U ⋙ F)) := + .ofπ adj.counit (whiskerLeft_comp_whiskerRight adj.counit adj.counit) + +def CategoryTheory.Adjunction.fork {C D} [Category C] [Category D] + {F : C ⥤ D} {U : D ⥤ C} (adj : F ⊣ U) : + Fork (whiskerLeft (F ⋙ U) adj.unit) (whiskerRight adj.unit (F ⋙ U)) := + .ofι adj.unit (whiskerLeft_comp_whiskerRight adj.unit adj.unit).symm + +theorem associator_eq_id {C D E E'} [Category C] [Category D] [Category E] [Category E'] + (F : C ⥤ D) (G : D ⥤ E) (H : E ⥤ E') : Functor.associator F G H = Iso.refl (F ⋙ G ⋙ H) := rfl + +theorem whiskerRight_left' {C D E B} [Category C] [Category D] [Category E] [Category B] + (F : B ⥤ C) {G H : C ⥤ D} (α : G ⟶ H) (K : D ⥤ E) : + whiskerRight (whiskerLeft F α) K = whiskerLeft F (whiskerRight α K) := rfl + +theorem id_whiskerLeft' {C D} [Category C] [Category D] {G H : C ⥤ D} (α : G ⟶ H) : + whiskerLeft (𝟭 C) α = α := rfl + +theorem id_whiskerRight' {C D} [Category C] [Category D] {G H : C ⥤ D} (α : G ⟶ H) : + whiskerRight α (𝟭 D) = α := rfl + +theorem whiskerLeft_twice' {C D E B} [Category C] [Category D] [Category E] [Category B] + (F : B ⥤ C) (G : C ⥤ D) {H K : D ⥤ E} (α : H ⟶ K) : + whiskerLeft F (whiskerLeft G α) = whiskerLeft (F ⋙ G) α := rfl + +theorem whiskerRight_twice' {C D E B} [Category C] [Category D] [Category E] [Category B] + {H K : B ⥤ C} (F : C ⥤ D) (G : D ⥤ E) (α : H ⟶ K) : + whiskerRight (whiskerRight α F) G = whiskerRight α (F ⋙ G) := rfl + +abbrev Cofork.π' {C} [Category C] {X Y : C} {f g : X ⟶ Y} (s : Cofork f g) : Y ⟶ s.pt := s.π + +def parallelPairComp {C D} [Category C] [Category D] {X Y : C} {f g : X ⟶ Y} (F : C ⥤ D) : + parallelPair f g ⋙ F ≅ parallelPair (F.map f) (F.map g) := diagramIsoParallelPair _ + +def preservesCoequalizer {C D} [Category C] [Category D] {X Y : C} {f g : X ⟶ Y} + {P : C} (π : Y ⟶ P) (w : f ≫ π = g ≫ π) (F : C ⥤ D) + (H : IsColimit (Cofork.ofπ π w)) [PreservesColimit (parallelPair f g) F] : + IsColimit (Cofork.ofπ (f := F.map f) (g := F.map g) (F.map π) + (by rw [← map_comp, w, map_comp])) := by + have := isColimitOfPreserves F H + let iso : parallelPair f g ⋙ F ≅ parallelPair (F.map f) (F.map g) := diagramIsoParallelPair _ + refine (IsColimit.ofCoconeEquiv (Cocones.precomposeEquivalence iso.symm)).symm this + |>.ofIsoColimit (Cofork.ext (Iso.refl _) ?_) + simp [Cocones.precompose, Cofork.π, iso] + +-- theorem whiskeringLeft_preservesEpi {C D E} [Category C] [Category D] [Category E] (F : C ⥤ D) +-- : ((whiskeringLeft C D E).obj F).PreservesEpimorphisms := by +-- refine ⟨fun {G G'} f ⟨hf⟩ => ⟨fun {K} g h eq => ?_⟩⟩ +-- ext X +-- replace eq := congr(($eq).app X) +-- dsimp at g h eq +-- exact hf _ _ eq + + + +-- have := isColimitOfPreserves F H +-- let iso : parallelPair f g ⋙ F ≅ parallelPair (F.map f) (F.map g) := diagramIsoParallelPair _ +-- refine (IsColimit.ofCoconeEquiv (Cocones.precomposeEquivalence iso.symm)).symm this +-- |>.ofIsoColimit (Cofork.ext (Iso.refl _) ?_) +-- simp [Cocones.precompose, Cofork.π, iso] + +-- instance evaluation_preservesColimit +-- {C : Type u} [Category.{v} C] {J : Type u₁} [Category.{v₁} J] {K : Type u₂} [Category.{v₂} K] +-- (F : J ⥤ K ⥤ C) (k : K) : +-- PreservesColimit F ((evaluation K C).obj k) := by +-- refine ⟨fun h' => ⟨fun s => ?_, ?_, ?_⟩⟩ +-- · simp +-- have := s.ι.app; simp at this +-- -- have := h'.desc precompose +-- have := h'.desc ⟨_, fun x => by +-- have := s.ι.app x +-- dsimp at this + +-- simp, _⟩ + -- let X : (k : K) → ColimitCocone (F.flip.obj k) := fun k => getColimitCocone (F.flip.obj k) + -- preservesColimit_of_preserves_colimit_cocone (combinedIsColimit _ X) <| + -- IsColimit.ofIsoColimit (colimit.isColimit _) (evaluateCombinedCocones F X k).symm + +-- instance whiskeringLeft_preservesColimit +-- {C : Type u₁} [Category.{v₁} C] +-- {D : Type u₂} [Category.{v₂} D] +-- {E : Type u₃} [Category.{v₃} E] +-- (J : Type u) [Category.{v} J] +-- (K : J ⥤ E ⥤ D) (F : C ⥤ E) +-- -- [∀ (k : E), HasColimit (K.flip.obj k)] +-- : +-- PreservesColimit K ((whiskeringLeft C E D).obj F) := +-- ⟨fun c {hc} => ⟨by +-- apply evaluationJointlyReflectsColimits +-- intro Y +-- change IsColimit (((evaluation E D).obj (F.obj Y)).mapCocone c) +-- have := evaluation_preservesColimit K (F.obj Y) +-- exact isColimitOfPreserves _ hc⟩⟩ + +attribute [-simp] whiskerLeft_twice whiskerRight_twice in +def adjointTriangle {B C A : Type*} [Category B] [Category C] [Category A] [HasCoequalizers A] + {U : B ⥤ C} {F : C ⥤ B} (adj1 : F ⊣ U) + {R : A ⥤ B} {F' : C ⥤ A} (adj2 : F' ⊣ R ⋙ U) + (H : IsColimit adj1.cofork) : (L : B ⥤ A) × (L ⊣ R) := by + let θ : F ⟶ F' ⋙ R := ((mateEquiv adj2 adj1).symm (.mk _ R (𝟭 _) _ (𝟙 _))).natTrans + let α : U ⋙ F ⋙ U ⋙ F' ⟶ U ⋙ F' := whiskerRight adj1.counit (U ⋙ F') + let β : U ⋙ F ⋙ U ⋙ F' ⟶ U ⋙ F' := + whiskerLeft U (whiskerRight θ (U ⋙ F')) ≫ whiskerLeft (U ⋙ F') adj2.counit + let L := coequalizer α β; use L + let π : _ ⟶ L := coequalizer.π .. + have eq : α ≫ π = β ≫ π := coequalizer.condition .. + have : whiskerLeft (R ⋙ U) θ ≫ whiskerRight adj2.counit R = whiskerLeft R adj1.counit := by + ext X; simp [θ] + have := adj2.right_triangle_components X; dsimp at this + rw [← counit_naturality, ← map_comp_assoc, this]; simp + let preserves : IsColimit (Cofork.ofπ + (f := whiskerLeft R α) (g := whiskerLeft R β) (whiskerLeft R π) _) := + preservesCoequalizer π eq ((whiskeringLeft A B A).obj R) (coequalizerIsCoequalizer ..) + let iso Y : (coequalizer α β).obj Y ≅ coequalizer (α.app Y) (β.app Y) := + letI J := _ + (colimitObjIsoColimitCompEvaluation (parallelPair α β) Y : _ ≅ colimit J).trans <| + colim.mapIso (diagramIsoParallelPair J) + refine + let η := H.desc (Cofork.ofπ (P := L ⋙ R) (whiskerLeft U θ ≫ whiskerRight π R) ?_) + let ε := preserves.desc (Cofork.ofπ adj2.counit ?_) + have η_cond : adj1.counit ≫ η = U.whiskerLeft θ ≫ whiskerRight π R := Cofork.IsColimit.π_desc H + have ε_cond : R.whiskerLeft π ≫ ε = adj2.counit := Cofork.IsColimit.π_desc preserves + .mkOfUnitCounit { + unit := η, counit := ε, left_triangle := (?_ : _ = 𝟙 _), right_triangle := (?_ : _ = 𝟙 _) } + · replace eq := congr(whiskerLeft (U ⋙ F ⋙ U) θ ≫ whiskerRight $eq R) + simp [α, β] at eq + conv_rhs at eq => + conv => enter [2,1]; apply whiskerRight_left' + rw [← whiskerLeft_twice', ← whiskerLeft_twice', ← whiskerLeft_comp_assoc] + conv => enter [1,2]; apply whiskerLeft_comp_whiskerRight + rw [whiskerLeft_comp_assoc]; + conv => + arg 2 + rw [whiskerRight_left', ← whiskerLeft_twice', ← whiskerLeft_twice'] + rw [← whiskerLeft_comp_assoc, ← whiskerLeft_comp] + enter [1,2,2]; rw [whiskerLeft_twice', this] + rw [← whiskerLeft_comp_assoc] + conv => enter [1,2]; apply (whiskerLeft_comp_whiskerRight ..).symm + rw [id_whiskerRight', whiskerLeft_comp_assoc, whiskerLeft_twice'] + rw [← eq, ← whiskerRight_twice', whiskerRight_twice'] + apply whiskerLeft_comp_whiskerRight_assoc + · simp [α, β]; rw [← whiskerRight_left', ← this] + rw [whiskerRight_comp_assoc, whiskerRight_left', whiskerLeft_twice']; congr 1 + exact (whiskerLeft_comp_whiskerRight adj2.counit adj2.counit).symm + · simp [associator_eq_id] + conv_lhs => arg 2; apply id_comp + have _ : Epi π := (Cofork.IsColimit.epi (coequalizerIsCoequalizer α β) :) + have _ : Epi (whiskerRight adj1.counit (U ⋙ F')) := by + refine SplitEpi.epi ⟨whiskerRight (whiskerLeft U adj1.unit) F', ?_⟩ + rw [← whiskerRight_twice', ← whiskerRight_comp, adj1.right_triangle] + apply whiskerRight_id + rw [← cancel_epi π, ← cancel_epi (whiskerRight adj1.counit (U ⋙ F'))] + conv_rhs => arg 2; apply comp_id + have := whiskerLeft_comp_whiskerRight adj1.counit π + rw [id_whiskerLeft'] at this; rw [← reassoc_of% this]; clear this + rw [← whiskerRight_comp_assoc, η_cond, whiskerRight_comp_assoc, + whiskerRight_left', ← whiskerLeft_twice', ← whiskerLeft_comp_assoc, + whiskerLeft_comp_whiskerRight, whiskerLeft_comp_assoc, whiskerLeft_twice'] + conv_lhs => arg 2; apply reassoc_of% whiskerLeft_comp_whiskerRight + rw [← whiskerLeft_twice', ← whiskerLeft_comp, ε_cond] + conv_lhs => arg 2; apply (whiskerLeft_comp_whiskerRight π adj2.counit).symm + rw [id_whiskerRight', ← assoc]; exact eq.symm + · simp [associator_eq_id] + suffices _ : Epi (R.whiskerLeft adj1.counit) by + refine (cancel_epi (R.whiskerLeft adj1.counit)).1 ?_ + rw [← whiskerLeft_comp_assoc, η_cond, whiskerLeft_comp_assoc, whiskerLeft_twice', + ← whiskerRight_left', ← whiskerRight_comp, ε_cond, this, comp_id] + -- have := adj1.left_triangle + -- refine SplitEpi.epi ⟨_, _⟩ + refine ⟨fun {Z} (f₁ f₂ : R ⟶ _) eq => ?_⟩ + -- let X : HasCoequalizers B := sorry + -- have (k : B) : HasColimit + -- ((parallelPair ((U ⋙ F).whiskerLeft adj1.counit) + -- (whiskerRight adj1.counit (U ⋙ F))).flip.obj k) := by + -- let α' := (U ⋙ F).whiskerLeft adj1.counit + -- let β' := whiskerRight adj1.counit (U ⋙ F) + -- let K : Cofork α' β' := adj1.cofork + -- have : α' ≫ adj1.counit = β' ≫ adj1.counit := K.condition + -- change IsColimit K at H + -- dsimp [Cofork] at K + -- let iso := diagramIsoParallelPair ((parallelPair α' β').flip.obj k) + -- let Q : Cocone (parallelPair (α'.app k) (β'.app k)) := + -- Cofork.ofπ (adj1.counit.app k) (by rw [← comp_app, this, comp_app]) + -- refine ⟨_, (IsColimit.ofCoconeEquiv (c := Q) (Cocones.precomposeEquivalence iso)).symm ?_⟩ + -- have := H + -- refine Cofork.IsColimit.mk _ (fun s => (H.desc s).app k) _ _ + -- #exit + -- simp [Cocones.precompose, iso] + -- stop + -- have := preservesCoequalizer _ _ ((whiskeringLeft A B B).obj R) H + have : Epi adj1.counit := Cofork.IsColimit.epi H + have := @this.1 + have := congr(R.whiskerLeft (U.whiskerLeft adj1.unit) ≫ whiskerRight $eq U) + simp at this + rw [whiskerRight_left', ← whiskerLeft_comp_assoc, ← whiskerLeft_comp_assoc, + adj1.right_triangle, whiskerLeft_id', id_comp, id_comp] at this + suffices _ : U.Faithful from faithful_whiskeringRight_obj.1 this + refine ⟨fun {X Y} f g eq => ?_⟩ + sorry + +def coadjointTriangle {C D E : Type*} [Category C] [Category D] [Category E] [HasEqualizers E] + {L : C ⥤ D} {R : D ⥤ C} (adj1 : L ⊣ R) + {L' : E ⥤ C} {R' : D ⥤ E} (adj2 : L' ⋙ L ⊣ R') + (H : IsLimit adj1.fork) : (R₁ : C ⥤ E) × (L' ⊣ R₁) := by + suffices Hop : IsColimit adj1.op.cofork from + have ⟨L, hL⟩ := adjointTriangle adj1.op adj2.op (R := L'.op) Hop + ⟨L.unop, hL.unop⟩ + refine Cofork.IsColimit.mk' _ fun s => ?_ + let π : s.pt.unop ⟶ L ⋙ R := NatTrans.unop s.π + let l := Fork.IsLimit.lift H π (congrArg NatTrans.unop s.condition) + refine have eq := Fork.IsLimit.lift_ι' ..; ⟨NatTrans.op l, congrArg NatTrans.op eq, ?_⟩ + refine fun {m} h => congrArg NatTrans.op (?_ : NatTrans.unop m = _) + exact Fork.IsLimit.hom_ext H ((congrArg NatTrans.unop h).trans eq.symm) + +def mapPullbackAdjComonadic {C} [Category C] [HasPullbacks C] {A B : C} (F : A ⟶ B) : + IsLimit (CategoryTheory.Adjunction.fork (mapPullbackAdj F)) := by + refine Fork.IsLimit.mk' _ fun s => ?_ + dsimp [CategoryTheory.Adjunction.fork] + let ι : s.pt ⟶ Over.map F ⋙ Over.pullback F := Fork.ι s + have w : ι ≫ _ = ι ≫ _ := Fork.condition s + refine ⟨⟨fun X => ?_, fun X Y f => ?_⟩, ?_, ?_⟩ + · simp + let X1 := X.left + let X2 : X1 ⟶ A := X.hom + refine Over.homMk ((ι.app X).left ≫ pullback.fst ..) ?_ + have := congr((($w).app X).left ≫ pullback.fst .. ≫ pullback.snd ..); simp at this ⊢ + rw [← this]; simpa using (ι.app X).w + · ext; simp + have := congr($(ι.naturality f).left ≫ pullback.fst ..); simpa [-naturality] + · ext X; simp; ext <;> simp; · rfl + simpa using congr((($w.symm).app X).left ≫ pullback.fst .. ≫ pullback.snd ..) + · intro m H; ext X + simpa using congr((($H).app X).left ≫ pullback.fst ..) + /-- The pullback of exponentiable morphisms is exponentiable. -/ -def pullback {I J K : C} (f : I ⟶ J) (g : K ⟶ J) - [gexp : ExponentiableMorphism g] : - ExponentiableMorphism (pullback.fst f g ) := - sorry +theorem of_isPullback {C' : Type u} [Category.{v} C'] [HasPullbacks C'] [HasTerminal C'] + {P I J K : C'} {fst : P ⟶ I} {snd : P ⟶ K} {f : I ⟶ J} {g : K ⟶ J} + (H : IsPullback fst snd f g) [ExponentiableMorphism g] : ExponentiableMorphism fst := by + refine ⟨⟨_, ⟨coadjointTriangle (mapPullbackAdj snd) + ((mapPullbackAdj f).comp (adj g) |>.ofNatIsoLeft (pullbackMapIsoSquare H.flip).symm) ?_ |>.2⟩⟩⟩ + apply mapPullbackAdjComonadic end ExponentiableMorphism diff --git a/Poly/UvPoly/Basic.lean b/Poly/UvPoly/Basic.lean index 4e3f06e..66407de 100644 --- a/Poly/UvPoly/Basic.lean +++ b/Poly/UvPoly/Basic.lean @@ -52,7 +52,7 @@ namespace UvPoly open TwoSquare -variable {C : Type*} [Category C] [HasTerminal C] [HasPullbacks C] +variable [HasTerminal C] instance : HasBinaryProducts C := hasBinaryProducts_of_hasTerminal_and_pullbacks C @@ -217,9 +217,10 @@ def comp {E B F D N M : C} {P : UvPoly E B} {Q : UvPoly F D} {R : UvPoly N M} end Hom +variable (C) in /-- Bundling up the the polynomials over different bases to form the underlying type of the category of polynomials. -/ -structure Total (C : Type*) [Category C] [HasPullbacks C] where +structure Total where {E B : C} (poly : UvPoly E B) @@ -248,7 +249,7 @@ def Total.ofHom {E' B' : C} (P : UvPoly E B) (Q : UvPoly E' B') (α : P.Hom Q) : namespace UvPoly -variable {C : Type u} [Category.{v} C] [HasTerminal C] [HasPullbacks C] +variable [HasTerminal C] instance : SMul C (Total C) where smul S P := Total.of (smul S P.poly) @@ -358,10 +359,76 @@ def compDom {E B D A : C} (P : UvPoly E B) (Q : UvPoly D A) := Limits.pullback Q.p (fan P A).snd @[simps!] -def comp [HasPullbacks C] [HasTerminal C] - {E B D A : C} (P : UvPoly E B) (Q : UvPoly D A) : UvPoly (compDom P Q) (P @ A) where - p := pullback.snd Q.p (fan P A).snd ≫ pullback.fst (fan P A).fst P.p - exp := sorry +def comp {E B D A : C} (P : UvPoly E B) (Q : UvPoly D A) : UvPoly (compDom P Q) (P @ A) := by + letI p := pullback.snd Q.p (fan P A).snd ≫ pullback.fst (fan P A).fst P.p + refine { p, exp.exists_rightAdjoint := ?_ } + let F1 := map (P.fstProj A) ⋙ Over.pullback P.p + let G1 := pushforward P.p ⋙ Over.pullback (P.fstProj A) + let adj1 : F1 ⊣ G1 := mapPullbackAdj (P.fstProj A) |>.comp (adj P.p) + let F2 := Over.pullback (pullback.fst (fan P A).fst P.p) + let G2 := map (pullback.snd (fan P A).fst P.p) + let F3 := map (fan P A).snd ⋙ Over.pullback Q.p + let G3 := pushforward Q.p ⋙ Over.pullback (fan P A).snd + let adj2 : F3 ⊣ G3 := mapPullbackAdj (fan P A).snd |>.comp (adj Q.p) + let G4 := map (pullback.fst Q.p (fan P A).snd) + let F5 := map p + let G5 := Over.pullback p + let adj3 : F5 ⊣ G5 := mapPullbackAdj p + suffices G5 ⊣ G4 ⋙ G3 ⋙ G2 ⋙ G1 from ⟨_, ⟨this⟩⟩ + refine { + unit := { + app Y := ?_ + naturality := sorry + } + counit := { + app X := ?_ + naturality := ?_ + } + left_triangle_components := sorry + right_triangle_components := sorry + } + · + change Y ⟶ (G5 ⋙ G4 ⋙ G3 ⋙ G2 ⋙ G1).obj Y + refine adj1.homEquiv _ _ ?_ + let f : F1.obj Y ⟶ (F2 ⋙ G2).obj Y := + Over.homMk (pullback.lift (pullback.fst ..) + (pullback.lift (pullback.fst .. ≫ Y.hom) (pullback.snd ..) + ?_) ?_) ?_ + refine f ≫ G2.map ?_ + refine adj2.homEquiv _ _ ?_ + refine ?_ ≫ G4.map (adj3.homEquiv (G5.obj Y) _ (Over.homMk (pullback.fst ..) ?_)) + refine Over.homMk (pullback.lift + (pullback.fst .. ≫ pullback.fst ..) + (pullback.lift (pullback.snd ..) + (pullback.fst .. ≫ pullback.snd ..) ?_) + ?_) ?_ + · simp [← pullback.condition, F2] + · simp only [assoc, pullback.condition, limit.lift_π_assoc, PullbackCone.mk_π_app, p] + · simp only [F3, F2, G4, G5, map_obj_hom, pullback_obj_hom, comp_obj] + rw [pullback.lift_snd_assoc, pullback.lift_fst] + · rw [pullback.condition]; rfl + · rw [← pullback.condition, assoc]; rfl + · rw [pullback.lift_fst] + · simp only [F2, G2, comp_obj, map_obj_hom, pullback_obj_hom] + rw [pullback.lift_snd_assoc, pullback.lift_snd]; rfl + dsimp + + done + -- simp + -- simp only [comp_obj, map_obj_hom, id_obj, + -- const_obj_obj, pullback_obj_hom, limit.lift_π_assoc, PullbackCone.mk_pt, cospan_right, + -- PullbackCone.mk_π_app, limit.lift_π, F3, F2, G4, G5] + + -- · simp [pullback.condition, F5, G5] + · + dsimp -- [G1,G2,G3,G4,G5] + have f X : G5.obj X ⟶ F1.obj X := + _ + refine adj1.counit + have := _ ≫ @(adj P.p).counit.app _ ≫ _; simp at this + refine ((mapPullbackAdj _).homEquiv _ _).symm ?_ + + done /-- The associated functor of the composition of two polynomials is isomorphic to the composition of the associated functors. -/ def compFunctorIso [HasPullbacks C] [HasTerminal C] @@ -378,6 +445,7 @@ instance monoidal [HasPullbacks C] [HasTerminal C] : MonoidalCategory (UvPoly.To leftUnitor := sorry rightUnitor := sorry +#print sorries UvPoly.comp UvPoly.PartialProduct.isLimitFan partialProd.lift_snd partialProd.hom_ext end UvPoly end CategoryTheory end From 68950eba8f80300988148b6c3edb9fa5680b4a7b Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Fri, 19 Sep 2025 01:48:05 +0200 Subject: [PATCH 2/4] finished --- .../Distributivity.lean | 120 ++++++------------ 1 file changed, 37 insertions(+), 83 deletions(-) diff --git a/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Distributivity.lean b/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Distributivity.lean index 6da44f2..5d780c4 100644 --- a/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Distributivity.lean +++ b/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Distributivity.lean @@ -107,60 +107,40 @@ def preservesCoequalizer {C D} [Category C] [Category D] {X Y : C} {f g : X ⟶ |>.ofIsoColimit (Cofork.ext (Iso.refl _) ?_) simp [Cocones.precompose, Cofork.π, iso] --- theorem whiskeringLeft_preservesEpi {C D E} [Category C] [Category D] [Category E] (F : C ⥤ D) --- : ((whiskeringLeft C D E).obj F).PreservesEpimorphisms := by --- refine ⟨fun {G G'} f ⟨hf⟩ => ⟨fun {K} g h eq => ?_⟩⟩ --- ext X --- replace eq := congr(($eq).app X) --- dsimp at g h eq --- exact hf _ _ eq - - - --- have := isColimitOfPreserves F H --- let iso : parallelPair f g ⋙ F ≅ parallelPair (F.map f) (F.map g) := diagramIsoParallelPair _ --- refine (IsColimit.ofCoconeEquiv (Cocones.precomposeEquivalence iso.symm)).symm this --- |>.ofIsoColimit (Cofork.ext (Iso.refl _) ?_) --- simp [Cocones.precompose, Cofork.π, iso] - --- instance evaluation_preservesColimit --- {C : Type u} [Category.{v} C] {J : Type u₁} [Category.{v₁} J] {K : Type u₂} [Category.{v₂} K] --- (F : J ⥤ K ⥤ C) (k : K) : --- PreservesColimit F ((evaluation K C).obj k) := by --- refine ⟨fun h' => ⟨fun s => ?_, ?_, ?_⟩⟩ --- · simp --- have := s.ι.app; simp at this --- -- have := h'.desc precompose --- have := h'.desc ⟨_, fun x => by --- have := s.ι.app x --- dsimp at this - --- simp, _⟩ - -- let X : (k : K) → ColimitCocone (F.flip.obj k) := fun k => getColimitCocone (F.flip.obj k) - -- preservesColimit_of_preserves_colimit_cocone (combinedIsColimit _ X) <| - -- IsColimit.ofIsoColimit (colimit.isColimit _) (evaluateCombinedCocones F X k).symm - --- instance whiskeringLeft_preservesColimit --- {C : Type u₁} [Category.{v₁} C] --- {D : Type u₂} [Category.{v₂} D] --- {E : Type u₃} [Category.{v₃} E] --- (J : Type u) [Category.{v} J] --- (K : J ⥤ E ⥤ D) (F : C ⥤ E) --- -- [∀ (k : E), HasColimit (K.flip.obj k)] --- : --- PreservesColimit K ((whiskeringLeft C E D).obj F) := --- ⟨fun c {hc} => ⟨by --- apply evaluationJointlyReflectsColimits --- intro Y --- change IsColimit (((evaluation E D).obj (F.obj Y)).mapCocone c) --- have := evaluation_preservesColimit K (F.obj Y) --- exact isColimitOfPreserves _ hc⟩⟩ +theorem evaluation_preservesMonomorphisms {C} (D) + [Category C] [Category D] [HasPullbacks D] (X : C) : + ((evaluation C D).obj X).PreservesMonomorphisms := by + refine ⟨fun {A B} f _ => ?_⟩ + have : IsPullback (𝟙 _) (𝟙 _) f f := by + refine ⟨⟨rfl⟩, ⟨Limits.PullbackCone.IsLimit.mk _ (·.fst) (by simp) (fun s => ?_) ?_⟩⟩ + · simpa using (cancel_mono f).1 s.condition + · intro s m h1 h2; simpa using h1 + suffices IsPullback (𝟙 _) (𝟙 _) (f.app X) (f.app X) from + ⟨fun {Z} g h eq => (this.lift_fst _ _ eq).symm.trans (this.lift_snd _ _ eq)⟩ + have := + (IsLimit.ofConeEquiv (Cones.postcomposeEquivalence (cospanCompIso ..))).symm <| + isLimitOfPreserves ((evaluation C D).obj X) this.2.some + refine ⟨⟨rfl⟩, ⟨.ofIsoLimit this <| PullbackCone.ext (Iso.refl _) ?_ ?_⟩⟩ <;> + simp [PullbackCone.fst, PullbackCone.snd] + +theorem evaluation_preservesEpimorphisms {C} (D) + [Category C] [Category D] [HasPushouts D] (X : C) : + ((evaluation C D).obj X).PreservesEpimorphisms := by + refine ⟨fun f _ => ⟨fun {Z} g h eq => ?_⟩⟩ + have : Mono (NatTrans.op f) := by + refine ⟨fun g h eq => ?_⟩ + have := congrArg NatTrans.unop eq; simp at this + exact congrArg NatTrans.op ((cancel_epi f).1 this) + have := evaluation_preservesMonomorphisms Dᵒᵖ (Opposite.op X) + have := (this.1 (NatTrans.op f)).1 (Z := .op Z) g.op h.op (by simpa using congr(($eq).op)) + exact congr(($this).unop) attribute [-simp] whiskerLeft_twice whiskerRight_twice in -def adjointTriangle {B C A : Type*} [Category B] [Category C] [Category A] [HasCoequalizers A] +theorem adjointTriangle {B C A : Type*} [Category B] [Category C] [Category A] [HasCoequalizers A] + [HasPushouts B] -- FIXME: Dubuc didn't need this assumption {U : B ⥤ C} {F : C ⥤ B} (adj1 : F ⊣ U) {R : A ⥤ B} {F' : C ⥤ A} (adj2 : F' ⊣ R ⋙ U) - (H : IsColimit adj1.cofork) : (L : B ⥤ A) × (L ⊣ R) := by + (H : IsColimit adj1.cofork) : Nonempty <| (L : B ⥤ A) × (L ⊣ R) := by let θ : F ⟶ F' ⋙ R := ((mateEquiv adj2 adj1).symm (.mk _ R (𝟭 _) _ (𝟙 _))).natTrans let α : U ⋙ F ⋙ U ⋙ F' ⟶ U ⋙ F' := whiskerRight adj1.counit (U ⋙ F') let β : U ⋙ F ⋙ U ⋙ F' ⟶ U ⋙ F' := @@ -229,45 +209,19 @@ def adjointTriangle {B C A : Type*} [Category B] [Category C] [Category A] [HasC refine (cancel_epi (R.whiskerLeft adj1.counit)).1 ?_ rw [← whiskerLeft_comp_assoc, η_cond, whiskerLeft_comp_assoc, whiskerLeft_twice', ← whiskerRight_left', ← whiskerRight_comp, ε_cond, this, comp_id] - -- have := adj1.left_triangle - -- refine SplitEpi.epi ⟨_, _⟩ refine ⟨fun {Z} (f₁ f₂ : R ⟶ _) eq => ?_⟩ - -- let X : HasCoequalizers B := sorry - -- have (k : B) : HasColimit - -- ((parallelPair ((U ⋙ F).whiskerLeft adj1.counit) - -- (whiskerRight adj1.counit (U ⋙ F))).flip.obj k) := by - -- let α' := (U ⋙ F).whiskerLeft adj1.counit - -- let β' := whiskerRight adj1.counit (U ⋙ F) - -- let K : Cofork α' β' := adj1.cofork - -- have : α' ≫ adj1.counit = β' ≫ adj1.counit := K.condition - -- change IsColimit K at H - -- dsimp [Cofork] at K - -- let iso := diagramIsoParallelPair ((parallelPair α' β').flip.obj k) - -- let Q : Cocone (parallelPair (α'.app k) (β'.app k)) := - -- Cofork.ofπ (adj1.counit.app k) (by rw [← comp_app, this, comp_app]) - -- refine ⟨_, (IsColimit.ofCoconeEquiv (c := Q) (Cocones.precomposeEquivalence iso)).symm ?_⟩ - -- have := H - -- refine Cofork.IsColimit.mk _ (fun s => (H.desc s).app k) _ _ - -- #exit - -- simp [Cocones.precompose, iso] - -- stop - -- have := preservesCoequalizer _ _ ((whiskeringLeft A B B).obj R) H + ext a have : Epi adj1.counit := Cofork.IsColimit.epi H - have := @this.1 - have := congr(R.whiskerLeft (U.whiskerLeft adj1.unit) ≫ whiskerRight $eq U) - simp at this - rw [whiskerRight_left', ← whiskerLeft_comp_assoc, ← whiskerLeft_comp_assoc, - adj1.right_triangle, whiskerLeft_id', id_comp, id_comp] at this - suffices _ : U.Faithful from faithful_whiskeringRight_obj.1 this - refine ⟨fun {X Y} f g eq => ?_⟩ - sorry - -def coadjointTriangle {C D E : Type*} [Category C] [Category D] [Category E] [HasEqualizers E] + have := (evaluation_preservesEpimorphisms _ (R.obj a)).1 adj1.counit + replace eq := congr(($eq).app a); simp at eq + exact this.1 _ _ eq + +def coadjointTriangle {C D E : Type*} [Category C] [Category D] [Category E] [HasEqualizers E] [HasPullbacks C] {L : C ⥤ D} {R : D ⥤ C} (adj1 : L ⊣ R) {L' : E ⥤ C} {R' : D ⥤ E} (adj2 : L' ⋙ L ⊣ R') (H : IsLimit adj1.fork) : (R₁ : C ⥤ E) × (L' ⊣ R₁) := by suffices Hop : IsColimit adj1.op.cofork from - have ⟨L, hL⟩ := adjointTriangle adj1.op adj2.op (R := L'.op) Hop + have ⟨L, hL⟩ := (adjointTriangle adj1.op adj2.op (R := L'.op) Hop).some ⟨L.unop, hL.unop⟩ refine Cofork.IsColimit.mk' _ fun s => ?_ let π : s.pt.unop ⟶ L ⋙ R := NatTrans.unop s.π From dd04acfc5c10ac0b05d23826cb2868e98d21a026 Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Fri, 19 Sep 2025 02:35:47 +0200 Subject: [PATCH 3/4] mathlib already had it... --- .../Distributivity.lean | 216 ++---------------- 1 file changed, 16 insertions(+), 200 deletions(-) diff --git a/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Distributivity.lean b/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Distributivity.lean index 5d780c4..cd0fba9 100644 --- a/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Distributivity.lean +++ b/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Distributivity.lean @@ -3,9 +3,7 @@ Copyright (c) 2025 Sina Hazratpour. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Sina Hazratpour, Emily Riehl -/ -import Mathlib.CategoryTheory.Limits.Shapes.Pullback.CommSq -import Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory -import Mathlib.CategoryTheory.Adjunction.Opposites +import Mathlib.CategoryTheory.Adjunction.Lifting.Right import Poly.ForMathlib.CategoryTheory.LocallyCartesianClosed.Basic import Poly.ForMathlib.CategoryTheory.NatTrans import Poly.ForMathlib.CategoryTheory.LocallyCartesianClosed.BeckChevalley @@ -56,207 +54,25 @@ def exponentiableMorphism : ExponentiableMorphism (g f u) := by infer_instance namespace ExponentiableMorphism -structure IsCoequalizer {C} [Category C] {A B L : C} (f g : A ⟶ B) {L} (π : B ⟶ L) : Prop where - w : f ≫ π = g ≫ π - isColimit : Nonempty (IsColimit (Cofork.ofπ π w)) - -def CategoryTheory.Adjunction.cofork {C D} [Category C] [Category D] - {F : C ⥤ D} {U : D ⥤ C} (adj : F ⊣ U) : - Cofork (whiskerLeft (U ⋙ F) adj.counit) (whiskerRight adj.counit (U ⋙ F)) := - .ofπ adj.counit (whiskerLeft_comp_whiskerRight adj.counit adj.counit) - -def CategoryTheory.Adjunction.fork {C D} [Category C] [Category D] - {F : C ⥤ D} {U : D ⥤ C} (adj : F ⊣ U) : - Fork (whiskerLeft (F ⋙ U) adj.unit) (whiskerRight adj.unit (F ⋙ U)) := - .ofι adj.unit (whiskerLeft_comp_whiskerRight adj.unit adj.unit).symm - -theorem associator_eq_id {C D E E'} [Category C] [Category D] [Category E] [Category E'] - (F : C ⥤ D) (G : D ⥤ E) (H : E ⥤ E') : Functor.associator F G H = Iso.refl (F ⋙ G ⋙ H) := rfl - -theorem whiskerRight_left' {C D E B} [Category C] [Category D] [Category E] [Category B] - (F : B ⥤ C) {G H : C ⥤ D} (α : G ⟶ H) (K : D ⥤ E) : - whiskerRight (whiskerLeft F α) K = whiskerLeft F (whiskerRight α K) := rfl - -theorem id_whiskerLeft' {C D} [Category C] [Category D] {G H : C ⥤ D} (α : G ⟶ H) : - whiskerLeft (𝟭 C) α = α := rfl - -theorem id_whiskerRight' {C D} [Category C] [Category D] {G H : C ⥤ D} (α : G ⟶ H) : - whiskerRight α (𝟭 D) = α := rfl - -theorem whiskerLeft_twice' {C D E B} [Category C] [Category D] [Category E] [Category B] - (F : B ⥤ C) (G : C ⥤ D) {H K : D ⥤ E} (α : H ⟶ K) : - whiskerLeft F (whiskerLeft G α) = whiskerLeft (F ⋙ G) α := rfl - -theorem whiskerRight_twice' {C D E B} [Category C] [Category D] [Category E] [Category B] - {H K : B ⥤ C} (F : C ⥤ D) (G : D ⥤ E) (α : H ⟶ K) : - whiskerRight (whiskerRight α F) G = whiskerRight α (F ⋙ G) := rfl - -abbrev Cofork.π' {C} [Category C] {X Y : C} {f g : X ⟶ Y} (s : Cofork f g) : Y ⟶ s.pt := s.π - -def parallelPairComp {C D} [Category C] [Category D] {X Y : C} {f g : X ⟶ Y} (F : C ⥤ D) : - parallelPair f g ⋙ F ≅ parallelPair (F.map f) (F.map g) := diagramIsoParallelPair _ - -def preservesCoequalizer {C D} [Category C] [Category D] {X Y : C} {f g : X ⟶ Y} - {P : C} (π : Y ⟶ P) (w : f ≫ π = g ≫ π) (F : C ⥤ D) - (H : IsColimit (Cofork.ofπ π w)) [PreservesColimit (parallelPair f g) F] : - IsColimit (Cofork.ofπ (f := F.map f) (g := F.map g) (F.map π) - (by rw [← map_comp, w, map_comp])) := by - have := isColimitOfPreserves F H - let iso : parallelPair f g ⋙ F ≅ parallelPair (F.map f) (F.map g) := diagramIsoParallelPair _ - refine (IsColimit.ofCoconeEquiv (Cocones.precomposeEquivalence iso.symm)).symm this - |>.ofIsoColimit (Cofork.ext (Iso.refl _) ?_) - simp [Cocones.precompose, Cofork.π, iso] - -theorem evaluation_preservesMonomorphisms {C} (D) - [Category C] [Category D] [HasPullbacks D] (X : C) : - ((evaluation C D).obj X).PreservesMonomorphisms := by - refine ⟨fun {A B} f _ => ?_⟩ - have : IsPullback (𝟙 _) (𝟙 _) f f := by - refine ⟨⟨rfl⟩, ⟨Limits.PullbackCone.IsLimit.mk _ (·.fst) (by simp) (fun s => ?_) ?_⟩⟩ - · simpa using (cancel_mono f).1 s.condition - · intro s m h1 h2; simpa using h1 - suffices IsPullback (𝟙 _) (𝟙 _) (f.app X) (f.app X) from - ⟨fun {Z} g h eq => (this.lift_fst _ _ eq).symm.trans (this.lift_snd _ _ eq)⟩ - have := - (IsLimit.ofConeEquiv (Cones.postcomposeEquivalence (cospanCompIso ..))).symm <| - isLimitOfPreserves ((evaluation C D).obj X) this.2.some - refine ⟨⟨rfl⟩, ⟨.ofIsoLimit this <| PullbackCone.ext (Iso.refl _) ?_ ?_⟩⟩ <;> - simp [PullbackCone.fst, PullbackCone.snd] - -theorem evaluation_preservesEpimorphisms {C} (D) - [Category C] [Category D] [HasPushouts D] (X : C) : - ((evaluation C D).obj X).PreservesEpimorphisms := by - refine ⟨fun f _ => ⟨fun {Z} g h eq => ?_⟩⟩ - have : Mono (NatTrans.op f) := by - refine ⟨fun g h eq => ?_⟩ - have := congrArg NatTrans.unop eq; simp at this - exact congrArg NatTrans.op ((cancel_epi f).1 this) - have := evaluation_preservesMonomorphisms Dᵒᵖ (Opposite.op X) - have := (this.1 (NatTrans.op f)).1 (Z := .op Z) g.op h.op (by simpa using congr(($eq).op)) - exact congr(($this).unop) - -attribute [-simp] whiskerLeft_twice whiskerRight_twice in -theorem adjointTriangle {B C A : Type*} [Category B] [Category C] [Category A] [HasCoequalizers A] - [HasPushouts B] -- FIXME: Dubuc didn't need this assumption - {U : B ⥤ C} {F : C ⥤ B} (adj1 : F ⊣ U) - {R : A ⥤ B} {F' : C ⥤ A} (adj2 : F' ⊣ R ⋙ U) - (H : IsColimit adj1.cofork) : Nonempty <| (L : B ⥤ A) × (L ⊣ R) := by - let θ : F ⟶ F' ⋙ R := ((mateEquiv adj2 adj1).symm (.mk _ R (𝟭 _) _ (𝟙 _))).natTrans - let α : U ⋙ F ⋙ U ⋙ F' ⟶ U ⋙ F' := whiskerRight adj1.counit (U ⋙ F') - let β : U ⋙ F ⋙ U ⋙ F' ⟶ U ⋙ F' := - whiskerLeft U (whiskerRight θ (U ⋙ F')) ≫ whiskerLeft (U ⋙ F') adj2.counit - let L := coequalizer α β; use L - let π : _ ⟶ L := coequalizer.π .. - have eq : α ≫ π = β ≫ π := coequalizer.condition .. - have : whiskerLeft (R ⋙ U) θ ≫ whiskerRight adj2.counit R = whiskerLeft R adj1.counit := by - ext X; simp [θ] - have := adj2.right_triangle_components X; dsimp at this - rw [← counit_naturality, ← map_comp_assoc, this]; simp - let preserves : IsColimit (Cofork.ofπ - (f := whiskerLeft R α) (g := whiskerLeft R β) (whiskerLeft R π) _) := - preservesCoequalizer π eq ((whiskeringLeft A B A).obj R) (coequalizerIsCoequalizer ..) - let iso Y : (coequalizer α β).obj Y ≅ coequalizer (α.app Y) (β.app Y) := - letI J := _ - (colimitObjIsoColimitCompEvaluation (parallelPair α β) Y : _ ≅ colimit J).trans <| - colim.mapIso (diagramIsoParallelPair J) - refine - let η := H.desc (Cofork.ofπ (P := L ⋙ R) (whiskerLeft U θ ≫ whiskerRight π R) ?_) - let ε := preserves.desc (Cofork.ofπ adj2.counit ?_) - have η_cond : adj1.counit ≫ η = U.whiskerLeft θ ≫ whiskerRight π R := Cofork.IsColimit.π_desc H - have ε_cond : R.whiskerLeft π ≫ ε = adj2.counit := Cofork.IsColimit.π_desc preserves - .mkOfUnitCounit { - unit := η, counit := ε, left_triangle := (?_ : _ = 𝟙 _), right_triangle := (?_ : _ = 𝟙 _) } - · replace eq := congr(whiskerLeft (U ⋙ F ⋙ U) θ ≫ whiskerRight $eq R) - simp [α, β] at eq - conv_rhs at eq => - conv => enter [2,1]; apply whiskerRight_left' - rw [← whiskerLeft_twice', ← whiskerLeft_twice', ← whiskerLeft_comp_assoc] - conv => enter [1,2]; apply whiskerLeft_comp_whiskerRight - rw [whiskerLeft_comp_assoc]; - conv => - arg 2 - rw [whiskerRight_left', ← whiskerLeft_twice', ← whiskerLeft_twice'] - rw [← whiskerLeft_comp_assoc, ← whiskerLeft_comp] - enter [1,2,2]; rw [whiskerLeft_twice', this] - rw [← whiskerLeft_comp_assoc] - conv => enter [1,2]; apply (whiskerLeft_comp_whiskerRight ..).symm - rw [id_whiskerRight', whiskerLeft_comp_assoc, whiskerLeft_twice'] - rw [← eq, ← whiskerRight_twice', whiskerRight_twice'] - apply whiskerLeft_comp_whiskerRight_assoc - · simp [α, β]; rw [← whiskerRight_left', ← this] - rw [whiskerRight_comp_assoc, whiskerRight_left', whiskerLeft_twice']; congr 1 - exact (whiskerLeft_comp_whiskerRight adj2.counit adj2.counit).symm - · simp [associator_eq_id] - conv_lhs => arg 2; apply id_comp - have _ : Epi π := (Cofork.IsColimit.epi (coequalizerIsCoequalizer α β) :) - have _ : Epi (whiskerRight adj1.counit (U ⋙ F')) := by - refine SplitEpi.epi ⟨whiskerRight (whiskerLeft U adj1.unit) F', ?_⟩ - rw [← whiskerRight_twice', ← whiskerRight_comp, adj1.right_triangle] - apply whiskerRight_id - rw [← cancel_epi π, ← cancel_epi (whiskerRight adj1.counit (U ⋙ F'))] - conv_rhs => arg 2; apply comp_id - have := whiskerLeft_comp_whiskerRight adj1.counit π - rw [id_whiskerLeft'] at this; rw [← reassoc_of% this]; clear this - rw [← whiskerRight_comp_assoc, η_cond, whiskerRight_comp_assoc, - whiskerRight_left', ← whiskerLeft_twice', ← whiskerLeft_comp_assoc, - whiskerLeft_comp_whiskerRight, whiskerLeft_comp_assoc, whiskerLeft_twice'] - conv_lhs => arg 2; apply reassoc_of% whiskerLeft_comp_whiskerRight - rw [← whiskerLeft_twice', ← whiskerLeft_comp, ε_cond] - conv_lhs => arg 2; apply (whiskerLeft_comp_whiskerRight π adj2.counit).symm - rw [id_whiskerRight', ← assoc]; exact eq.symm - · simp [associator_eq_id] - suffices _ : Epi (R.whiskerLeft adj1.counit) by - refine (cancel_epi (R.whiskerLeft adj1.counit)).1 ?_ - rw [← whiskerLeft_comp_assoc, η_cond, whiskerLeft_comp_assoc, whiskerLeft_twice', - ← whiskerRight_left', ← whiskerRight_comp, ε_cond, this, comp_id] - refine ⟨fun {Z} (f₁ f₂ : R ⟶ _) eq => ?_⟩ - ext a - have : Epi adj1.counit := Cofork.IsColimit.epi H - have := (evaluation_preservesEpimorphisms _ (R.obj a)).1 adj1.counit - replace eq := congr(($eq).app a); simp at eq - exact this.1 _ _ eq - -def coadjointTriangle {C D E : Type*} [Category C] [Category D] [Category E] [HasEqualizers E] [HasPullbacks C] - {L : C ⥤ D} {R : D ⥤ C} (adj1 : L ⊣ R) - {L' : E ⥤ C} {R' : D ⥤ E} (adj2 : L' ⋙ L ⊣ R') - (H : IsLimit adj1.fork) : (R₁ : C ⥤ E) × (L' ⊣ R₁) := by - suffices Hop : IsColimit adj1.op.cofork from - have ⟨L, hL⟩ := (adjointTriangle adj1.op adj2.op (R := L'.op) Hop).some - ⟨L.unop, hL.unop⟩ - refine Cofork.IsColimit.mk' _ fun s => ?_ - let π : s.pt.unop ⟶ L ⋙ R := NatTrans.unop s.π - let l := Fork.IsLimit.lift H π (congrArg NatTrans.unop s.condition) - refine have eq := Fork.IsLimit.lift_ι' ..; ⟨NatTrans.op l, congrArg NatTrans.op eq, ?_⟩ - refine fun {m} h => congrArg NatTrans.op (?_ : NatTrans.unop m = _) - exact Fork.IsLimit.hom_ext H ((congrArg NatTrans.unop h).trans eq.symm) - -def mapPullbackAdjComonadic {C} [Category C] [HasPullbacks C] {A B : C} (F : A ⟶ B) : - IsLimit (CategoryTheory.Adjunction.fork (mapPullbackAdj F)) := by - refine Fork.IsLimit.mk' _ fun s => ?_ - dsimp [CategoryTheory.Adjunction.fork] - let ι : s.pt ⟶ Over.map F ⋙ Over.pullback F := Fork.ι s - have w : ι ≫ _ = ι ≫ _ := Fork.condition s - refine ⟨⟨fun X => ?_, fun X Y f => ?_⟩, ?_, ?_⟩ - · simp - let X1 := X.left - let X2 : X1 ⟶ A := X.hom - refine Over.homMk ((ι.app X).left ≫ pullback.fst ..) ?_ - have := congr((($w).app X).left ≫ pullback.fst .. ≫ pullback.snd ..); simp at this ⊢ - rw [← this]; simpa using (ι.app X).w - · ext; simp - have := congr($(ι.naturality f).left ≫ pullback.fst ..); simpa [-naturality] - · ext X; simp; ext <;> simp; · rfl - simpa using congr((($w.symm).app X).left ≫ pullback.fst .. ≫ pullback.snd ..) - · intro m H; ext X - simpa using congr((($H).app X).left ≫ pullback.fst ..) +instance mapPullbackAdj_regularMono {C} [Category C] [HasPullbacks C] {A B : C} (F : A ⟶ B) + (X : Over A) : RegularMono ((mapPullbackAdj F).unit.app X) := by + let FU := Over.map F ⋙ Over.pullback F + set η := (mapPullbackAdj F).unit + have := congr($((whiskerLeft_comp_whiskerRight η η)).app X) + refine ⟨_, _, _, this, Fork.IsLimit.mk' _ fun s => ?_⟩ + have hi := (Fork.ι s).w; simp at hi + have w := congr($(Fork.condition s).left ≫ pullback.fst .. ≫ pullback.snd ..); simp [η] at w + refine ⟨homMk (s.ι.left ≫ pullback.fst ..) (by simp [w, hi]), ?_, ?_⟩ + · ext; simp; ext <;> simp [η]; rw [w] + · intro m H; ext; simpa [η] using congr(($H).left ≫ pullback.fst ..) /-- The pullback of exponentiable morphisms is exponentiable. -/ theorem of_isPullback {C' : Type u} [Category.{v} C'] [HasPullbacks C'] [HasTerminal C'] {P I J K : C'} {fst : P ⟶ I} {snd : P ⟶ K} {f : I ⟶ J} {g : K ⟶ J} - (H : IsPullback fst snd f g) [ExponentiableMorphism g] : ExponentiableMorphism fst := by - refine ⟨⟨_, ⟨coadjointTriangle (mapPullbackAdj snd) - ((mapPullbackAdj f).comp (adj g) |>.ofNatIsoLeft (pullbackMapIsoSquare H.flip).symm) ?_ |>.2⟩⟩⟩ - apply mapPullbackAdjComonadic + (H : IsPullback fst snd f g) [ExponentiableMorphism g] : ExponentiableMorphism fst := + have : IsLeftAdjoint _ := + ⟨_, ⟨(mapPullbackAdj f).comp (adj g) |>.ofNatIsoLeft (pullbackMapIsoSquare H.flip).symm⟩⟩ + isLeftAdjoint_triangle_lift (Over.pullback fst) (mapPullbackAdj snd) end ExponentiableMorphism From 56ac18da62ca5ddcdd7b13c63542bbcd06ecc7bc Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Fri, 19 Sep 2025 02:46:40 +0200 Subject: [PATCH 4/4] composition is exponentiable --- Poly/UvPoly/Basic.lean | 105 +++++++++-------------------------------- 1 file changed, 21 insertions(+), 84 deletions(-) diff --git a/Poly/UvPoly/Basic.lean b/Poly/UvPoly/Basic.lean index 66407de..74e0d4f 100644 --- a/Poly/UvPoly/Basic.lean +++ b/Poly/UvPoly/Basic.lean @@ -5,6 +5,7 @@ Authors: Sina Hazratpour, Wojciech Nawrocki -/ import Poly.ForMathlib.CategoryTheory.LocallyCartesianClosed.BeckChevalley -- LCCC.BeckChevalley +import Poly.ForMathlib.CategoryTheory.LocallyCartesianClosed.Distributivity import Mathlib.CategoryTheory.Functor.TwoSquare import Poly.ForMathlib.CategoryTheory.PartialProduct import Poly.ForMathlib.CategoryTheory.NatTrans @@ -36,7 +37,7 @@ noncomputable section namespace CategoryTheory -open CategoryTheory Category Limits Functor Adjunction Over ExponentiableMorphism +open Category Limits Functor Adjunction Over ExponentiableMorphism LocallyCartesianClosed variable {C : Type*} [Category C] [HasPullbacks C] @@ -74,7 +75,7 @@ def prod {E' B'} (P : UvPoly E B) (Q : UvPoly E' B') [HasBinaryCoproducts C] : /-- For a category `C` with binary products, `P.functor : C ⥤ C` is the functor associated to a single variable polynomial `P : UvPoly E B`. -/ def functor (P : UvPoly E B) : C ⥤ C := - star E ⋙ pushforward P.p ⋙ forget B + star E ⋙ pushforward P.p ⋙ Over.forget B /-- The evaluation function of a polynomial `P` at an object `X`. -/ def apply (P : UvPoly E B) : C → C := (P.functor).obj @@ -93,8 +94,8 @@ variable (B) def id : UvPoly B B := ⟨𝟙 B, by infer_instance⟩ /-- The functor associated to the identity polynomial is isomorphic to the identity functor. -/ -def idIso : (UvPoly.id B).functor ≅ star B ⋙ forget B := - isoWhiskerRight (isoWhiskerLeft _ (pushforwardIdIso B)) (forget B) +def idIso : (UvPoly.id B).functor ≅ star B ⋙ Over.forget B := + isoWhiskerRight (isoWhiskerLeft _ (pushforwardIdIso B)) (Over.forget B) /-- Evaluating the identity polynomial at an object `X` is isomorphic to `B × X`. -/ def idApplyIso (X : C) : (id B) @ X ≅ B ⨯ X := sorry @@ -136,7 +137,7 @@ def verticalNatTrans {F : C} (P : UvPoly E B) (Q : UvPoly F B) (ρ : E ⟶ F) (h let cellLeft := (Over.starPullbackIsoStar ρ).hom let cellMid := (pushforwardPullbackTwoSquare ρ P.p Q.p (𝟙 _) sq) let cellLeftMidPasted := TwoSquare.whiskerRight (cellLeft ≫ₕ cellMid) (Over.pullbackId).inv - simpa using (cellLeftMidPasted ≫ₕ (vId (forget B))) + simpa using (cellLeftMidPasted ≫ₕ (vId (Over.forget B))) /-- A cartesian map of polynomials ``` @@ -166,7 +167,7 @@ def cartesianNatTrans {D F : C} (P : UvPoly E B) (Q : UvPoly F D) (Over.starPullbackIsoStar φ).inv let cellMid : TwoSquare (pullback φ) (pushforward Q.p) (pushforward P.p) (pullback δ) := (pushforwardPullbackIsoSquare pb.flip).inv - let cellRight : TwoSquare (pullback δ) (forget D) (forget B) (𝟭 C) := + let cellRight : TwoSquare (pullback δ) (Over.forget D) (Over.forget B) (𝟭 C) := pullbackForgetTwoSquare δ let := cellLeft ≫ᵥ cellMid ≫ᵥ cellRight this @@ -276,7 +277,7 @@ def ε (P : UvPoly E B) (X : C) : pullback (P.fstProj X) P.p ⟶ E ⨯ X := /-- The partial product fan associated to a polynomial `P : UvPoly E B` and an object `X : C`. -/ @[simps -isSimp] -def fan (P : UvPoly E B) (X : C) : Fan P.p X where +def fan (P : UvPoly E B) (X : C) : PartialProduct.Fan P.p X where pt := P @ X fst := P.fstProj X snd := ε P X ≫ prod.snd -- ((forgetAdjStar E).counit).app X @@ -287,12 +288,12 @@ attribute [simp] fan_pt fan_fst `P.PartialProduct.fan` is in fact a limit fan; this provides the univeral mapping property of the polynomial functor. -/ -def isLimitFan (P : UvPoly E B) (X : C) : IsLimit (fan P X) where +def isLimitFan (P : UvPoly E B) (X : C) : PartialProduct.IsLimit (PartialProduct.fan P X) where lift c := (pushforwardCurry <| overPullbackToStar c.fst c.snd).left fac_left := by aesop_cat (add norm fstProj) fac_right := by intro c - simp only [fan_snd, pullbackMap, ε, ev, ← assoc, ← comp_left] + simp only [fan_snd, PartialProduct.pullbackMap, ε, ev, ← assoc, ← comp_left] simp_rw [homMk_eta] erw [← homEquiv_counit] simp [← ExponentiableMorphism.homEquiv_apply_eq, overPullbackToStar_prod_snd] @@ -303,7 +304,7 @@ def isLimitFan (P : UvPoly E B) (X : C) : IsLimit (fan P X) where rw [← homMk_left m (U := Over.mk c.fst) (V := Over.mk (P.fstProj X))] congr 1 apply (Adjunction.homEquiv_apply_eq (adj P.p) (overPullbackToStar c.fst c.snd) (Over.homMk m)).mpr - simp [overPullbackToStar, Fan.overPullbackToStar, Fan.over] + simp [overPullbackToStar, PartialProduct.Fan.overPullbackToStar, PartialProduct.Fan.over] apply (Adjunction.homEquiv_apply_eq _ _ _).mpr rw [← h_right] simp [forgetAdjStar, comp_homEquiv, Comonad.adj] @@ -327,13 +328,13 @@ theorem lift_fst {Γ X : C} {P : UvPoly E B} {b : Γ ⟶ B} {e : pullback b P.p @[reassoc] theorem lift_snd {Γ X : C} {P : UvPoly E B} {b : Γ ⟶ B} {e : pullback b P.p ⟶ X} : - comparison (c := fan P X) (P.lift b e) ≫ (fan P X).snd = + PartialProduct.comparison (c := PartialProduct.fan P X) (P.lift b e) ≫ (fan P X).snd = (pullback.congrHom (partialProd.lift_fst b e) rfl).hom ≫ e := partialProd.lift_snd .. theorem hom_ext {Γ X : C} {P : UvPoly E B} {f g : Γ ⟶ P @ X} (h₁ : f ≫ P.fstProj X = g ≫ P.fstProj X) - (h₂ : comparison f ≫ (fan P X).snd = - (pullback.congrHom (by exact h₁) rfl).hom ≫ comparison g ≫ (fan P X).snd) : + (h₂ : PartialProduct.comparison f ≫ (fan P X).snd = + (pullback.congrHom (by exact h₁) rfl).hom ≫ PartialProduct.comparison g ≫ (fan P X).snd) : f = g := partialProd.hom_ext ⟨fan P X, isLimitFan P X⟩ h₁ h₂ /-- A morphism `f : Γ ⟶ P @ X` projects to a morphism `b : Γ ⟶ B` and a morphism @@ -359,76 +360,13 @@ def compDom {E B D A : C} (P : UvPoly E B) (Q : UvPoly D A) := Limits.pullback Q.p (fan P A).snd @[simps!] -def comp {E B D A : C} (P : UvPoly E B) (Q : UvPoly D A) : UvPoly (compDom P Q) (P @ A) := by - letI p := pullback.snd Q.p (fan P A).snd ≫ pullback.fst (fan P A).fst P.p - refine { p, exp.exists_rightAdjoint := ?_ } - let F1 := map (P.fstProj A) ⋙ Over.pullback P.p - let G1 := pushforward P.p ⋙ Over.pullback (P.fstProj A) - let adj1 : F1 ⊣ G1 := mapPullbackAdj (P.fstProj A) |>.comp (adj P.p) - let F2 := Over.pullback (pullback.fst (fan P A).fst P.p) - let G2 := map (pullback.snd (fan P A).fst P.p) - let F3 := map (fan P A).snd ⋙ Over.pullback Q.p - let G3 := pushforward Q.p ⋙ Over.pullback (fan P A).snd - let adj2 : F3 ⊣ G3 := mapPullbackAdj (fan P A).snd |>.comp (adj Q.p) - let G4 := map (pullback.fst Q.p (fan P A).snd) - let F5 := map p - let G5 := Over.pullback p - let adj3 : F5 ⊣ G5 := mapPullbackAdj p - suffices G5 ⊣ G4 ⋙ G3 ⋙ G2 ⋙ G1 from ⟨_, ⟨this⟩⟩ - refine { - unit := { - app Y := ?_ - naturality := sorry - } - counit := { - app X := ?_ - naturality := ?_ - } - left_triangle_components := sorry - right_triangle_components := sorry - } - · - change Y ⟶ (G5 ⋙ G4 ⋙ G3 ⋙ G2 ⋙ G1).obj Y - refine adj1.homEquiv _ _ ?_ - let f : F1.obj Y ⟶ (F2 ⋙ G2).obj Y := - Over.homMk (pullback.lift (pullback.fst ..) - (pullback.lift (pullback.fst .. ≫ Y.hom) (pullback.snd ..) - ?_) ?_) ?_ - refine f ≫ G2.map ?_ - refine adj2.homEquiv _ _ ?_ - refine ?_ ≫ G4.map (adj3.homEquiv (G5.obj Y) _ (Over.homMk (pullback.fst ..) ?_)) - refine Over.homMk (pullback.lift - (pullback.fst .. ≫ pullback.fst ..) - (pullback.lift (pullback.snd ..) - (pullback.fst .. ≫ pullback.snd ..) ?_) - ?_) ?_ - · simp [← pullback.condition, F2] - · simp only [assoc, pullback.condition, limit.lift_π_assoc, PullbackCone.mk_π_app, p] - · simp only [F3, F2, G4, G5, map_obj_hom, pullback_obj_hom, comp_obj] - rw [pullback.lift_snd_assoc, pullback.lift_fst] - · rw [pullback.condition]; rfl - · rw [← pullback.condition, assoc]; rfl - · rw [pullback.lift_fst] - · simp only [F2, G2, comp_obj, map_obj_hom, pullback_obj_hom] - rw [pullback.lift_snd_assoc, pullback.lift_snd]; rfl - dsimp - - done - -- simp - -- simp only [comp_obj, map_obj_hom, id_obj, - -- const_obj_obj, pullback_obj_hom, limit.lift_π_assoc, PullbackCone.mk_pt, cospan_right, - -- PullbackCone.mk_π_app, limit.lift_π, F3, F2, G4, G5] - - -- · simp [pullback.condition, F5, G5] - · - dsimp -- [G1,G2,G3,G4,G5] - have f X : G5.obj X ⟶ F1.obj X := - _ - refine adj1.counit - have := _ ≫ @(adj P.p).counit.app _ ≫ _; simp at this - refine ((mapPullbackAdj _).homEquiv _ _).symm ?_ - - done +def comp [HasPullbacks C] [HasTerminal C] + {E B D A : C} (P : UvPoly E B) (Q : UvPoly D A) : UvPoly (compDom P Q) (P @ A) where + p := pullback.snd Q.p (fan P A).snd ≫ pullback.fst (fan P A).fst P.p + exp := + haveI := ExponentiableMorphism.of_isPullback (.flip <| .of_hasPullback Q.p (fan P A).snd) + haveI := ExponentiableMorphism.of_isPullback (.of_hasPullback (fan P A).fst P.p) + inferInstance /-- The associated functor of the composition of two polynomials is isomorphic to the composition of the associated functors. -/ def compFunctorIso [HasPullbacks C] [HasTerminal C] @@ -445,7 +383,6 @@ instance monoidal [HasPullbacks C] [HasTerminal C] : MonoidalCategory (UvPoly.To leftUnitor := sorry rightUnitor := sorry -#print sorries UvPoly.comp UvPoly.PartialProduct.isLimitFan partialProd.lift_snd partialProd.hom_ext end UvPoly end CategoryTheory end