to_mulShift_inj_of_isPrimitive — Mathlib

English

If ψ is primitive, the map a ↦ mulShift ψ a is injective on the underlying ring.

Русский

Если ψ примитивна, отображение a ↦ mulShift ψ a инъективно на рёберном кольце.

LaTeX

$$Function.Injective(ψ.mulShift)$$

Lean4

/-- The map associating to `a : R` the multiplicative shift of `ψ` by `a`
is injective when `ψ` is primitive. -/
theorem to_mulShift_inj_of_isPrimitive {ψ : AddChar R R'} (hψ : IsPrimitive ψ) : Function.Injective ψ.mulShift :=
  by
  intro a b h
  apply_fun fun x => x * mulShift ψ (-b) at h
  simp only [mulShift_mul, mulShift_zero, add_neg_cancel] at h
  simpa [← sub_eq_add_neg, sub_eq_zero] using
    (hψ · h)
      -- `AddCommGroup.equiv_direct_sum_zmod_of_fintype`
      -- gives the structure theorem for finite abelian groups.
      -- This could be used to show that the map above is a bijection.
      -- We leave this for a later occasion.

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