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
• Z is the initial object
• 0 is the strict terminal object
• cartesian product is the product
• RingHom.eqLocus is the equalizer

def CommRingCat.pushoutCocone {R : CommRingCat} {A : CommRingCat} {B : CommRingCat} (f : R ⟶ A) (g : R ⟶ B) : CategoryTheory.Limits.PushoutCocone f g

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CommRingCat.pushoutCocone_inl {R : CommRingCat} {A : CommRingCat} {B : CommRingCat} (f : R ⟶ A) (g : R ⟶ B) : CategoryTheory.Limits.PushoutCocone.inl (CommRingCat.pushoutCocone f g) = Algebra.TensorProduct.includeLeftRingHom

@[simp]

theorem CommRingCat.pushoutCocone_inr {R : CommRingCat} {A : CommRingCat} {B : CommRingCat} (f : R ⟶ A) (g : R ⟶ B) : CategoryTheory.Limits.PushoutCocone.inr (CommRingCat.pushoutCocone f g) = ↑Algebra.TensorProduct.includeRight

@[simp]

theorem CommRingCat.pushoutCocone_pt {R : CommRingCat} {A : CommRingCat} {B : CommRingCat} (f : R ⟶ A) (g : R ⟶ B) : (CommRingCat.pushoutCocone f g).pt = CommRingCat.of (TensorProduct ↑R ↑A ↑B)

def CommRingCat.pushoutCoconeIsColimit {R : CommRingCat} {A : CommRingCat} {B : CommRingCat} (f : R ⟶ A) (g : R ⟶ B) : CategoryTheory.Limits.IsColimit (CommRingCat.pushoutCocone f g)

Verify that the pushout_cocone is indeed the colimit.

Equations

• One or more equations did not get rendered due to their size.

def CommRingCat.punitIsTerminal : CategoryTheory.Limits.IsTerminal (CommRingCat.of PUnit.{u + 1} )

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

Equations

• CommRingCat.punitIsTerminal = CategoryTheory.Limits.IsTerminal.ofUnique (CommRingCat.of PUnit.{u + 1} )

instance CommRingCat.commRingCat_hasStrictTerminalObjects : CategoryTheory.Limits.HasStrictTerminalObjects CommRingCat

Equations

• CommRingCat.commRingCat_hasStrictTerminalObjects = CommRingCat.commRingCat_hasStrictTerminalObjects.proof_1

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

def CommRingCat.zIsInitial : CategoryTheory.Limits.IsInitial (CommRingCat.of ℤ)

ℤ is the initial object of CommRingCat.

Equations

• CommRingCat.zIsInitial = CategoryTheory.Limits.IsInitial.ofUnique (CommRingCat.of ℤ)

@[simp]

theorem CommRingCat.prodFan_pt (A : CommRingCat) (B : CommRingCat) : (CommRingCat.prodFan A B).pt = CommRingCat.of (↑A × ↑B)

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

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

Equations

• CommRingCat.prodFan A B = CategoryTheory.Limits.BinaryFan.mk (CommRingCat.ofHom (RingHom.fst ↑A ↑B)) (CommRingCat.ofHom (RingHom.snd ↑A ↑B))

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

The product in CommRingCat is the cartesian product.

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

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

The equalizer in CommRingCat is the equalizer as sets.

Equations

• One or more equations did not get rendered due to their size.

instance CommRingCat.instIsLocalRingHomαCommRingObjWalkingParallelPairToQuiverToCategoryStructWalkingParallelPairHomCategoryCommRingCatToQuiverToCategoryStructInstCommRingCatLargeCategoryToPrefunctorObjFunctorCategoryToPrefunctorConstPtParallelPairEqualizerForkZeroToSemiringToRingStrι {A : CommRingCat} {B : CommRingCat} (f : A ⟶ B) (g : A ⟶ B) : IsLocalRingHom (CategoryTheory.Limits.Fork.ι (CommRingCat.equalizerFork f g))

Equations

• One or more equations did not get rendered due to their size.

instance CommRingCat.equalizer_ι_isLocalRingHom (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair CommRingCat) : IsLocalRingHom (CategoryTheory.Limits.limit.π F CategoryTheory.Limits.WalkingParallelPair.zero)

Equations

• CommRingCat.equalizer_ι_isLocalRingHom = CommRingCat.equalizer_ι_isLocalRingHom.proof_1

instance CommRingCat.equalizer_ι_is_local_ring_hom' (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPairᵒᵖ CommRingCat) : IsLocalRingHom (CategoryTheory.Limits.limit.π F (Opposite.op CategoryTheory.Limits.WalkingParallelPair.one))

Equations

• CommRingCat.equalizer_ι_is_local_ring_hom' = CommRingCat.equalizer_ι_is_local_ring_hom'.proof_1

def CommRingCat.pullbackCone {A : CommRingCat} {B : CommRingCat} {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.

Equations

• One or more equations did not get rendered due to their size.

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

The constructed pullback cone is indeed the limit.

Equations

• One or more equations did not get rendered due to their size.