Constructions of (co)limits in CommRing #
In this file we provide the explicit (co)cones for various (co)limits in CommRing
, including
- tensor product is the pushout
Z
is the initial object0
is the strict terminal object- cartesian product is the product
ring_hom.eq_locus
is the equalizer
The explicit cocone with tensor products as the fibered product in CommRing
.
Equations
- CommRing.pushout_cocone f g = let _inst : algebra ↥R ↥A := ring_hom.to_algebra f, _inst_1 : algebra ↥R ↥B := ring_hom.to_algebra g in category_theory.limits.pushout_cocone.mk (id algebra.tensor_product.include_left.to_ring_hom) (id algebra.tensor_product.include_right.to_ring_hom) _
@[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
@[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
@[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)
Verify that the pushout_cocone
is indeed the colimit.
Equations
- CommRing.pushout_cocone_is_colimit f g = (CommRing.pushout_cocone f g).is_colimit_aux' (λ (s : category_theory.limits.pushout_cocone f g), let _inst : algebra ↥R ↥A := ring_hom.to_algebra f, _inst_1 : algebra ↥R ↥B := ring_hom.to_algebra g, _inst_2 : algebra ↥R ↥(s.X) := ring_hom.to_algebra (f ≫ s.inl), f' : ↥A →ₐ[↥R] ↥(s.X) := {to_fun := s.inl.to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}, g' : ↥B →ₐ[↥R] ↥(s.X) := {to_fun := s.inr.to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _} in ⟨(algebra.tensor_product.product_map f' g').to_ring_hom, _⟩)
The trivial ring is the (strict) terminal object of CommRing
.
@[protected, instance]
theorem
CommRing.subsingleton_of_is_terminal
{X : CommRing}
(hX : category_theory.limits.is_terminal X) :
ℤ
is the initial object of CommRing
.
The product in CommRing
is the cartesian product. This is the binary fan.
Equations
- A.prod_fan B = category_theory.limits.binary_fan.mk (CommRing.of_hom (ring_hom.fst ↥A ↥B)) (CommRing.of_hom (ring_hom.snd ↥A ↥B))
@[simp]
The product in CommRing
is the cartesian product.
Equations
- A.prod_fan_is_limit B = {lift := λ (c : category_theory.limits.cone (category_theory.limits.pair A B)), ring_hom.prod (c.π.app {as := category_theory.limits.walking_pair.left}) (c.π.app {as := category_theory.limits.walking_pair.right}), fac' := _, uniq' := _}
The equalizer in CommRing
is the equalizer as sets. This is the equalizer fork.
Equations
The equalizer in CommRing
is the equalizer as sets.
Equations
- CommRing.equalizer_fork_is_limit f g = category_theory.limits.fork.is_limit.mk' (CommRing.equalizer_fork f g) (λ (s : category_theory.limits.fork f g), ⟨ring_hom.cod_restrict s.ι (ring_hom.eq_locus f g) _, _⟩)
@[protected, instance]