feat: bump to Lean v4.28.0-rc1 (#36)

Author: Vtec234

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

@@ -35,10 +35,6 @@ 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 :=

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

@@ -9,7 +9,7 @@ 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
+import Poly.ForMathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
 
 noncomputable section
 
@@ -19,7 +19,7 @@ namespace CategoryTheory
 
 open Category Limits Comonad MonoidalCategory CartesianMonoidalCategory
 
-attribute [local instance] CartesianMonoidalCategory.ofFiniteProducts
+attribute [local instance] CartesianMonoidalCategory.ofHasFiniteProducts
 
 variable {C : Type u₁} [Category.{v₁} C]
 
@@ -211,7 +211,7 @@ 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] CartesianMonoidalCategory.ofFiniteProducts
+attribute [local instance] CartesianMonoidalCategory.ofHasFiniteProducts
 
 lemma whiskerLeftProdMapId [HasFiniteLimits C] {X : C} {A A' : C} {g : A ⟶ A'} :
     X ◁ g = prod.map (𝟙 X) g := by
@@ -298,12 +298,6 @@ def starIsoToOverTerminal [HasTerminal C] [HasBinaryProducts C] :
 
 variable {C}
 
-/-- A natural isomorphism between the functors `star X` and `star Y ⋙ pullback f`
-for any morphism `f : X ⟶ Y`. -/
-def starPullbackIsoStar [HasBinaryProducts C] [HasPullbacks C] {X Y : C} (f : X ⟶ Y) :
-    star Y ⋙ pullback f ≅ star X :=
-  conjugateIsoEquiv ((mapPullbackAdj f).comp (forgetAdjStar Y)) (forgetAdjStar X) (mapForget f)
-
 /-- The functor `Over.pullback f : Over Y ⥤ Over X` is naturally isomorphic to
 `Over.star : Over Y ⥤ Over (Over.mk f)` post-composed with the
 iterated slice equivlanece `Over (Over.mk f) ⥤ Over X`. -/

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

@@ -28,7 +28,7 @@ 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] CartesianMonoidalCategory.ofFiniteProducts
+attribute [local instance] CartesianMonoidalCategory.ofHasFiniteProducts
 
 section
 
@@ -69,11 +69,11 @@ end
 
 variable [HasTerminal C] [HasPullbacks C]
 
-variable (I : C) [Exponentiable I]
+variable (I : C) [Closed I]
 
 /-- The first leg of a cospan constructing a pullback diagram in `C` used to define `sections` . -/
 def curryId : ⊤_ C ⟶ (I ⟹ I) :=
-  CartesianClosed.curry (fst I (⊤_ C))
+  MonoidalClosed.curry (fst I (⊤_ C))
 
 variable {I}
 
