Constructions of (co)limits in CommRingCat

In this file we provide the explicit (co)cones for various (co)limits in CommRingCat, including

• tensor product is the pushout
• tensor product over ℤ is the binary coproduct
• ℤ is the initial object
• 0 is the strict terminal object
• Cartesian product is the product
• arbitrary direct product of a family of rings is the product object (Pi object)
• RingHom.eqLocus is the equalizer

def CommRingCat.pushoutCocone (R A B : Type u) [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] : CategoryTheory.Limits.PushoutCocone (ofHom (algebraMap R A)) (ofHom (algebraMap R B))

The explicit cocone with tensor products as the fibered product in CommRingCat.

@[simp]

theorem CommRingCat.pushoutCocone_inl (R A B : Type u) [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] : (pushoutCocone R A B).inl = ofHom Algebra.TensorProduct.includeLeftRingHom

@[simp]

theorem CommRingCat.pushoutCocone_inr (R A B : Type u) [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] : (pushoutCocone R A B).inr = ofHom Algebra.TensorProduct.includeRight.toRingHom

@[simp]

theorem CommRingCat.pushoutCocone_pt (R A B : Type u) [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] : (pushoutCocone R A B).pt = { carrier := TensorProduct R A B, commRing := Algebra.TensorProduct.instCommRing }

def CommRingCat.pushoutCoconeIsColimit (R A B : Type u) [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] : CategoryTheory.Limits.IsColimit (pushoutCocone R A B)

Verify that the pushout_cocone is indeed the colimit.

theorem CommRingCat.isPushout_tensorProduct (R A B : Type u) [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] : CategoryTheory.IsPushout (ofHom (algebraMap R A)) (ofHom (algebraMap R B)) (ofHom Algebra.TensorProduct.includeLeftRingHom) (ofHom Algebra.TensorProduct.includeRight.toRingHom)

theorem CommRingCat.isPushout_of_isPushout (R S A B : Type u) [CommRing R] [CommRing S] [CommRing A] [CommRing B] [Algebra R S] [Algebra S B] [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B] [IsScalarTower R S B] [Algebra.IsPushout R S A B] : CategoryTheory.IsPushout (ofHom (algebraMap R S)) (ofHom (algebraMap R A)) (ofHom (algebraMap S B)) (ofHom (algebraMap A B))

theorem CommRingCat.isPushout_iff_isPushout {R S : Type u} [CommRing R] [CommRing S] [Algebra R S] {R' S' : Type u} [CommRing R'] [CommRing S'] [Algebra R R'] [Algebra S S'] [Algebra R' S'] [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] : CategoryTheory.IsPushout (ofHom (algebraMap R R')) (ofHom (algebraMap R S)) (ofHom (algebraMap R' S')) (ofHom (algebraMap S S')) ↔ Algebra.IsPushout R R' S S'

theorem CommRingCat.isPushout_of_isLocalization {R S Rₘ Sₘ : Type u} [CommRing R] [CommRing Rₘ] [Algebra R Rₘ] [CommRing S] [CommRing Sₘ] [Algebra S Sₘ] (f : R →+* S) (fₘ : Rₘ →+* Sₘ) (H : fₘ.comp (algebraMap R Rₘ) = (algebraMap S Sₘ).comp f) (M : Submonoid R) [IsLocalization M Rₘ] [IsLocalization (Submonoid.map f M) Sₘ] : CategoryTheory.IsPushout (ofHom f) (ofHom (algebraMap R Rₘ)) (ofHom (algebraMap S Sₘ)) (ofHom fₘ)

theorem CommRingCat.closure_range_union_range_eq_top_of_isPushout {R A B X : CommRingCat} {f : R ⟶ A} {g : R ⟶ B} {a : A ⟶ X} {b : B ⟶ X} (H : CategoryTheory.IsPushout f g a b) : Subring.closure (Set.range ⇑(CategoryTheory.ConcreteCategory.hom a) ∪ Set.range ⇑(CategoryTheory.ConcreteCategory.hom b)) = ⊤

def CommRingCat.coproductCocone (A B : CommRingCat) : CategoryTheory.Limits.BinaryCofan A B

The tensor product A ⊗[ℤ] B forms a cocone for A and B.

@[simp]

theorem CommRingCat.coproductCocone_ι (A B : CommRingCat) : (A.coproductCocone B).ι = { app := fun (x : CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) => match x.as with | CategoryTheory.Limits.WalkingPair.left => ofHom ↑Algebra.TensorProduct.includeLeft | CategoryTheory.Limits.WalkingPair.right => ofHom ↑Algebra.TensorProduct.includeRight, naturality := ⋯ }

@[simp]

theorem CommRingCat.coproductCocone_pt (A B : CommRingCat) : (A.coproductCocone B).pt = { carrier := TensorProduct ℤ ↑A ↑B, commRing := Algebra.TensorProduct.instCommRing }

@[simp]

theorem CommRingCat.coproductCocone_inl (A B : CommRingCat) : (A.coproductCocone B).inl = ofHom Algebra.TensorProduct.includeLeft.toRingHom

@[simp]

