torsionMapQuot — Mathlib

English

If absNorm(I) ≠ 1 and gcd(absNorm(I), torsionOrder(K)) = 1, then the torsion map quotient I → 𝓞K/I is injective on units (torsion of K).

Русский

Если absNorm(I) ≠ 1 и gcd(absNorm(I), torsionOrder(K)) = 1, то отображение torsionMapQuot инъективно на единицах.

LaTeX

$$If $|\\mathrm{absNorm}(I)| \\neq 1$ and $\\gcd(|\\mathrm{absNorm}(I)|, \\mathrm{torsionOrder}(K)) = 1$, then $\\mathrm{torsionMapQuot}$ is injective on the torsion subgroup.$$

Lean4

/-- For `I` an integral ideal of `K`, the group morphism from the torsion of `K` to `(𝓞 K ⧸ I)ˣ`.
-/
def torsionMapQuot : (Units.torsion K) →* ((𝓞 K) ⧸ I)ˣ :=
  (Units.map (Ideal.Quotient.mk I).toMonoidHom).restrict (torsion K)

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