@@ -90,14 +90,14 @@ pullback diagram:
   ⊤_ C    ---->  I ⟹ I
 ```-/
 abbrev sectionsObj (X : Over I) : C :=
-  Limits.pullback (curryId I) ((exp I).map X.hom)
+  Limits.pullback (curryId I) ((ihom I).map X.hom)
 
 /-- The functoriality of `sectionsObj`. -/
 def sectionsMap {X X' : Over I} (u : X ⟶ X') :
     sectionsObj X ⟶ sectionsObj X' := by
   fapply pullback.map
   · exact 𝟙 _
-  · exact (exp I).map u.left
+  · exact (ihom I).map u.left
   · exact 𝟙 _
   · simp only [comp_id, id_comp]
   · simp only [comp_id, ← Functor.map_comp, w]
@@ -130,29 +130,30 @@ variable {I}
 in `C`. See `sectionsCurry`. -/
 def sectionsCurryAux {X : Over I} {A : C} (u : (star I).obj A ⟶ X) :
     A ⟶ (I ⟹ X.left) :=
-  CartesianClosed.curry (u.left)
+  MonoidalClosed.curry (u.left)
 
 /-- The currying operation `Hom ((star I).obj A) X → Hom A (I ⟹ X.left)`. -/
 def sectionsCurry {X : Over I} {A : C} (u : (star I).obj A ⟶ X) :
     A ⟶ (sections I).obj X := by
   apply pullback.lift (terminal.from A)
-    (CartesianClosed.curry ((prodIsoTensorObj _ _).inv ≫ u.left)) (uncurry_injective _)
-  rw [uncurry_natural_left]
-  simp [curryId, uncurry_natural_right, uncurry_curry]
+    (MonoidalClosed.curry ((prodIsoTensorObj _ _).inv ≫ u.left))
+    (MonoidalClosed.uncurry_injective _)
+  rw [MonoidalClosed.uncurry_natural_left]
+  simp [curryId, MonoidalClosed.uncurry_natural_right, MonoidalClosed.uncurry_curry]
 
 /-- The uncurrying operation `Hom A (section X) → Hom ((star I).obj A) X`. -/
 def sectionsUncurry {X : Over I} {A : C} (v : A ⟶ (sections I).obj X) :
     (star I).obj A ⟶ X := by
   let v₂ : A ⟶ (I ⟹ X.left) := v ≫ pullback.snd ..
-  have w : terminal.from A ≫ (curryId I) = v₂ ≫ (exp I).map X.hom := by
+  have w : terminal.from A ≫ (curryId I) = v₂ ≫ (ihom I).map X.hom := by
     rw [IsTerminal.hom_ext terminalIsTerminal (terminal.from A ) (v ≫ (pullback.fst ..))]
     simp [v₂, pullback.condition]
   dsimp [curryId] at w
   have w' := homEquiv_naturality_right_square (F := MonoidalCategory.tensorLeft I)
-    (adj := exp.adjunction I) _ _ _ _ w
-  simp [CartesianClosed.curry] at w'
-  refine Over.homMk ((prodIsoTensorObj I A).hom ≫ CartesianClosed.uncurry v₂) ?_
-  · dsimp [CartesianClosed.uncurry] at *
+    (adj := ihom.adjunction I) _ _ _ _ w
+  simp [MonoidalClosed.curry] at w'
+  refine Over.homMk ((prodIsoTensorObj I A).hom ≫ MonoidalClosed.uncurry v₂) ?_
+  · dsimp [MonoidalClosed.uncurry] at *
     rw [Category.assoc, ← w']
     simp [star_obj_hom]
 
@@ -188,13 +189,13 @@ def coreHomEquiv : CoreHomEquiv (star I) (sections I) where
     simp only [star_map]
     rw [← Over.homMk_comp]  -- note: in a newer version of mathlib this is `Over.homMk_eta`
     congr 1
-    simp [CartesianClosed.uncurry_natural_left]
+    simp [MonoidalClosed.uncurry_natural_left]
   homEquiv_naturality_right := by
     intro A X' X u g
     dsimp [sectionsCurry, sectionsUncurry, curryId]
     apply pullback.hom_ext (IsTerminal.hom_ext terminalIsTerminal _ _)
     simp [sectionsMap, curryId]
-    rw [← CartesianClosed.curry_natural_right, Category.assoc]
+    rw [← MonoidalClosed.curry_natural_right, Category.assoc]
 
 variable (I)
 

…heory/Limits/Shapes/Pullback/CommSq.lean …ts/Shapes/Pullback/IsPullback/Basic.leanPoly/ForMathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean renamed to Poly/ForMathlib/CategoryTheory/Limits/Shapes/Pullback/IsPullback/Basic.lean Poly/ForMathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean renamed to Poly/ForMathlib/CategoryTheory/Limits/Shapes/Pullback/IsPullback/Basic.lean

@@ -3,7 +3,7 @@ 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 Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
 import Poly.ForMathlib.CategoryTheory.CommSq
 
 namespace CategoryTheory.Functor

Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Basic.lean

@@ -67,7 +67,7 @@ open CategoryTheory Category MonoidalCategory CartesianMonoidalCategory Limits F
 
 variable {C : Type u} [Category.{v} C]
 
-attribute [local instance] CartesianMonoidalCategory.ofFiniteProducts
+attribute [local instance] CartesianMonoidalCategory.ofHasFiniteProducts
 
 /-- A morphism `f : I ⟶ J` is exponentiable if the pullback functor `Over J ⥤ Over I`
 has a right adjoint. -/
@@ -179,7 +179,7 @@ instance isMultiplicative : (ExponentiableMorphism (C:= C)).IsMultiplicative whe
 /-- A morphism with a pushforward is an exponentiable object in the slice category. -/
 def exponentiableOverMk [HasFiniteWidePullbacks C] {X I : C} (f : X ⟶ I)
     [ExponentiableMorphism f] :
-    Exponentiable (Over.mk f) where
+    Closed (Over.mk f) where
   rightAdj := pullback f ⋙ pushforward f
   adj := by
     apply ofNatIsoLeft _ _
@@ -192,7 +192,7 @@ morphism `X.hom`.
 Here the pushforward functor along a morphism `f : I ⟶ J` is defined using the section functor
 `Over (Over.mk f) ⥤ Over J`.
 -/
-def ofOverExponentiable [HasFiniteWidePullbacks C] {I : C} (X : Over I) [Exponentiable X] :
+def ofOverExponentiable [HasFiniteWidePullbacks C] {I : C} (X : Over I) [Closed X] :
     ExponentiableMorphism X.hom :=
   ⟨X.iteratedSliceEquiv.inverse ⋙ sections X, ⟨by
     refine ofNatIsoLeft (Adjunction.comp ?_ ?_) (starIteratedSliceForwardIsoPullback X.hom)
@@ -217,7 +217,7 @@ variable {C} [HasFiniteWidePullbacks C] [HasPushforwards C]
 /-- In a category where pushforwards exists along all morphisms, every slice category `Over I` is
 cartesian closed. -/
 instance cartesianClosedOver (I : C) :
-    CartesianClosed (Over I) where
+    MonoidalClosed (Over I) where
   closed X := @exponentiableOverMk _ _ _ _ _ _ X.hom (HasPushforwards.exponentiable X.hom)
 
 end HasPushforwards
@@ -226,13 +226,13 @@ namespace CartesianClosedOver
 
 open Over Reindex IsIso CartesianClosed HasPushforwards ExponentiableMorphism
 
-variable {C} [HasFiniteWidePullbacks C] {I J : C} [CartesianClosed (Over J)]
+variable {C} [HasFiniteWidePullbacks C] {I J : C} [MonoidalClosed (Over J)]
 
 instance (f : I ⟶ J) : ExponentiableMorphism f :=
   ExponentiableMorphism.ofOverExponentiable (Over.mk f)
 
 /-- A category with cartesian closed slices has pushforwards along all morphisms. -/
-instance hasPushforwards [Π (I : C), CartesianClosed (Over I)] : HasPushforwards C where
+instance hasPushforwards [Π (I : C), MonoidalClosed (Over I)] : HasPushforwards C where
   exponentiable f := ExponentiableMorphism.ofOverExponentiable (Over.mk f)
 
 end CartesianClosedOver
@@ -242,7 +242,7 @@ is exponentiable and all the slices are cartesian closed. -/
 class LocallyCartesianClosed [HasFiniteWidePullbacks C] extends
     HasPushforwards C where
   /-- every slice category `Over I` is cartesian closed. This is filled in by default. -/
-  cartesianClosedOver : Π (I : C), CartesianClosed (Over I) := HasPushforwards.cartesianClosedOver
+  cartesianClosedOver : Π (I : C), MonoidalClosed (Over I) := HasPushforwards.cartesianClosedOver
 
 namespace LocallyCartesianClosed
 
@@ -256,7 +256,7 @@ attribute [scoped instance] hasFiniteLimits_of_hasTerminal_and_pullbacks
 instance mkOfHasPushforwards [HasPushforwards C] : LocallyCartesianClosed C where
 
 /-- A category with cartesian closed slices is locally cartesian closed. -/
-instance mkOfCartesianClosedOver [Π (I : C), CartesianClosed (Over I)] :
+instance mkOfCartesianClosedOver [Π (I : C), MonoidalClosed (Over I)] :
   LocallyCartesianClosed C where
 
 variable [LocallyCartesianClosed C]
@@ -282,15 +282,16 @@ abbrev ev' {I : C} (X : Over I) (Y : Over X.left) : Reindex X (Pi X Y) ⟶ Y :=
   adj X.hom |>.counit.app Y
 
 /-- A locally cartesian closed category with a terminal object is cartesian closed. -/
-def cartesianClosed [HasTerminal C] :
-    CartesianClosed C := cartesianClosedOfEquiv <| equivOverTerminal C
+def monoidalClosed [HasTerminal C] :
+    MonoidalClosed C := cartesianClosedOfEquiv <| equivOverTerminal C
 
 /-- The slices of a locally cartesian closed category are locally cartesian closed. -/
 def overLocallyCartesianClosed (I : C) : LocallyCartesianClosed (Over I) := by
   apply (config := { allowSynthFailures:= true}) mkOfCartesianClosedOver
   intro X
   exact cartesianClosedOfEquiv (C := Over (X.left)) X.iteratedSliceEquiv.symm
 
+open CartesianClosed in
 /-- The exponential `X^^A` in the slice category `Over I` is isomorphic to the pushforward of the
 pullback of `X` along `A`. -/
 def expIso {I : C} (A X : Over I) :  Pi A (Reindex A X) ≅ A ⟹ X := Iso.refl _

Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/BeckChevalley.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sina Hazratpour, Emily Riehl
 -/
 import Poly.ForMathlib.CategoryTheory.LocallyCartesianClosed.Basic
-import Mathlib.CategoryTheory.Limits.Shapes.Pullback.CommSq
+import Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
 
 /-!
 # Beck-Chevalley natural transformations and natural isomorphisms

Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Presheaf.lean

@@ -22,10 +22,10 @@ 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] CartesianMonoidalCategory.ofFiniteProducts
+attribute [local instance] CartesianMonoidalCategory.ofHasFiniteProducts
 
-instance cartesianClosedOver {C : Type u} [Category.{max u v} C] (P : Psh C) :
-    CartesianClosed (Over P) :=
+instance monoidalClosedOver {C : Type u} [Category.{max u v} C] (P : Psh C) :
+    MonoidalClosed (Over P) :=
   cartesianClosedOfEquiv (overEquivPresheafCostructuredArrow P).symm
 
 instance locallyCartesianClosed : LocallyCartesianClosed (Psh C) := by

Poly/ForMathlib/CategoryTheory/NatTrans.lean

@@ -6,7 +6,7 @@ Authors: Sina Hazratpour
 
 import Mathlib.CategoryTheory.NatTrans
 import Mathlib.CategoryTheory.Functor.TwoSquare
-import Mathlib.CategoryTheory.Limits.Shapes.Pullback.CommSq
+import Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
 
 open CategoryTheory Limits IsPullback
 

Poly/ForMathlib/CategoryTheory/PartialProduct.lean

@@ -3,7 +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
 -/
-import Mathlib.CategoryTheory.Limits.Shapes.Pullback.CommSq
+import Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
 import Mathlib.CategoryTheory.Comma.Over.Pullback
 import Poly.ForMathlib.CategoryTheory.Comma.Over.Pullback
 import Mathlib.CategoryTheory.Monoidal.Closed.Cartesian
@@ -100,6 +100,8 @@ structure Fan.Hom (c c' : Fan s X) where
 
 attribute [reassoc (attr := simp)] Fan.Hom.w_left Fan.Hom.w_right
 
+-- TODO: this is taking ages to check since 4.28.0-rc1.
+set_option maxHeartbeats 0 in
 @[simps]
 instance : Category (Fan s X) where
   Hom := Fan.Hom

Poly/Type/Univariate.lean

@@ -189,7 +189,7 @@ def Obj.iget [DecidableEq P.B] {X} [Inhabited X] (x : P X) (i : P.Total) : X :=
 @[simp]
 theorem iget_map [DecidableEq P.B] [Inhabited X] [Inhabited Y] (x : P X)
     (f : X → Y) (i : P.Total) (h : i.1 = x.1) : (P.map f x).iget i = f (x.iget i) := by
-  simp only [Obj.iget, fst_map, *, dif_pos, eq_self_iff_true]
+  simp only [Obj.iget, fst_map, *, dif_pos]
   cases x
   rfl