English
For a natural n, the norm on the ideal side corresponds to the norm on integerSet side via the integerSetEquivNorm equivalence.
Русский
Для данного n соответствие норм между сторонами идеалов и целевых множеств через эквивалентность integerSetEquivNorm сохраняется.
LaTeX
$$$\\operatorname{integerSetEquivNorm} : {\\,a\\;|\\; \\operatorname{mixedEmbedding.norm}(a) = n\\} \\simeq {\\,I\\;|\\; (J ∣ I) \\wedge \\operatorname{absNorm}(I)=n\\}$$$
Lean4
/-- The equivalence between `integerSet K` and the product of the set of nonzero principal
ideals of `K` and the torsion of `K`. -/
def integerSetEquiv : integerSet K ≃ { I : (Ideal (𝓞 K))⁰ // IsPrincipal I.val } × torsion K :=
(MulAction.selfEquivSigmaOrbitsQuotientStabilizer (torsion K) (integerSet K)).trans
((Equiv.sigmaEquivProdOfEquiv
(by
intro _
simp_rw [integerSetTorsionSMul_stabilizer]
exact QuotientGroup.quotientBot.toEquiv)).trans
(Equiv.prodCongrLeft
(fun _ ↦ (integerSetQuotEquivAssociates K).trans (Ideal.associatesNonZeroDivisorsEquivIsPrincipal (𝓞 K)))))
