feat: bump to v4.22.0-rc2

Poly/ForMathlib/CategoryTheory/Comma/Over/Pullback.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sina Hazratpour
 -/
 import Mathlib.CategoryTheory.Comma.Over.Pullback
-import Mathlib.CategoryTheory.ChosenFiniteProducts
+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
@@ -16,7 +16,9 @@ universe v₁ v₂ u₁ u₂
 
 namespace CategoryTheory
 
-open Category Limits Comonad MonoidalCategory
+open Category Limits Comonad MonoidalCategory CartesianMonoidalCategory
+
+attribute [local instance] CartesianMonoidalCategory.ofFiniteProducts
 
 variable {C : Type u₁} [Category.{v₁} C]
 
@@ -87,7 +89,7 @@ end Reindex
 
 section BinaryProduct
 
-open ChosenFiniteProducts Sigma Reindex
+open Sigma Reindex
 
 variable [HasFiniteWidePullbacks C] {X : C}
 
@@ -106,8 +108,6 @@ def isBinaryProductSigmaReindex (Y Z : Over X) :
     · exact congr_arg CommaMorphism.left (h ⟨ .right⟩)
     · exact congr_arg CommaMorphism.left (h ⟨ .left ⟩)
 
-attribute [local instance] ChosenFiniteProducts.ofFiniteProducts
-
 /-- The object `(Sigma Y) (Reindex Y Z)` is isomorphic to the binary product `Y × Z`
 in `Over X`. -/
 @[simps!]
@@ -122,12 +122,12 @@ def sigmaReindexIsoProdMk {Y : C} (f : Y ⟶ X) (Z : Over X) :
   sigmaReindexIsoProd (Over.mk f) _
 
 lemma sigmaReindexIsoProd_hom_comp_fst {Y Z : Over X} :
-    (sigmaReindexIsoProd Y Z).hom ≫ (fst Y Z) = (π_ Y Z) :=
+    (sigmaReindexIsoProd Y Z).hom ≫ fst Y Z = (π_ Y Z) :=
   IsLimit.conePointUniqueUpToIso_hom_comp
     (isBinaryProductSigmaReindex Y Z) (Limits.prodIsProd Y Z) ⟨.left⟩
 
 lemma sigmaReindexIsoProd_hom_comp_snd {Y Z : Over X} :
-    (sigmaReindexIsoProd Y Z).hom ≫ (snd Y Z) = (μ_ Y Z) :=
+    (sigmaReindexIsoProd Y Z).hom ≫ snd Y Z = (μ_ Y Z) :=
   IsLimit.conePointUniqueUpToIso_hom_comp
     (isBinaryProductSigmaReindex Y Z) (Limits.prodIsProd Y Z) ⟨.right⟩
 
@@ -137,10 +137,7 @@ end Over
 
 section TensorLeft
 
-open MonoidalCategory Over Functor ChosenFiniteProducts
-
-attribute [local instance] ChosenFiniteProducts.ofFiniteProducts
-attribute [local instance] monoidalOfChosenFiniteProducts
+open Over Functor
 
 variable [HasFiniteWidePullbacks C] {X : C}
 
@@ -150,16 +147,16 @@ def Over.sigmaReindexNatIsoTensorLeft (Y : Over X) :
     (pullback Y.hom) ⋙ (map Y.hom) ≅ tensorLeft Y := by
   fapply NatIso.ofComponents
   · intro Z
-    simp only [const_obj_obj, Functor.id_obj, comp_obj, tensorLeft_obj, tensorObj, Over.pullback]
+    simp only [const_obj_obj, Functor.id_obj, comp_obj, Over.pullback]
     exact sigmaReindexIsoProd Y Z
   · intro Z Z' f
-    simp
+    dsimp
     ext1 <;> simp_rw [assoc]
-    · simp_rw [whiskerLeft_fst]
+    · rw [whiskerLeft_fst]
       iterate rw [sigmaReindexIsoProd_hom_comp_fst]
       ext
       simp
-    · simp_rw [whiskerLeft_snd]
+    · rw [whiskerLeft_snd]
       iterate rw [sigmaReindexIsoProd_hom_comp_snd, ← assoc, sigmaReindexIsoProd_hom_comp_snd]
       ext
       simp [Reindex.sndProj]
@@ -187,7 +184,7 @@ def equivOverTerminal [HasTerminal C] : Over (⊤_ C) ≌ C :=
 
 namespace Over
 
