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.

Equations

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

@[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 = of (TensorProduct R A B)

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.

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

Equations

• A.coproductCocone B = CategoryTheory.Limits.BinaryCofan.mk (CommRingCat.ofHom Algebra.TensorProduct.includeLeft.toRingHom) (CommRingCat.ofHom Algebra.TensorProduct.includeRight.toRingHom)

@[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 = of (TensorProduct ℤ ↑A ↑B)

@[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.

Equations

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

@[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.

Equations

• A.coproductColimitCocone B = { cocone := A.coproductCocone B, isColimit := A.coproductCoconeIsColimit B }

instance CommRingCat.instUniqueHomOfPUnit (X : CommRingCat) : Unique (X ⟶ of PUnit.{u + 1})

Equations

• X.instUniqueHomOfPUnit = { default := CommRingCat.ofHom { toMonoidHom := 1, map_zero' := ⋯, map_add' := ⋯ }, uniq := ⋯ }

def CommRingCat.punitIsTerminal : CategoryTheory.Limits.IsTerminal (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.7 + 1})

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 (of ℤ)

ℤ is the initial object of CommRingCat.

Equations

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

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

ULift.{u} ℤ is initial in CommRingCat.

Equations

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

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 = of (↑A × ↑B)

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.

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))) fun (i : ι) => CommRingCat.ofHom (Pi.evalRingHom (fun (i : ι) => ↑(R i)) i)

@[simp]

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

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

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

Equations

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

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

The categorical product and the usual product agree

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 agree

Equations

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

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 ((CommRingCat.Hom.hom f).eqLocus (CommRingCat.Hom.hom g)).subtype) ⋯

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.

Equations

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

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.

Equations

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

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.

Equations

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