mathlib documentation

algebra.category.Ring.constructions

Constructions of (co)limits in CommRing #

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

source
def CommRing.pushout_cocone {R A B : CommRing} (f : R ⟶ A) (g : R ⟶ B) :
category_theory.limits.pushout_cocone f g

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

Equations
source
@[simp]
theorem CommRing.pushout_cocone_inl {R A B : CommRing} (f : R ⟶ A) (g : R ⟶ B) :
(CommRing.pushout_cocone f g).inl = let _inst : algebra ↥R ↥A := ring_hom.to_algebra f, _inst_1 : algebra ↥R ↥B := ring_hom.to_algebra g in algebra.tensor_product.include_left.to_ring_hom
source
@[simp]
theorem CommRing.pushout_cocone_inr {R A B : CommRing} (f : R ⟶ A) (g : R ⟶ B) :
(CommRing.pushout_cocone f g).inr = let _inst : algebra ↥R ↥A := ring_hom.to_algebra f, _inst_1 : algebra ↥R ↥B := ring_hom.to_algebra g in algebra.tensor_product.include_right.to_ring_hom
source
@[simp]
theorem CommRing.pushout_cocone_X {R A B : CommRing} (f : R ⟶ A) (g : R ⟶ B) :
(CommRing.pushout_cocone f g).X = let _inst : algebra ↥R ↥A := ring_hom.to_algebra f, _inst_1 : algebra ↥R ↥B := ring_hom.to_algebra g in CommRing.of (tensor_product ↥R ↥A ↥B)
source
def CommRing.pushout_cocone_is_colimit {R A B : CommRing} (f : R ⟶ A) (g : R ⟶ B) :
category_theory.limits.is_colimit (CommRing.pushout_cocone f g)

Verify that the pushout_cocone is indeed the colimit.

Equations
source
def CommRing.punit_is_terminal  :
category_theory.limits.is_terminal (CommRing.of punit)

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

Equations
source
@[protected, instance]
def CommRing.CommRing_has_strict_terminal_objects  :
category_theory.limits.has_strict_terminal_objects CommRing
source
theorem CommRing.subsingleton_of_is_terminal {X : CommRing} (hX : category_theory.limits.is_terminal X) :
subsingleton ↥X
source
def CommRing.Z_is_initial  :
category_theory.limits.is_initial (CommRing.of ℤ)

ℤ is the initial object of CommRing.

Equations
source
def CommRing.prod_fan (A B : CommRing) :
category_theory.limits.binary_fan A B

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

Equations
source
@[simp]
theorem CommRing.prod_fan_X (A B : CommRing) :
(A.prod_fan B).X = CommRing.of (↥A × ↥B)
source
def CommRing.prod_fan_is_limit (A B : CommRing) :
category_theory.limits.is_limit (A.prod_fan B)

The product in CommRing is the cartesian product.

Equations
source
def CommRing.equalizer_fork {A B : CommRing} (f g : A ⟶ B) :
category_theory.limits.fork f g

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

Equations
source
def CommRing.equalizer_fork_is_limit {A B : CommRing} (f g : A ⟶ B) :
category_theory.limits.is_limit (CommRing.equalizer_fork f g)

The equalizer in CommRing is the equalizer as sets.

Equations
source
@[protected, instance]
def CommRing.ι.is_local_ring_hom {A B : CommRing} (f g : A ⟶ B) :
is_local_ring_hom (CommRing.equalizer_fork f g).ι
source
@[protected, instance]
def CommRing.equalizer_ι_is_local_ring_hom (F : category_theory.limits.walking_parallel_pair ⥤ CommRing) :
is_local_ring_hom (category_theory.limits.limit.π F category_theory.limits.walking_parallel_pair.zero)
source
@[protected, instance]
def CommRing.equalizer_ι_is_local_ring_hom' (F : category_theory.limits.walking_parallel_pairᵒᵖ ⥤ CommRing) :
is_local_ring_hom (category_theory.limits.limit.π F (opposite.op category_theory.limits.walking_parallel_pair.one))
source
def CommRing.pullback_cone {A B C : CommRing} (f : A ⟶ C) (g : B ⟶ C) :
category_theory.limits.pullback_cone f g

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

Equations
source
def CommRing.pullback_cone_is_limit {A B C : CommRing} (f : A ⟶ C) (g : B ⟶ C) :
category_theory.limits.is_limit (CommRing.pullback_cone f g)

The constructed pullback cone is indeed the limit.

Equations