instRingColimitType — Mathlib

English

Given a diagram F: J ⥤ RingCat over a small category J, the ColimitType F carries a natural ring structure, i.e., the colimit exists and inherits ring operations from the diagram.

Русский

Для диаграммы F: J ⥤ RingCat над малой категорией J тип ColimitType F естественно оборудован структурой кольца, то есть колимит существует и порождается на диаграмме.

LaTeX

$$$\forall J\;[\text{SmallCategory } J]\; (F:J\to RingCat),\; \text{Ring}(\mathrm{ColimitType}(F))$$

Lean4

instance : Ring (ColimitType.{v} F) :=
  {
    ColimitType.AddGroupWithOne
      F with
    mul := Quot.map₂ Prequotient.mul Relation.mul_2 Relation.mul_1
    one_mul := fun x => Quot.inductionOn x fun _ => Quot.sound <| Relation.one_mul _
    mul_one := fun x => Quot.inductionOn x fun _ => Quot.sound <| Relation.mul_one _
    add_comm := fun x y => Quot.induction_on₂ x y fun _ _ => Quot.sound <| Relation.add_comm _ _
    mul_assoc := fun x y z =>
      Quot.induction_on₃ x y z fun x y z => by
        simp only [(· * ·)]
        exact Quot.sound (Relation.mul_assoc _ _ _)
    mul_zero := fun x => Quot.inductionOn x fun _ => Quot.sound <| Relation.mul_zero _
    zero_mul := fun x => Quot.inductionOn x fun _ => Quot.sound <| Relation.zero_mul _
    left_distrib := fun x y z =>
      Quot.induction_on₃ x y z fun x y z => by
        simp only [(· + ·), (· * ·), Add.add]
        exact Quot.sound (Relation.left_distrib _ _ _)
    right_distrib := fun x y z =>
      Quot.induction_on₃ x y z fun x y z => by
        simp only [(· + ·), (· * ·), Add.add]
        exact Quot.sound (Relation.right_distrib _ _ _) }

Похожие утверждения