diff --git a/Poly/ForMathlib/CategoryTheory/CommSq.lean b/Poly/ForMathlib/CategoryTheory/CommSq.lean new file mode 100644 index 0000000..358be06 --- /dev/null +++ b/Poly/ForMathlib/CategoryTheory/CommSq.lean @@ -0,0 +1,21 @@ +/- +Copyright (c) 2025 Wojciech Nawrocki. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Wojciech Nawrocki +-/ +import Mathlib.CategoryTheory.CommSq + +namespace CategoryTheory.Functor + +theorem reflect_commSq + {C D : Type*} [Category C] [Category D] + (F : C ⥤ D) [Functor.Faithful F] + {X Y Z W : C} {f : X ⟶ Y} {g : X ⟶ Z} {h : Y ⟶ W} {i : Z ⟶ W} : + CommSq (F.map f) (F.map g) (F.map h) (F.map i) → + CommSq f g h i := by + intro cs + constructor + apply Functor.map_injective F + simpa [← Functor.map_comp] using cs.w + +end CategoryTheory.Functor diff --git a/Poly/ForMathlib/CategoryTheory/Comma/Over/Basic.lean b/Poly/ForMathlib/CategoryTheory/Comma/Over/Basic.lean index 0abbddf..c7d37a7 100644 --- a/Poly/ForMathlib/CategoryTheory/Comma/Over/Basic.lean +++ b/Poly/ForMathlib/CategoryTheory/Comma/Over/Basic.lean @@ -35,6 +35,10 @@ lemma homMk_comp'_assoc {X Y Z W : T} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ W) lemma homMk_id {X B : T} (f : X ⟶ B) (h : 𝟙 X ≫ f = f) : homMk (𝟙 X) h = 𝟙 (mk f) := rfl +@[simp] +theorem mkIdTerminal_from_left {B : T} (U : Over B) : (mkIdTerminal.from U).left = U.hom := by + simp [mkIdTerminal, CostructuredArrow.mkIdTerminal, Limits.IsTerminal.from, Functor.preimage] + /-- `Over.Sigma Y U` is a shorthand for `(Over.map Y.hom).obj U`. This is a category-theoretic analogue of `Sigma` for types. -/ abbrev Sigma {X : T} (Y : Over X) (U : Over (Y.left)) : Over X := diff --git a/Poly/ForMathlib/CategoryTheory/Comma/Over/Pullback.lean b/Poly/ForMathlib/CategoryTheory/Comma/Over/Pullback.lean index c772233..d180a48 100644 --- a/Poly/ForMathlib/CategoryTheory/Comma/Over/Pullback.lean +++ b/Poly/ForMathlib/CategoryTheory/Comma/Over/Pullback.lean @@ -8,7 +8,8 @@ import Mathlib.CategoryTheory.Monoidal.Cartesian.Basic import Mathlib.CategoryTheory.Limits.Constructions.Over.Basic import Mathlib.CategoryTheory.Monad.Products import Poly.ForMathlib.CategoryTheory.Comma.Over.Basic - +import Poly.ForMathlib.CategoryTheory.NatTrans +import Poly.ForMathlib.CategoryTheory.Limits.Shapes.Pullback.CommSq noncomputable section @@ -24,6 +25,19 @@ variable {C : Type u₁} [Category.{v₁} C] namespace Over +theorem isCartesian_mapPullbackAdj_counit [HasPullbacks C] {X Y : C} (f : X ⟶ Y) : + NatTrans.IsCartesian (Over.mapPullbackAdj f).counit := by + intro A B U + apply IsPullback.of_right + (h₁₂ := Over.homMk (V := Over.mk f) (pullback.snd B.hom f) <| by simp) + (v₁₃ := Over.mkIdTerminal.from _) + (h₂₂ := Over.mkIdTerminal.from _) + case p => ext; simp + . apply (Over.forget Y).reflect_isPullback + convert (IsPullback.of_hasPullback A.hom f).flip using 1 <;> simp + . apply (Over.forget Y).reflect_isPullback + convert (IsPullback.of_hasPullback B.hom f).flip using 1 <;> simp + /-- The reindexing of `Z : Over X` along `Y : Over X`, defined by pulling back `Z` along `Y.hom : Y.left ⟶ X`. -/ abbrev Reindex [HasPullbacks C] {X : C} (Y : Over X) (Z : Over X) : Over Y.left := diff --git a/Poly/ForMathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean b/Poly/ForMathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean new file mode 100644 index 0000000..29faccd --- /dev/null +++ b/Poly/ForMathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean @@ -0,0 +1,30 @@ +/- +Copyright (c) 2025 Wojciech Nawrocki. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Wojciech Nawrocki +-/ +import Mathlib.CategoryTheory.Limits.Shapes.Pullback.CommSq +import Poly.ForMathlib.CategoryTheory.CommSq + +namespace CategoryTheory.Functor +open Limits + +theorem reflect_isPullback + {C D : Type*} [Category C] [Category D] (F : C ⥤ D) + {X Y Z W : C} (f : X ⟶ Y) (g : X ⟶ Z) (h : Y ⟶ W) (i : Z ⟶ W) + [rl : ReflectsLimit (cospan h i) F] [Functor.Faithful F] : + IsPullback (F.map f) (F.map g) (F.map h) (F.map i) → + IsPullback f g h i := by + intro pb + have sq := F.reflect_commSq pb.toCommSq + apply IsPullback.mk sq + apply rl.reflects + let i := cospanCompIso F h i + apply IsLimit.equivOfNatIsoOfIso i.symm pb.cone _ _ pb.isLimit + let j : + ((Cones.postcompose i.symm.hom).obj pb.cone).pt ≅ + (F.mapCone <| PullbackCone.mk f g sq.w).pt := + Iso.refl _ + apply WalkingCospan.ext j <;> simp +zetaDelta + +end CategoryTheory.Functor diff --git a/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/BeckChevalley.lean b/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/BeckChevalley.lean index 99fe861..f80e02d 100644 --- a/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/BeckChevalley.lean +++ b/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/BeckChevalley.lean @@ -80,19 +80,19 @@ def mapIsoSquare {X Y Z W : C} {h : X ⟶ Z} {f : X ⟶ Y} {g : Z ⟶ W} {k : Y Over.map h ⋙ Over.map g ≅ Over.map f ⋙ Over.map k := eqToIso (map_square_eq sq) -variable [HasBinaryProducts C] [HasPullbacks C] +variable [HasPullbacks C] variable {X Y Z W : C} (h : X ⟶ Z) (f : X ⟶ Y) (g : Z ⟶ W) (k : Y ⟶ W) -(sq : CommSq h f g k) + (sq : CommSq h f g k) /-- The Beck-Chevalley natural transformation `pullback f ⋙ map h ⟶ map k ⋙ pullback g` constructed as a mate of `mapIsoSquare`: ``` - Over X -- .map h -> Over Z - ↑ ↑ -.pullback f | ↘ | .pullback g - | | - Over Y -- .map k -> Over W + Over Y - pullback f → Over X + | | +map k | ↙ | map h + ↓ ↓ + Over W - pullback g → Over Z ``` -/ --pullbackBeckChevalleySquare @@ -100,21 +100,28 @@ def pullbackMapTwoSquare : TwoSquare (pullback f) (map k) (map h) (pullback g) : mateEquiv (mapPullbackAdj f) (mapPullbackAdj g) (mapIsoSquare sq).hom /-- -The natural transformation `pullback f ⋙ forget X ⟶ forget Y ⋙ 𝟭 C` as the mate the isomorphism -`mapForget f`: +The natural transformation `pullback f ⋙ forget X ⟶ forget Y ⋙ 𝟭 C` +as the mate of the isomorphism `mapForget f`: ``` - Over X --.forget X -> C - ↑ | -.pullback f | ↘ | 𝟭 - | | - Over Y --.forget Y -> C + Over Y - pullback f → Over X + | | +forget Y | ↙ | forget X + ↓ ↓ + C ======== 𝟭 ======== C ``` -/ ---pullbackForgetBeckChevalleySquare -def pullbackForgetTwoSquare : TwoSquare (pullback f) (forget Y) (forget X) (𝟭 C) := by - let iso := (mapForget f).inv - rw [← Functor.comp_id (forget X)] at iso - exact (mateEquiv (mapPullbackAdj f) (Adjunction.id)) iso +def pullbackForgetTwoSquare : TwoSquare (pullback f) (forget Y) (forget X) (𝟭 C) := + mateEquiv (mapPullbackAdj f) Adjunction.id (mapForget f).inv + +theorem isCartesian_pullbackForgetTwoSquare {X Y : C} (f : X ⟶ Y) : + NatTrans.IsCartesian (pullbackForgetTwoSquare f) := by + unfold pullbackForgetTwoSquare + simp only [mateEquiv_apply] + repeat apply IsCartesian.comp; apply isCartesian_of_isIso + apply IsCartesian.comp + . apply IsCartesian.whiskerRight + apply isCartesian_mapPullbackAdj_counit + . apply isCartesian_of_isIso /-- The natural transformation `pullback f ⋙ forget X ⟶ forget Y`, a variant of `pullbackForgetTwoSquare`. -/ @@ -130,7 +137,7 @@ def pullbackMapTriangle (h' : Y ⟶ Z) (w : f ≫ h' = h) : let iso := (mapComp f h').hom rw [w] at iso rw [← Functor.comp_id (map h)] at iso - exact (mateEquiv (mapPullbackAdj f) (Adjunction.id)) iso + exact (mateEquiv (mapPullbackAdj f) Adjunction.id) iso /-- The isomorphism between the pullbacks along a commutative square. This is constructed as the conjugate of the `mapIsoSquare`. @@ -151,11 +158,11 @@ def pullbackIsoSquare : pullback k ⋙ pullback f ≅ pullback g ⋙ pullback h `pushforward g ⋙ pullback k ⟶ pullback h ⋙ pushforward f` constructed as a mate of `pullbackMapTwoSquare`. ``` - Over X ←-.pullback h-- Over Z - | | -.pushforward f | ↖ | .pushforward g - ↓ ↓ - Over Y ←-.pullback k-- Over W + Over Z - pushforward g → Over W + | | +pullback h | ↙ | pullback k + ↓ ↓ + Over X - pushforward f → Over Y ``` -/ --pushforwardBeckChevalleySquare @@ -169,12 +176,11 @@ def pushforwardPullbackTwoSquare A variant of `pushforwardTwoSquare` involving `star` instead of `pullback`. -/ --pushforwardStarBeckChevalleySquare -def starPushforwardTriangle - [ExponentiableMorphism f] : +def starPushforwardTriangle [HasBinaryProducts C] [ExponentiableMorphism f] : star Y ⟶ star X ⋙ pushforward f := by let iso := (starPullbackIsoStar f).hom rw [← Functor.id_comp (star X)] at iso - exact (mateEquiv (Adjunction.id) (adj f)) iso + exact (mateEquiv Adjunction.id (adj f)) iso /-- The conjugate isomorphism between the pushforwards along a commutative square. ``` diff --git a/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Distributivity.lean b/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Distributivity.lean index eca421e..3078438 100644 --- a/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Distributivity.lean +++ b/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Distributivity.lean @@ -92,8 +92,8 @@ def cellLeftTriangle : e f u ≫ u = w f u := by def cellLeft : pullback (e f u) ⋙ map (w f u) ⟶ map u := pullbackMapTriangle _ _ _ (cellLeftTriangle f u) -lemma cellLeftCartesian : cartesian (cellLeft f u) := by - unfold cartesian +lemma isCartesian_cellLeft : IsCartesian (cellLeft f u) := by + unfold IsCartesian simp only [id_obj, mk_left, comp_obj, pullback_obj_left, Functor.comp_map] unfold cellLeft intros i j f' @@ -107,8 +107,8 @@ def cellRightCommSq : CommSq (g f u) (w f u) (v f u) f := def cellRight' : pushforward (g f u) ⋙ map (v f u) ≅ map (w f u) ⋙ pushforward f := sorry -lemma cellRightCartesian : cartesian (cellRight' f u).hom := - cartesian_of_isIso ((cellRight' f u).hom) +lemma isCartesian_cellRight' : IsCartesian (cellRight' f u).hom := + isCartesian_of_isIso ((cellRight' f u).hom) def pasteCell1 : pullback (e f u) ⋙ pushforward (g f u) ⋙ map (v f u) ⟶ pullback (e f u) ⋙ map (w f u) ⋙ pushforward f := by @@ -122,19 +122,19 @@ def pasteCell2 : (pullback (e f u) ⋙ map (w f u)) ⋙ pushforward f def pasteCell := pasteCell1 f u ≫ pasteCell2 f u -def paste : cartesian (pasteCell f u) := by - apply cartesian.comp +def paste : IsCartesian (pasteCell f u) := by + apply IsCartesian.comp · unfold pasteCell1 - apply cartesian.whiskerLeft (cellRightCartesian f u) + apply (isCartesian_cellRight' f u).whiskerLeft · unfold pasteCell2 - apply cartesian.whiskerRight (cellLeftCartesian f u) + apply (isCartesian_cellLeft f u).whiskerRight -- use `pushforwardPullbackTwoSquare` to construct this iso. def pentagonIso : map u ⋙ pushforward f ≅ pullback (e f u) ⋙ pushforward (g f u) ⋙ map (v f u) := by - have := cartesian_of_isPullback_to_terminal (pasteCell f u) + have := isCartesian_of_isPullback_to_terminal (pasteCell f u) letI : IsIso ((pasteCell f u).app (⊤_ Over ((𝟭 (Over B)).obj (Over.mk u)).left)) := sorry - have := isIso_of_cartesian (pasteCell f u) (paste f u) + have := isIso_of_isCartesian (pasteCell f u) (paste f u) exact (asIso (pasteCell f u)).symm end CategoryTheory diff --git a/Poly/ForMathlib/CategoryTheory/NatTrans.lean b/Poly/ForMathlib/CategoryTheory/NatTrans.lean index cd1f798..6fd36bb 100644 --- a/Poly/ForMathlib/CategoryTheory/NatTrans.lean +++ b/Poly/ForMathlib/CategoryTheory/NatTrans.lean @@ -5,6 +5,7 @@ Authors: Sina Hazratpour -/ import Mathlib.CategoryTheory.NatTrans +import Mathlib.CategoryTheory.Functor.TwoSquare import Mathlib.CategoryTheory.Limits.Shapes.Pullback.CommSq open CategoryTheory Limits IsPullback @@ -20,75 +21,93 @@ namespace NatTrans open Functor -/-- A natural transformation is cartesian if every commutative square of the following form is -a pullback. -``` -F(X) → F(Y) - ↓ ↓ -G(X) → G(Y) -``` --/ -def cartesian {F G : J ⥤ C} (α : F ⟶ G) : Prop := +/-- A natural transformation is *cartesian* +if all its naturality squares are pullbacks. -/ +def IsCartesian {F G : J ⥤ C} (α : F ⟶ G) : Prop := ∀ ⦃i j : J⦄ (f : i ⟶ j), IsPullback (F.map f) (α.app i) (α.app j) (G.map f) -theorem cartesian_of_isIso {F G : J ⥤ C} (α : F ⟶ G) [IsIso α] : cartesian α := +theorem isCartesian_of_isIso {F G : J ⥤ C} (α : F ⟶ G) [IsIso α] : IsCartesian α := fun _ _ f => IsPullback.of_vert_isIso ⟨NatTrans.naturality _ f⟩ -theorem isIso_of_cartesian [HasTerminal J] {F G : J ⥤ C} (α : F ⟶ G) (hα : cartesian α) +theorem isIso_of_isCartesian [HasTerminal J] {F G : J ⥤ C} (α : F ⟶ G) (hα : IsCartesian α) [IsIso (α.app (⊤_ J))] : IsIso α := by refine @NatIso.isIso_of_isIso_app _ _ _ _ _ _ α (fun j ↦ isIso_snd_of_isIso <| hα <| terminal.from j) -theorem cartesian.comp {F G H : J ⥤ C} {α : F ⟶ G} {β : G ⟶ H} (hα : cartesian α) - (hβ : cartesian β) : cartesian (α ≫ β) := - fun _ _ f => (hα f).paste_vert (hβ f) - -theorem cartesian.whiskerRight {F G : J ⥤ C} {α : F ⟶ G} (hα : cartesian α) - (H : C ⥤ D) [∀ (i j : J) (f : j ⟶ i), PreservesLimit (cospan (α.app i) (G.map f)) H] : - cartesian (whiskerRight α H) := - fun _ _ f => (hα f).map H - -theorem cartesian.whiskerLeft {K : Type*} [Category K] {F G : J ⥤ C} {α : F ⟶ G} - (hα : cartesian α) (H : K ⥤ J) : cartesian (whiskerLeft H α) := - fun _ _ f => hα (H.map f) - -theorem cartesian.comp_horizz {M N K : Type*} - [Category M] [Category N] [Category K] {F G : J ⥤ C} {M N : C ⥤ K} {α : F ⟶ G} {β : M ⟶ N} - (hα : cartesian α) (hβ : cartesian β) - [∀ (i j : J) (f : j ⟶ i), PreservesLimit (cospan (α.app i) (G.map f)) M] : - cartesian (NatTrans.hcomp α β) := by { - have ha := cartesian.whiskerRight hα M - have hb := cartesian.whiskerLeft hβ G - have hc := cartesian.comp ha hb - unfold cartesian - intros i j f - specialize hc f - simp only [Functor.comp_obj, Functor.comp_map, comp_app, - whiskerRight_app, whiskerLeft_app, - naturality] at hc - exact hc - } - -theorem cartesian_of_discrete {ι : Type*} {F G : Discrete ι ⥤ C} - (α : F ⟶ G) : cartesian α := by +theorem isCartesian_of_discrete {ι : Type*} {F G : Discrete ι ⥤ C} + (α : F ⟶ G) : IsCartesian α := by rintro ⟨i⟩ ⟨j⟩ ⟨⟨rfl : i = j⟩⟩ simp only [Discrete.functor_map_id] exact IsPullback.of_horiz_isIso ⟨by rw [Category.id_comp, Category.comp_id]⟩ -theorem cartesian_of_isPullback_to_terminal [HasTerminal J] {F G : J ⥤ C} (α : F ⟶ G) +theorem isCartesian_of_isPullback_to_terminal [HasTerminal J] {F G : J ⥤ C} (α : F ⟶ G) (pb : ∀ j, IsPullback (F.map (terminal.from j)) (α.app j) (α.app (⊤_ J)) (G.map (terminal.from j))) : - cartesian α := by + IsCartesian α := by intro i j f apply IsPullback.of_right (h₁₂ := F.map (terminal.from j)) (h₂₂ := G.map (terminal.from j)) simpa [← F.map_comp, ← G.map_comp] using (pb i) exact α.naturality f exact pb j +namespace IsCartesian -end NatTrans +theorem comp {F G H : J ⥤ C} {α : F ⟶ G} {β : G ⟶ H} (hα : IsCartesian α) (hβ : IsCartesian β) : + IsCartesian (α ≫ β) := + fun _ _ f => (hα f).paste_vert (hβ f) + +theorem whiskerRight {F G : J ⥤ C} {α : F ⟶ G} (hα : IsCartesian α) (H : C ⥤ D) + [∀ (i j : J) (f : j ⟶ i), PreservesLimit (cospan (α.app i) (G.map f)) H] : + IsCartesian (whiskerRight α H) := + fun _ _ f => (hα f).map H -open NatTrans +theorem whiskerLeft {K : Type*} [Category K] {F G : J ⥤ C} + {α : F ⟶ G} (hα : IsCartesian α) (H : K ⥤ J) : IsCartesian (whiskerLeft H α) := + fun _ _ f => hα (H.map f) -theorem mapPair_cartesian {F F' : Discrete WalkingPair ⥤ C} (α : F ⟶ F') : cartesian α := - cartesian_of_discrete α +theorem hcomp {K : Type*} [Category K] {F G : J ⥤ C} {M N : C ⥤ K} {α : F ⟶ G} {β : M ⟶ N} + (hα : IsCartesian α) (hβ : IsCartesian β) + [∀ (i j : J) (f : j ⟶ i), PreservesLimit (cospan (α.app i) (G.map f)) M] : + IsCartesian (NatTrans.hcomp α β) := by + have ha := hα.whiskerRight M + have hb := hβ.whiskerLeft G + have hc := ha.comp hb + unfold IsCartesian + intros i j f + specialize hc f + simp only [Functor.comp_obj, Functor.comp_map, comp_app, + whiskerRight_app, whiskerLeft_app, + naturality] at hc + exact hc + +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 vComp {w : TwoSquare T L R B} {w' : TwoSquare B L' R'' B''} + [∀ (i j : C₁) (f : j ⟶ i), PreservesLimit (cospan (w.app i) ((L ⋙ B).map f)) R''] : + IsCartesian w → IsCartesian w' → IsCartesian (w ≫ᵥ w') := + fun cw cw' => + (isCartesian_of_isIso _).comp <| + (cw.whiskerRight _).comp <| + (isCartesian_of_isIso _).comp <| + (cw'.whiskerLeft _).comp <| + (isCartesian_of_isIso _) + +theorem hComp {w : TwoSquare T L R B} {w' : TwoSquare T' R R' B'} + [∀ (i j : C₁) (f : j ⟶ i), PreservesLimit (cospan (w.app i) ((L ⋙ B).map f)) B'] : + IsCartesian w → IsCartesian w' → IsCartesian (w ≫ₕ w') := + fun cw cw' => + (isCartesian_of_isIso _).comp <| + (cw'.whiskerLeft _).comp <| + (isCartesian_of_isIso _).comp <| + (cw.whiskerRight _).comp <| + (isCartesian_of_isIso _) + +end IsCartesian +end NatTrans diff --git a/Poly/UvPoly/Basic.lean b/Poly/UvPoly/Basic.lean index a684339..363f319 100644 --- a/Poly/UvPoly/Basic.lean +++ b/Poly/UvPoly/Basic.lean @@ -7,6 +7,7 @@ Authors: Sina Hazratpour, Wojciech Nawrocki import Poly.ForMathlib.CategoryTheory.LocallyCartesianClosed.BeckChevalley -- LCCC.BeckChevalley import Mathlib.CategoryTheory.Functor.TwoSquare import Poly.ForMathlib.CategoryTheory.PartialProduct +import Poly.ForMathlib.CategoryTheory.NatTrans /-! @@ -61,18 +62,18 @@ variable {E B : C} /-- The constant polynomial in many variables: for this we need the initial object -/ def const [HasInitial C] (S : C) : UvPoly (⊥_ C) S := ⟨initial.to S, sorry⟩ -def smul [HasBinaryProducts C] (S : C) (P : UvPoly E B) : UvPoly (S ⨯ E) (S ⨯ B) := +def smul (S : C) (P : UvPoly E B) : UvPoly (S ⨯ E) (S ⨯ B) := ⟨prod.map (𝟙 S) P.p, sorry⟩ /-- The product of two polynomials in a single variable. -/ -def prod {E' B'} (P : UvPoly E B) (Q : UvPoly E' B') [HasBinaryCoproducts C]: +def prod {E' B'} (P : UvPoly E B) (Q : UvPoly E' B') [HasBinaryCoproducts C] : UvPoly ((E ⨯ B') ⨿ (B ⨯ E')) (B ⨯ B') where p := coprod.desc (prod.map P.p (𝟙 B')) (prod.map (𝟙 B) Q.p) exp := sorry -- perhaps we need extra assumptions on `C` to prove this, e.g. `C` is lextensive? /-- 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 [HasBinaryProducts C] (P : UvPoly E B) : C ⥤ C := +def functor (P : UvPoly E B) : C ⥤ C := star E ⋙ pushforward P.p ⋙ forget B /-- The evaluation function of a polynomial `P` at an object `X`. -/ @@ -81,6 +82,10 @@ def apply (P : UvPoly E B) : C → C := (P.functor).obj @[inherit_doc] infix:90 " @ " => UvPoly.apply +instance (P : UvPoly E B) : Limits.PreservesLimitsOfShape WalkingCospan P.functor := by + unfold functor + infer_instance + variable (B) /-- The identity polynomial functor in single variable. -/ @@ -155,17 +160,24 @@ C --- > C/E ----> C/B ----> C P.p ``` -/ -def cartesianNaturalTrans {D F : C}[HasBinaryProducts C] (P : UvPoly E B) (Q : UvPoly F D) - (δ : B ⟶ D) (φ : E ⟶ F) (pb : IsPullback P.p φ δ Q.p) : - P.functor ⟶ Q.functor := by - have sq : CommSq φ P.p Q.p δ := pb.toCommSq.flip +def cartesianNatTrans {D F : C} (P : UvPoly E B) (Q : UvPoly F D) + (δ : B ⟶ D) (φ : E ⟶ F) (pb : IsPullback P.p φ δ Q.p) : P.functor ⟶ Q.functor := let cellLeft : TwoSquare (𝟭 C) (Over.star F) (Over.star E) (pullback φ) := (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) := pullbackForgetTwoSquare δ - simpa using cellLeft ≫ᵥ cellMid ≫ᵥ cellRight + let := cellLeft ≫ᵥ cellMid ≫ᵥ cellRight + this + +open NatTrans in +theorem isCartesian_cartesianNatTrans {D F : C} (P : UvPoly E B) (Q : UvPoly F D) + (δ : B ⟶ D) (φ : E ⟶ F) (pb : IsPullback P.p φ δ Q.p) : + NatTrans.IsCartesian (cartesianNatTrans P Q δ φ pb) := + (isCartesian_of_isIso _).vComp <| + (isCartesian_of_isIso _).vComp <| + isCartesian_pullbackForgetTwoSquare _ /-- 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