logEmbeddingQuot — Mathlib

English

There is a natural Z-linear bijection between ((𝓞 K)ˣ / torsion K) and unitLattice K.

Русский

Существует естественное Z-линейное биективное соответствие между ((𝓞 K)ˣ / torsion K) и unitLattice K.

LaTeX

$$$\logEmbeddingEquiv K : ((\mathcal O_K)^{\times})/(torsion\ K) \simeq_{\mathbb{Z}} unitLattice(K)$$$

Lean4

/-- The map obtained by quotienting by the kernel of `logEmbedding`. -/
def logEmbeddingQuot : Additive ((𝓞 K)ˣ ⧸ (torsion K)) →+ logSpace K :=
  MonoidHom.toAdditiveLeft <|
    (QuotientGroup.kerLift (AddMonoidHom.toMultiplicativeRight (logEmbedding K))).comp
      (QuotientGroup.quotientMulEquivOfEq
          (by
            ext
            rw [MonoidHom.mem_ker, AddMonoidHom.toMultiplicativeRight_apply_apply, ofAdd_eq_one, ←
              logEmbedding_eq_zero_iff])).toMonoidHom

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