Limits in Under R for a commutative ring R

We show that Under.pushout f is left-exact, i.e. preserves finite limits, if f : R ⟶ S is flat.

def CommRingCat.Under.piFan {R : CommRingCat} {ι : Type u} (P : ι → CategoryTheory.Under R) : CategoryTheory.Limits.Fan P

The canonical fan on P : ι → Under R given by ∀ i, P i.

noncomputable def CommRingCat.Under.piFanIsLimit {R : CommRingCat} {ι : Type u} (P : ι → CategoryTheory.Under R) : CategoryTheory.Limits.IsLimit (piFan P)

The canonical fan is limiting.

def CommRingCat.Under.tensorProductFan {R : CommRingCat} (S : CommRingCat) [Algebra ↑R ↑S] {ι : Type u} (P : ι → CategoryTheory.Under R) : CategoryTheory.Limits.Fan fun (i : ι) => S.mkUnder (TensorProduct ↑R ↑S ↑(P i).right)

The fan on i ↦ S ⊗[R] P i given by S ⊗[R] ∀ i, P i

def CommRingCat.Under.tensorProductFan' {R : CommRingCat} (S : CommRingCat) [Algebra ↑R ↑S] {ι : Type u} (P : ι → CategoryTheory.Under R) : CategoryTheory.Limits.Fan fun (i : ι) => S.mkUnder (TensorProduct ↑R ↑S ↑(P i).right)

The fan on i ↦ S ⊗[R] P i given by ∀ i, S ⊗[R] P i

def CommRingCat.Under.tensorProductFanIso {R S : CommRingCat} [Algebra ↑R ↑S] {ι : Type u} (P : ι → CategoryTheory.Under R) [Fintype ι] [DecidableEq ι] : tensorProductFan S P ≅ tensorProductFan' S P

The two fans on i ↦ S ⊗[R] P i agree if ι is finite.

noncomputable def CommRingCat.Under.tensorProductFanIsLimit {R S : CommRingCat} [Algebra ↑R ↑S] {ι : Type u} (P : ι → CategoryTheory.Under R) [Finite ι] : CategoryTheory.Limits.IsLimit (tensorProductFan S P)

The fan on i ↦ S ⊗[R] P i given by S ⊗[R] ∀ i, P i is limiting if ι is finite.

noncomputable def CommRingCat.Under.piFanTensorProductIsLimit {R S : CommRingCat} [Algebra ↑R ↑S] {ι : Type u} (P : ι → CategoryTheory.Under R) [Finite ι] : CategoryTheory.Limits.IsLimit ((R.tensorProd S).mapCone (piFan P))

tensorProd R S preserves the limit of the canonical fan on P.

instance CommRingCat.Under.instPreservesLimitUnderDiscreteFunctorTensorProdOfFinite {R S : CommRingCat} [Algebra ↑R ↑S] (J : Type u) [Finite J] (f : J → CategoryTheory.Under R) : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor f) (R.tensorProd S)

instance CommRingCat.Under.instPreservesFiniteProductsUnderTensorProd {R S : CommRingCat} [Algebra ↑R ↑S] : CategoryTheory.Limits.PreservesFiniteProducts (R.tensorProd S)

theorem CommRingCat.Under.equalizer_comp {R : CommRingCat} {A B : CategoryTheory.Under R} (f g : A ⟶ B) : CategoryTheory.CategoryStruct.comp (AlgHom.equalizer (toAlgHom f) (toAlgHom g)).val.toUnder f = CategoryTheory.CategoryStruct.comp (AlgHom.equalizer (toAlgHom f) (toAlgHom g)).val.toUnder g

def CommRingCat.Under.equalizerFork {R : CommRingCat} {A B : CategoryTheory.Under R} (f g : A ⟶ B) : CategoryTheory.Limits.Fork f g

The canonical fork on f g : A ⟶ B given by the equalizer.

@[simp]

theorem CommRingCat.Under.equalizerFork_ι {R : CommRingCat} {A B : CategoryTheory.Under R} (f g : A ⟶ B) : (equalizerFork f g).ι = (AlgHom.equalizer (toAlgHom f) (toAlgHom g)).val.toUnder

def CommRingCat.Under.equalizerFork' {R : CommRingCat} {A B : Type u} [CommRing A] [CommRing B] [Algebra (↑R) A] [Algebra (↑R) B] (f g : A →ₐ[↑R] B) : CategoryTheory.Limits.Fork f.toUnder g.toUnder

