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
• arbitrary direct product of a family of rings is the product object (Pi object)
• RingHom.eqLocus is the equalizer

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

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

Equations

• CommRingCat.pushoutCocone R A B = CategoryTheory.Limits.PushoutCocone.mk Algebra.TensorProduct.includeLeftRingHom Algebra.TensorProduct.includeRight.toRingHom ⋯

@[simp]

theorem CommRingCat.pushoutCocone_inl (R A B : Type u) [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] : (CommRingCat.pushoutCocone R A B).inl = 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] : (CommRingCat.pushoutCocone R A B).inr = 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] : (CommRingCat.pushoutCocone R A B).pt = CommRingCat.of (TensorProduct R A B)

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

Verify that the pushout_cocone is indeed the colimit.

Equations

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

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

noncomputable 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.12 + 1} )

noncomputable instance CommRingCat.commRingCat_hasStrictTerminalObjects : CategoryTheory.Limits.HasStrictTerminalObjects CommRingCat

Equations

• CommRingCat.commRingCat_hasStrictTerminalObjects = ⋯

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

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

ℤ is the initial object of CommRingCat.

Equations

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

noncomputable def CommRingCat.isInitial : CategoryTheory.Limits.IsInitial (CommRingCat.of (ULift.{u, 0} ℤ))

ULift.{u} ℤ is initial in CommRingCat.

Equations

• CommRingCat.isInitial = CategoryTheory.Limits.IsInitial.ofUnique (CommRingCat.of (ULift.{?u.9, 0} ℤ))

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

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

Equations

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

@[simp]

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

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

The product in CommRingCat is the cartesian product.

Equations

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

noncomputable 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.

Equations

• CommRingCat.piFan R = CategoryTheory.Limits.Fan.mk (CommRingCat.of ((i : ι) → ↑(R i))) (Pi.evalRingHom fun (i : ι) => ↑(R i))

@[simp]

theorem CommRingCat.piFan_pt {ι : Type u} (R : ι → CommRingCat) : (CommRingCat.piFan R).pt = CommRingCat.of ((i : ι) → ↑(R i))

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

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

Equations

• CommRingCat.piFanIsLimit R = { lift := fun (s : CategoryTheory.Limits.Cone (CategoryTheory.Discrete.functor R)) => Pi.ringHom fun (i : ι) => s.π.app { as := i }, fac := ⋯, uniq := ⋯ }

noncomputable def CommRingCat.piIsoPi {ι : Type u} (R : ι → CommRingCat) : ∏ᶜ R ≅ CommRingCat.of ((i : ι) → ↑(R i))

The categorical product and the usual product agrees

Equations

• CommRingCat.piIsoPi R = CategoryTheory.Limits.limit.isoLimitCone { cone := CommRingCat.piFan R, isLimit := CommRingCat.piFanIsLimit R }

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

The categorical product and the usual product agrees

Equations

• RingEquiv.piEquivPi R = (CommRingCat.piIsoPi fun (x : ι) => CommRingCat.of (R x)).commRingCatIsoToRingEquiv

noncomputable 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.

Equations

• CommRingCat.equalizerFork f g = CategoryTheory.Limits.Fork.ofι (CommRingCat.ofHom (RingHom.eqLocus f g).subtype) ⋯

noncomputable def CommRingCat.equalizerForkIsLimit {A B : CommRingCat} (f 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.

noncomputable instance CommRingCat.instIsLocalHomαCommRingObjWalkingParallelPairFunctorConstPtEqualizerForkZeroParallelPairHomι {A B : CommRingCat} (f g : A ⟶ B) : IsLocalHom (CommRingCat.equalizerFork f g).ι

Equations

• ⋯ = ⋯

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

@[deprecated CommRingCat.equalizer_ι_isLocalHom]

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

Alias of CommRingCat.equalizer_ι_isLocalHom.

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

Equations

• ⋯ = ⋯

noncomputable 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.

Equations

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

noncomputable def CommRingCat.pullbackConeIsLimit {A B 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.