monoid — Mathlib

English

The trivial square-zero extension tsze_R M carries a monoid structure compatible with the base ring/action data; i.e., it forms a well-defined monoid under multiplication.

Русский

У тривиального квадратно-ноль расширения tsze_R M имеется согласованная моноидальная структура, совместимая с данными о кольце/действии; то есть образуется моноид по умножению.

LaTeX

$$$ tsze_R M \\text{ is a monoid}$$$

Lean4

instance monoid [Monoid R] [AddMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] :
    Monoid (tsze R M) :=
  {
    TrivSqZeroExt.mulOneClass with
    mul_assoc := fun x y z =>
      ext (mul_assoc x.1 y.1 z.1) <|
        show
          (x.1 * y.1) •> z.2 + (x.1 •> y.2 + x.2 <• y.1) <• z.1 = x.1 •> (y.1 •> z.2 + y.2 <• z.1) + x.2 <• (y.1 * z.1)
          by simp_rw [smul_add, ← mul_smul, add_assoc, smul_comm, op_mul]
    npow := fun n x => x ^ n
    npow_zero := fun x => ext (pow_zero x.fst) (by simp [snd_pow_eq_sum])
    npow_succ := fun n x =>
      ext (pow_succ _ _)
        (by
          simp_rw [snd_mul, snd_pow_eq_sum, Nat.pred_succ]
          cases n
          · simp [List.range_succ]
          rw [List.sum_range_succ']
          simp only [pow_zero, op_one, Nat.sub_zero, one_smul, Nat.succ_sub_succ_eq_sub, fst_pow, Nat.pred_succ,
            List.smul_sum, List.map_map, Function.comp_def]
          simp_rw [← smul_comm (_ : R) (_ : Rᵐᵒᵖ), smul_smul, pow_succ]
          rfl) }

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