theorem CommRingCat.coproductCocone_inr (A B : CommRingCat) : (A.coproductCocone B).inr = ofHom Algebra.TensorProduct.includeRight.toRingHom

def CommRingCat.coproductCoconeIsColimit (A B : CommRingCat) : CategoryTheory.Limits.IsColimit (A.coproductCocone B)

The tensor product A ⊗[ℤ] B is a coproduct for A and B.

@[simp]

theorem CommRingCat.coproductCoconeIsColimit_desc (A B : CommRingCat) (s : CategoryTheory.Limits.BinaryCofan A B) : (A.coproductCoconeIsColimit B).desc s = ofHom (Algebra.TensorProduct.lift (Hom.hom s.inl).toIntAlgHom (Hom.hom s.inr).toIntAlgHom ⋯).toRingHom

def CommRingCat.coproductColimitCocone (A B : CommRingCat) : CategoryTheory.Limits.ColimitCocone (CategoryTheory.Limits.pair A B)

The limit cone of the tensor product A ⊗[ℤ] B in CommRingCat.

instance CommRingCat.instUniqueHomOfPUnit (X : CommRingCat) : Unique (X ⟶ { carrier := PUnit.{u + 1}, commRing := PUnit.commRing })

def CommRingCat.punitIsTerminal : CategoryTheory.Limits.IsTerminal { carrier := PUnit.{u + 1}, commRing := PUnit.commRing }

The trivial ring is the (strict) terminal object of CommRingCat.

instance CommRingCat.commRingCat_hasStrictTerminalObjects : CategoryTheory.Limits.HasStrictTerminalObjects CommRingCat

theorem CommRingCat.subsingleton_of_isTerminal {X : CommRingCat} (hX : CategoryTheory.Limits.IsTerminal X) : Subsingleton ↑X

def CommRingCat.zIsInitial : CategoryTheory.Limits.IsInitial { carrier := ℤ, commRing := Int.instCommRing }

ℤ is the initial object of CommRingCat.

def CommRingCat.isInitial : CategoryTheory.Limits.IsInitial { carrier := ULift.{u, 0} ℤ, commRing := ULift.commRing }

ULift.{u} ℤ is initial in CommRingCat.

def CommRingCat.prodFan (A B : CommRingCat) : CategoryTheory.Limits.BinaryFan A B

The product in CommRingCat is the Cartesian product. This is the binary fan.

@[simp]

theorem CommRingCat.prodFan_pt (A B : CommRingCat) : (A.prodFan B).pt = { carrier := ↑A × ↑B, commRing := Prod.instCommRing }

def CommRingCat.prodFanIsLimit (A B : CommRingCat) : CategoryTheory.Limits.IsLimit (A.prodFan B)

The product in CommRingCat is the Cartesian product.

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

The categorical product of rings is the Cartesian product of rings. This is its Fan.

@[simp]

theorem CommRingCat.piFan_pt {ι : Type u} (R : ι → CommRingCat) : (piFan R).pt = { carrier := (i : ι) → ↑(R i), commRing := Pi.commRing }

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

The categorical product of rings is the Cartesian product of rings.

noncomputable def CommRingCat.piIsoPi {ι : Type u} (R : ι → CommRingCat) : ∏ᶜ R ≅ { carrier := (i : ι) → ↑(R i), commRing := Pi.commRing }

The categorical product and the usual product agree

noncomputable def RingEquiv.piEquivPi {ι : Type u} (R : ι → Type u) [(i : ι) → CommRing (R i)] : ↑(∏ᶜ fun (i : ι) => { carrier := R i, commRing := inst✝ i }) ≃+* ((i : ι) → R i)

The categorical product and the usual product agree

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

The equalizer in CommRingCat is the equalizer as sets. This is the equalizer fork.

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

The equalizer in CommRingCat is the equalizer as sets.

instance CommRingCat.instIsLocalHomCarrierObjWalkingParallelPairFunctorConstPtEqualizerForkZeroParallelPairRingHomHomι {A B : CommRingCat} (f g : A ⟶ B) : IsLocalHom (Hom.hom (equalizerFork f g).ι)

instance CommRingCat.equalizer_ι_isLocalHom (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair CommRingCat) : IsLocalHom (Hom.hom (CategoryTheory.Limits.limit.π F CategoryTheory.Limits.WalkingParallelPair.zero))

instance CommRingCat.equalizer_ι_isLocalHom' (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPairᵒᵖ CommRingCat) : IsLocalHom (Hom.hom (CategoryTheory.Limits.limit.π F (Opposite.op CategoryTheory.Limits.WalkingParallelPair.one)))

def CommRingCat.pullbackCone {A B C : CommRingCat} (f : A ⟶ C) (g : B ⟶ C) : CategoryTheory.Limits.PullbackCone f g

In the category of CommRingCat, the pullback of f : A ⟶ C and g : B ⟶ C is the eqLocus of the two maps A × B ⟶ C. This is the constructed pullback cone.

def CommRingCat.pullbackConeIsLimit {A B C : CommRingCat} (f : A ⟶ C) (g : B ⟶ C) : CategoryTheory.Limits.IsLimit (pullbackCone f g)

The constructed pullback cone is indeed the limit.