-open MonoidalCategory
+open CartesianMonoidalCategory
 
 variable {C}
 
@@ -201,15 +198,14 @@ lemma star_map [HasBinaryProducts C] {X : C} {Y Z : C} (f : Y ⟶ Z) :
 instance [HasBinaryProducts C]  (X : C) : (forget X).IsLeftAdjoint  :=
   ⟨_, ⟨forgetAdjStar X⟩⟩
 
-attribute [local instance] ChosenFiniteProducts.ofFiniteProducts
-attribute [local instance] monoidalOfChosenFiniteProducts
+attribute [local instance] CartesianMonoidalCategory.ofFiniteProducts
 
 lemma whiskerLeftProdMapId [HasFiniteLimits C] {X : C} {A A' : C} {g : A ⟶ A'} :
     X ◁ g = prod.map (𝟙 X) g := by
   ext
-  · simp only [ChosenFiniteProducts.whiskerLeft_fst]
+  · simp only [whiskerLeft_fst]
     exact (Category.comp_id _).symm.trans (prod.map_fst (𝟙 X) g).symm
-  · simp only [ChosenFiniteProducts.whiskerLeft_snd]
+  · simp only [whiskerLeft_snd]
     exact (prod.map_snd (𝟙 X) g).symm
 
 def starForgetIsoTensorLeft [HasFiniteLimits C] (X : C) :

Poly/ForMathlib/CategoryTheory/Comma/Over/Sections.lean

@@ -21,49 +21,48 @@ universe v₁ v₂ u₁ u₂
 
 namespace CategoryTheory
 
-open Category Limits MonoidalCategory CartesianClosed Adjunction Over
+open Category Limits MonoidalCategory CartesianMonoidalCategory CartesianClosed Adjunction Over
 
 variable {C : Type u₁} [Category.{v₁} C]
 
 attribute [local instance] hasBinaryProducts_of_hasTerminal_and_pullbacks
 attribute [local instance] hasFiniteProducts_of_has_binary_and_terminal
-attribute [local instance] ChosenFiniteProducts.ofFiniteProducts
-attribute [local instance] monoidalOfChosenFiniteProducts
+attribute [local instance] CartesianMonoidalCategory.ofFiniteProducts
 
 section
 
 variable [HasFiniteProducts C]
 
 /-- The isomorphism between `X ⨯ Y` and `X ⊗ Y` for objects `X` and `Y` in `C`.
 This is tautological by the definition of the cartesian monoidal structure on `C`.
-This isomorphism provides an interface between `prod.fst` and `ChosenFiniteProducts.fst`
+This isomorphism provides an interface between `prod.fst` and `CartesianMonoidalCategory.fst`
 as well as between `prod.map` and `tensorHom`. -/
 def prodIsoTensorObj (X Y : C) : X ⨯ Y ≅ X ⊗ Y := Iso.refl _
 
 @[reassoc (attr := simp)]
 theorem prodIsoTensorObj_inv_fst {X Y : C} :
-    (prodIsoTensorObj X Y).inv ≫ prod.fst = ChosenFiniteProducts.fst X Y :=
+    (prodIsoTensorObj X Y).inv ≫ prod.fst = fst X Y :=
   Category.id_comp _
 
 @[reassoc (attr := simp)]
 theorem prodIsoTensorObj_inv_snd {X Y : C} :
-    (prodIsoTensorObj X Y).inv ≫ prod.snd = ChosenFiniteProducts.snd X Y :=
+    (prodIsoTensorObj X Y).inv ≫ prod.snd = snd X Y :=
   Category.id_comp _
 
 @[reassoc (attr := simp)]
 theorem prodIsoTensorObj_hom_fst {X Y : C} :
-    (prodIsoTensorObj X Y).hom ≫ ChosenFiniteProducts.fst X Y = prod.fst :=
+    (prodIsoTensorObj X Y).hom ≫ fst X Y = prod.fst :=
   Category.id_comp _
 
 @[reassoc (attr := simp)]
 theorem prodIsoTensorObj_hom_snd {X Y : C} :
-    (prodIsoTensorObj X Y).hom ≫ ChosenFiniteProducts.snd X Y = prod.snd :=
+    (prodIsoTensorObj X Y).hom ≫ snd X Y = prod.snd :=
   Category.id_comp _
 
 @[reassoc (attr := simp)]
 theorem prodMap_comp_prodIsoTensorObj_hom {X Y Z W : C} (f : X ⟶ Y) (g : Z ⟶ W) :