Variant of Under.equalizerFork' for algebra maps. This is definitionally equal to Under.equalizerFork but this is costly in applications.

@[simp]

theorem CommRingCat.Under.equalizerFork'_ι {R : CommRingCat} {A B : Type u} [CommRing A] [CommRing B] [Algebra (↑R) A] [Algebra (↑R) B] (f g : A →ₐ[↑R] B) : (equalizerFork' f g).ι = (AlgHom.equalizer f g).val.toUnder

noncomputable def CommRingCat.Under.equalizerForkIsLimit {R : CommRingCat} {A B : CategoryTheory.Under R} (f g : A ⟶ B) : CategoryTheory.Limits.IsLimit (equalizerFork f g)

The canonical fork on f g : A ⟶ B is limiting.

noncomputable def CommRingCat.Under.equalizerFork'IsLimit {R : CommRingCat} {A B : Type u} [CommRing A] [CommRing B] [Algebra (↑R) A] [Algebra (↑R) B] (f g : A →ₐ[↑R] B) : CategoryTheory.Limits.IsLimit (equalizerFork' f g)

Variant of Under.equalizerForkIsLimit for algebra maps.

def CommRingCat.Under.tensorProdEqualizer {R S : CommRingCat} [Algebra ↑R ↑S] {A B : CategoryTheory.Under R} (f g : A ⟶ B) : CategoryTheory.Limits.Fork ((R.tensorProd S).map f) ((R.tensorProd S).map g)

The fork on 𝟙 ⊗[R] f and 𝟙 ⊗[R] g given by S ⊗[R] eq(f, g).

@[simp]

theorem CommRingCat.Under.tensorProdEqualizer_ι {R S : CommRingCat} [Algebra ↑R ↑S] {A B : CategoryTheory.Under R} (f g : A ⟶ B) : (tensorProdEqualizer f g).ι = (R.tensorProd S).map (AlgHom.equalizer (toAlgHom f) (toAlgHom g)).val.toUnder

noncomputable def CommRingCat.Under.equalizerForkTensorProdIso {R S : CommRingCat} [Algebra ↑R ↑S] [Module.Flat ↑R ↑S] {A B : CategoryTheory.Under R} (f g : A ⟶ B) : tensorProdEqualizer f g ≅ equalizerFork' (Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (toAlgHom f)) (Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (toAlgHom g))

If S is R-flat, S ⊗[R] eq(f, g) is isomorphic to eq(𝟙 ⊗[R] f, 𝟙 ⊗[R] g).

noncomputable def CommRingCat.Under.tensorProdMapEqualizerForkIsLimit {R S : CommRingCat} [Algebra ↑R ↑S] [Module.Flat ↑R ↑S] {A B : CategoryTheory.Under R} (f g : A ⟶ B) : CategoryTheory.Limits.IsLimit ((R.tensorProd S).mapCone (equalizerFork f g))

If S is R-flat, tensorProd R S preserves the equalizer of f and g.

instance CommRingCat.Under.instPreservesLimitUnderWalkingParallelPairParallelPairTensorProdOfFlatCarrier {R S : CommRingCat} [Algebra ↑R ↑S] [Module.Flat ↑R ↑S] {A B : CategoryTheory.Under R} (f g : A ⟶ B) : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f g) (R.tensorProd S)

instance CommRingCat.Under.instPreservesLimitsOfShapeUnderWalkingParallelPairTensorProdOfFlatCarrier {R S : CommRingCat} [Algebra ↑R ↑S] [Module.Flat ↑R ↑S] : CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingParallelPair (R.tensorProd S)

instance CommRingCat.Under.instPreservesFiniteLimitsUnderTensorProdOfFlatCarrier {R S : CommRingCat} [Algebra ↑R ↑S] [Module.Flat ↑R ↑S] : CategoryTheory.Limits.PreservesFiniteLimits (R.tensorProd S)

instance CommRingCat.Under.instPreservesFiniteProductsUnderPushout {R S : CommRingCat} (f : R ⟶ S) : CategoryTheory.Limits.PreservesFiniteProducts (CategoryTheory.Under.pushout f)

Under.pushout f preserves finite products.

theorem CommRingCat.Under.preservesFiniteLimits_of_flat {R S : CommRingCat} (f : R ⟶ S) (hf : (Hom.hom f).Flat) : CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.Under.pushout f)

Under.pushout f preserves finite limits if f is flat.