feat: a pullback of schemes is canonically over the second component (#31475)

From Toric

Author: YaelDillies

Mathlib/AlgebraicGeometry/Pullbacks.lean

@@ -33,7 +33,7 @@ universe u v w
 
 noncomputable section
 
-open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
+open CategoryTheory Functor CartesianMonoidalCategory Limits AlgebraicGeometry
 
 namespace AlgebraicGeometry.Scheme
 
@@ -635,6 +635,14 @@ instance Scheme.pullback_map_isOpenImmersion {X Y S X' Y' S' : Scheme}
   rw [pullback_map_eq_pullbackFstFstIso_inv]
   infer_instance
 
+section CartesianMonoidalCategory
+variable {S : Scheme}
+
+instance : CartesianMonoidalCategory (Over S) := Over.cartesianMonoidalCategory _
+instance : BraidedCategory (Over S) := .ofCartesianMonoidalCategory
+
+end CartesianMonoidalCategory
+
 section Spec
 
 variable (R S T : Type u) [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T]
@@ -662,6 +670,11 @@ lemma pullbackSpecIso_inv_fst :
     (pullbackSpecIso R S T).inv ≫ pullback.fst _ _ = Spec.map (ofHom includeLeftRingHom) :=
   limit.isoLimitCone_inv_π _ _
 
+@[reassoc]
+lemma pullbackSpecIso_inv_fst' :
+    (pullbackSpecIso R S T).inv ≫ pullback.fst _ _ = Spec.map (ofHom (algebraMap S _)) :=
+  pullbackSpecIso_inv_fst ..
+
 /--
 The composition of the inverse of the isomorphism `pullbackSpecIso R S T` (from the pullback of
 `Spec S ⟶ Spec R` and `Spec T ⟶ Spec R` to `Spec (S ⊗[R] T)`) with the second projection is
@@ -685,6 +698,11 @@ lemma pullbackSpecIso_hom_fst :
     (pullbackSpecIso R S T).hom ≫ Spec.map (ofHom includeLeftRingHom) = pullback.fst _ _ := by
   rw [← pullbackSpecIso_inv_fst, Iso.hom_inv_id_assoc]
 
+@[reassoc (attr := simp)]
+lemma pullbackSpecIso_hom_fst' :
+    (pullbackSpecIso R S T).hom ≫ Spec.map (ofHom (algebraMap S _)) = pullback.fst _ _ :=
+  pullbackSpecIso_hom_fst ..
+
 /--
 The composition of the isomorphism `pullbackSpecIso R S T` (from the pullback of
 `Spec S ⟶ Spec R` and `Spec T ⟶ Spec R` to `Spec (S ⊗[R] T)`) with the morphism
@@ -696,6 +714,12 @@ lemma pullbackSpecIso_hom_snd :
     (pullbackSpecIso R S T).hom ≫ Spec.map (ofHom (toRingHom includeRight)) = pullback.snd _ _ := by
   rw [← pullbackSpecIso_inv_snd, Iso.hom_inv_id_assoc]
 
+@[reassoc (attr := simp)]
+lemma pullbackSpecIso_hom_base :
+    (pullbackSpecIso R S T).hom ≫ Spec.map (ofHom (algebraMap R _)) =
+      pullback.fst _ _ ≫ Spec.map (ofHom (algebraMap _ _)) := by
+  simp [Algebra.TensorProduct.algebraMap_def]
+
 lemma isPullback_SpecMap_of_isPushout {A B C P : CommRingCat} (f : A ⟶ B) (g : A ⟶ C)
     (inl : B ⟶ P) (inr : C ⟶ P) (h : IsPushout f g inl inr) :
     IsPullback (Spec.map inl) (Spec.map inr) (Spec.map f) (Spec.map g) :=
@@ -726,12 +750,28 @@ lemma diagonal_SpecMap :
 
 end Spec
 
-section CartesianMonoidalCategory
-variable {S : Scheme}
+namespace Scheme
+variable {M S T : Scheme.{u}} [M.Over S] {f : T ⟶ S}
 
-instance : CartesianMonoidalCategory (Over S) := Over.cartesianMonoidalCategory _
-instance : BraidedCategory (Over S) := .ofCartesianMonoidalCategory
+@[simps]
+instance canonicallyOverPullback : (pullback (M ↘ S) f).CanonicallyOver T where
+  hom := pullback.snd (M ↘ S) f
 
-end CartesianMonoidalCategory
+@[simps! -isSimp mul one]
+instance monObjAsOverPullback [MonObj (asOver M S)] : MonObj (asOver (pullback (M ↘ S) f) T) := by
+  unfold asOver OverClass.asOver at *; exact Over.monObjMkPullbackSnd
+
+instance isCommMonObj_asOver_pullback [MonObj (asOver M S)] [IsCommMonObj (asOver M S)] :
+    IsCommMonObj (asOver (pullback (M ↘ S) f) T) := by
+  unfold asOver OverClass.asOver at *; exact Over.isCommMonObj_mk_pullbackSnd
+
+instance GrpObjAsOverPullback [GrpObj (asOver M S)] : GrpObj (asOver (pullback (M ↘ S) f) T) := by
+  unfold asOver OverClass.asOver at *; exact Over.grpObjMkPullbackSnd
 
-end AlgebraicGeometry
+instance : (pullback.fst (M ↘ S) (𝟙 S)).IsOver S := ⟨pullback.condition.trans (by simp)⟩
+
+instance isMonHom_fst_id_right [MonObj (asOver M S)] :
+    IsMonHom ((pullback.fst (M ↘ S) (𝟙 S)).asOver S) := by
+  unfold asOver OverClass.asOver at *; exact Over.isMonHom_pullbackFst_id_right
+
+end AlgebraicGeometry.Scheme

Mathlib/CategoryTheory/Monoidal/Cartesian/Over.lean

@@ -5,8 +5,11 @@ Authors: Andrew Yang
 -/
 module
 
-public import Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
+public import Mathlib.CategoryTheory.Adjunction.Limits
+public import Mathlib.CategoryTheory.Comma.Over.Pullback
 public import Mathlib.CategoryTheory.Limits.Constructions.Over.Products
+public import Mathlib.CategoryTheory.Monoidal.CommMon_
+public import Mathlib.CategoryTheory.Monoidal.Grp_
 
 /-!
 
@@ -17,28 +20,29 @@ for the induced `MonoidalCategory (Over X)` instance.
 
 -/
 
-@[expose] public section
+public noncomputable section
 
 namespace CategoryTheory.Over
 
-open Limits CartesianMonoidalCategory
+open Functor Limits CartesianMonoidalCategory
 
 variable {C : Type*} [Category C] [HasPullbacks C]
 
 /-- A choice of finite products of `Over X` given by `Limits.pullback`. -/
-noncomputable abbrev cartesianMonoidalCategory (X : C) : CartesianMonoidalCategory (Over X) :=
+abbrev cartesianMonoidalCategory (X : C) : CartesianMonoidalCategory (Over X) :=
   .ofChosenFiniteProducts
     ⟨asEmptyCone (Over.mk (𝟙 X)), IsTerminal.ofUniqueHom (fun Y ↦ Over.homMk Y.hom)
       fun Y m ↦ Over.OverMorphism.ext (by simpa using m.w)⟩
     fun Y Z ↦ ⟨pullbackConeEquivBinaryFan.functor.obj (pullback.cone Y.hom Z.hom),
     (pullback.isLimit _ _).pullbackConeEquivBinaryFanFunctor⟩
 
-@[deprecated (since := "2025-05-15")] alias chosenFiniteProducts := cartesianMonoidalCategory
+@[deprecated (since := "2025-05-15")]
+noncomputable alias chosenFiniteProducts := cartesianMonoidalCategory
 
 attribute [local instance] cartesianMonoidalCategory
 
 /-- `Over X` is braided w.r.t. the Cartesian monoidal structure given by `Limits.pullback`. -/
-noncomputable abbrev braidedCategory (X : C) : BraidedCategory (Over X) :=
+abbrev braidedCategory (X : C) : BraidedCategory (Over X) :=
   .ofCartesianMonoidalCategory
 
 attribute [local instance] braidedCategory
@@ -54,7 +58,7 @@ lemma tensorObj_ext {R : C} {S T : Over X} (f₁ f₂ : R ⟶ (S ⊗ T).left)
   pullback.hom_ext e₁ e₂
 
 @[simp]
-lemma tensorObj_left (R S : Over X) : (R ⊗ S).left = pullback R.hom S.hom := rfl
+lemma tensorObj_left (R S : Over X) : (R ⊗ S).left = Limits.pullback R.hom S.hom := rfl
 
 @[simp]
 lemma tensorObj_hom (R S : Over X) : (R ⊗ S).hom = pullback.fst R.hom S.hom ≫ R.hom := rfl
@@ -185,4 +189,127 @@ lemma braiding_hom_left {R S : Over X} :
 lemma braiding_inv_left {R S : Over X} :
     (β_ R S).inv.left = (pullbackSymmetry _ _).hom := rfl
 
+variable {A B R S Y Z : C} {f : R ⟶ X} {g : S ⟶ X}
+
+instance : (Over.pullback f).Braided := .ofChosenFiniteProducts _
+
+@[simp]
+lemma η_pullback_left : (OplaxMonoidal.η (Over.pullback f)).left = (pullback.snd (𝟙 _) f) := rfl
+
+@[simp]
+lemma ε_pullback_left : (LaxMonoidal.ε (Over.pullback f)).left = inv (pullback.snd (𝟙 _) f) := by
+  apply IsIso.eq_inv_of_hom_inv_id
+  rw [← η_pullback_left, ← Over.comp_left, Monoidal.η_ε, Over.id_left]
+
+lemma μ_pullback_left_fst_fst (R S : Over X) :
+    (LaxMonoidal.μ (Over.pullback f) R S).left ≫
+      pullback.fst _ _ ≫ pullback.fst _ _ = pullback.fst _ _ ≫ pullback.fst _ _ := by
+  rw [Monoidal.μ_of_cartesianMonoidalCategory,
+    ← cancel_epi (prodComparisonIso (Over.pullback f) R S).hom.left, ← Over.comp_left_assoc,
+    Iso.hom_inv_id]
+  simp [CartesianMonoidalCategory.prodComparison, fst]
+
+lemma μ_pullback_left_fst_snd (R S : Over X) :
+    (LaxMonoidal.μ (Over.pullback f) R S).left ≫
+      pullback.fst _ _ ≫ pullback.snd _ _ = pullback.snd _ _ ≫ pullback.fst _ _ := by
+  rw [Monoidal.μ_of_cartesianMonoidalCategory,
+    ← cancel_epi (prodComparisonIso (Over.pullback f) R S).hom.left,
+    ← Over.comp_left_assoc, Iso.hom_inv_id]
+  simp [CartesianMonoidalCategory.prodComparison, snd]
+
+lemma μ_pullback_left_snd (R S : Over X) :
+    (LaxMonoidal.μ (Over.pullback f) R S).left ≫ pullback.snd _ _ =
+      pullback.snd _ _ ≫ pullback.snd _ _ := by
+  rw [Monoidal.μ_of_cartesianMonoidalCategory,
+    ← cancel_epi (prodComparisonIso (Over.pullback f) R S).hom.left,
+    ← Over.comp_left_assoc, Iso.hom_inv_id]
+  simp [CartesianMonoidalCategory.prodComparison]
+
+@[simp]
+lemma μ_pullback_left_fst_fst' (g₁ : Y ⟶ X) (g₂ : Z ⟶ X) :
+    (LaxMonoidal.μ (Over.pullback f) (.mk g₁) (.mk g₂)).left ≫
+      pullback.fst (pullback.fst g₁ g₂ ≫ g₁) f ≫ pullback.fst g₁ g₂ =
+        pullback.fst _ _ ≫ pullback.fst _ _ :=
+  μ_pullback_left_fst_fst ..
+
+@[simp]
+lemma μ_pullback_left_fst_snd' (g₁ : Y ⟶ X) (g₂ : Z ⟶ X) :
+    (LaxMonoidal.μ (Over.pullback f) (.mk g₁) (.mk g₂)).left ≫
+      pullback.fst (pullback.fst g₁ g₂ ≫ g₁) f ≫ pullback.snd g₁ g₂ =
+        pullback.snd _ _ ≫ pullback.fst _ _ :=
+  μ_pullback_left_fst_snd ..
+
+@[simp]
+lemma μ_pullback_left_snd' (g₁ : Y ⟶ X) (g₂ : Z ⟶ X) :
+    (LaxMonoidal.μ (Over.pullback f) (.mk g₁) (.mk g₂)).left ≫
+      pullback.snd (pullback.fst g₁ g₂ ≫ g₁) f =
+        pullback.snd _ _ ≫ pullback.snd _ _ := μ_pullback_left_snd ..
+
+@[simp]
+lemma preservesTerminalIso_pullback (f : R ⟶ S) :
+    preservesTerminalIso (Over.pullback f) =
+      Over.isoMk (asIso (pullback.snd (𝟙 _) f)) (by simp) := by
+  ext1; exact toUnit_unique _ _
+
+@[simp]
+lemma prodComparisonIso_pullback_inv_left_fst_fst (f : X ⟶ Y) (A B : Over Y) :
+    (prodComparisonIso (Over.pullback f) A B).inv.left ≫
+      pullback.fst (pullback.fst A.hom B.hom ≫ A.hom) f ≫ pullback.fst _ _ =
+        pullback.fst (pullback.snd A.hom f) (pullback.snd B.hom f) ≫ pullback.fst _ _ := by
+  rw [← cancel_epi (prodComparisonIso (Over.pullback f) A B).hom.left,
+    Over.hom_left_inv_left_assoc]
+  simp [CartesianMonoidalCategory.prodComparison, fst]
+
+@[simp]
+lemma prodComparisonIso_pullback_Spec_inv_left_fst_fst' (f : X ⟶ Y) (gA : A ⟶ Y) (gB : B ⟶ Y) :
+    (prodComparisonIso (Over.pullback f) (.mk gA) (.mk gB)).inv.left ≫
+      pullback.fst (pullback.fst gA gB ≫ gA) f ≫ pullback.fst _ _ =
+        pullback.fst (pullback.snd gA f) (pullback.snd gB f) ≫ pullback.fst _ _ :=
+  prodComparisonIso_pullback_inv_left_fst_fst ..
+
+@[simp]
+lemma prodComparisonIso_pullback_inv_left_fst_snd' (f : X ⟶ Y) (gA : A ⟶ Y) (gB : B ⟶ Y) :
+    (prodComparisonIso (Over.pullback f) (.mk gA) (.mk gB)).inv.left ≫
+      pullback.fst (pullback.fst gA gB ≫ gA) f ≫ pullback.snd _ _ =
+        pullback.snd _ _ ≫ pullback.fst _ _ := by
+  rw [← cancel_epi (prodComparisonIso (Over.pullback f) _ _).hom.left,
+    Over.hom_left_inv_left_assoc]
+  simp [CartesianMonoidalCategory.prodComparison, snd]
+
+@[simp]
+lemma prodComparisonIso_pullback_inv_left_snd' (f : X ⟶ Y) (gA : A ⟶ Y) (gB : B ⟶ Y) :
+    (prodComparisonIso (Over.pullback f) (.mk gA) (.mk gB)).inv.left ≫
+      pullback.snd (pullback.fst gA gB ≫ gA) f = pullback.snd _ _ ≫ pullback.snd _ _ := by
+  rw [← cancel_epi (prodComparisonIso (Over.pullback f) _ _).hom.left,
+    Over.hom_left_inv_left_assoc]
+  simp [CartesianMonoidalCategory.prodComparison]
+
+/-- The pullback of a monoid object is a monoid object. -/
+@[simps! -isSimp mul one]
+abbrev monObjMkPullbackSnd [MonObj (Over.mk f)] : MonObj (Over.mk <| pullback.snd f g) :=
+  ((Over.pullback g).mapMon.obj <| .mk <| .mk f).mon
+
+attribute [local instance] monObjMkPullbackSnd
+
+instance isCommMonObj_mk_pullbackSnd [MonObj (Over.mk f)] [IsCommMonObj (Over.mk f)] :
+    IsCommMonObj (Over.mk <| pullback.snd f g) :=
+  ((Over.pullback g).mapCommMon.obj <| .mk <| .mk f).comm
+
+/-- The pullback of a monoid object is a monoid object. -/
+@[simps! -isSimp mul one]
+abbrev grpObjMkPullbackSnd [GrpObj (Over.mk f)] : GrpObj (Over.mk (pullback.snd f g)) :=
+  ((Over.pullback g).mapGrp.obj <| .mk <| .mk f).grp
+
+attribute [local simp] monObjMkPullbackSnd_one in
+instance isMonHom_pullbackFst_id_right [MonObj (Over.mk f)] :
+    IsMonHom <| Over.homMk (U := Over.mk <| pullback.snd f (𝟙 X)) (V := Over.mk f)
+      (pullback.fst f (𝟙 X)) (pullback.condition.trans <| by simp) where
+  mul_hom := by
+    ext
+    dsimp [monObjMkPullbackSnd_mul]
+    simp only [Category.assoc, limit.lift_π, PullbackCone.mk_pt, PullbackCone.mk_π_app]
+    simp only [← Category.assoc]
+    congr 1
+    ext <;> simp
+
 end CategoryTheory.Over