-    prod.map f g ≫ (prodIsoTensorObj _ _).hom = (prodIsoTensorObj _ _).hom ≫ (f ⊗ g) := by
-  apply ChosenFiniteProducts.hom_ext <;> simp
+    prod.map f g ≫ (prodIsoTensorObj _ _).hom = (prodIsoTensorObj _ _).hom ≫ (f ⊗ₘ g) := by
+  apply hom_ext <;> simp
 
 end
 
@@ -73,7 +72,7 @@ variable (I : C) [Exponentiable I]
 
 /-- The first leg of a cospan constructing a pullback diagram in `C` used to define `sections` . -/
 def curryId : ⊤_ C ⟶ (I ⟹ I) :=
-  CartesianClosed.curry (ChosenFiniteProducts.fst I (⊤_ C))
+  CartesianClosed.curry (fst I (⊤_ C))
 
 variable {I}
 

Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Basic.lean

@@ -62,11 +62,12 @@ universe v u
 
 namespace CategoryTheory
 
-open CategoryTheory Category MonoidalCategory Limits Functor Adjunction Over
+open CategoryTheory Category MonoidalCategory CartesianMonoidalCategory Limits Functor Adjunction
+  Over
 
 variable {C : Type u} [Category.{v} C]
 
-attribute [local instance] ChosenFiniteProducts.ofFiniteProducts
+attribute [local instance] CartesianMonoidalCategory.ofFiniteProducts
 
 /-- A morphism `f : I ⟶ J` is exponentiable if the pullback functor `Over J ⥤ Over I`
 has a right adjoint. -/
@@ -223,7 +224,7 @@ end HasPushforwards
 
 namespace CartesianClosedOver
 
-open Over Reindex IsIso ChosenFiniteProducts CartesianClosed HasPushforwards ExponentiableMorphism
+open Over Reindex IsIso CartesianClosed HasPushforwards ExponentiableMorphism
 
 variable {C} [HasFiniteWidePullbacks C] {I J : C} [CartesianClosed (Over J)]
 

Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Distributivity.lean

@@ -129,8 +129,6 @@ def paste : cartesian (pasteCell f u) := by
   · unfold pasteCell2
     apply cartesian.whiskerRight (cellLeftCartesian f u)
 
-#check pushforwardPullbackTwoSquare
-
 -- 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

Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Presheaf.lean

@@ -22,7 +22,7 @@ abbrev Psh (C : Type u) [Category.{v} C] : Type (max u (v + 1)) := Cᵒᵖ ⥤ T
 
 variable {C : Type*} [SmallCategory C] [HasTerminal C]
 
-attribute [local instance] ChosenFiniteProducts.ofFiniteProducts
+attribute [local instance] CartesianMonoidalCategory.ofFiniteProducts
 
 instance cartesianClosedOver {C : Type u} [Category.{max u v} C] (P : Psh C) :
     CartesianClosed (Over P) :=

Poly/ForMathlib/CategoryTheory/NatTrans.lean

@@ -18,6 +18,8 @@ variable {K : Type*} [Category K] {D : Type*} [Category D]
 
 namespace NatTrans
 
+open Functor
+
 /-- A natural transformation is cartesian if every commutative square of the following form is
 a pullback.
 ```

Poly/UvPoly/Basic.lean

@@ -223,10 +223,10 @@ instance : Category (UvPoly.Total C) where
   id P := UvPoly.Hom.id P.poly
   comp := UvPoly.Hom.comp
   id_comp := by
-    simp [UvPoly.Hom.id, UvPoly.Hom.comp]
+    simp [UvPoly.Hom.comp]
     sorry
   comp_id := by
-    simp [UvPoly.Hom.id, UvPoly.Hom.comp]
+    simp [UvPoly.Hom.comp]
     sorry
   assoc := by
     simp [UvPoly.Hom.comp]

Poly/UvPoly/UPFan.lean

@@ -23,8 +23,7 @@ def equiv (P : UvPoly E B) (Γ : C) (X : C) :
     dsimp
     symm
     fapply partialProd.hom_ext ⟨fan P X, isLimitFan P X⟩
-    · simp [partialProd.lift]
-      rfl
+    · simp; rfl
     · sorry
   right_inv := by
     intro ⟨b, e⟩