English
Evaluation of logEmbeddingQuot on a representative coincides with logEmbedding.
Русский
Оценка logEmbeddingQuot на представителе совпадает с logEmbedding.
LaTeX
$$$\logEmbeddingQuot K (Additive.ofMul (QuotientGroup.mk x)) = \logEmbedding K (Additive.ofMul x)$$$
Lean4
/-- The linear equivalence between `(𝓞 K)ˣ ⧸ (torsion K)` as an additive `ℤ`-module and
`unitLattice` . -/
def logEmbeddingEquiv : Additive ((𝓞 K)ˣ ⧸ (torsion K)) ≃ₗ[ℤ] (unitLattice K) :=
LinearEquiv.ofBijective
((logEmbeddingQuot K).codRestrict (unitLattice K)
(Quotient.ind fun _ ↦ logEmbeddingQuot_apply K _ ▸ Submodule.mem_map_of_mem trivial)).toIntLinearMap
⟨fun _ _ ↦
by
rw [AddMonoidHom.coe_toIntLinearMap, AddMonoidHom.codRestrict_apply, AddMonoidHom.codRestrict_apply,
Subtype.mk.injEq]
apply logEmbeddingQuot_injective K, fun ⟨a, ⟨b, _, ha⟩⟩ ↦ ⟨⟦b⟧, by simpa using ha⟩⟩
