English
The normalization map respects the pullback through idealSetEquivNorm for a fixed element a.
Русский
Нормализация согласуется с отображением через idealSetEquivNorm для фиксированного элемента a.
LaTeX
$$$\\operatorname{integerSetEquivNorm\\_apply\\_fst}(a) : \\operatorname{integerSet\\_equiv Norm}(a) = \\operatorname{absNorm}(I).$$$
Lean4
/-- For an integer `n`, The equivalence between the elements of `integerSet K` of norm `n`
and the product of the set of nonzero principal ideals of `K` of norm `n` and the torsion of `K`. -/
def integerSetEquivNorm (n : ℕ) :
{ a : integerSet K // mixedEmbedding.norm (a : mixedSpace K) = n } ≃
{ I : (Ideal (𝓞 K))⁰ // IsPrincipal (I : Ideal (𝓞 K)) ∧ absNorm (I : Ideal (𝓞 K)) = n } × (torsion K) :=
calc
_ ≃ { I : { I : (Ideal (𝓞 K))⁰ // IsPrincipal I.1 } × torsion K // absNorm (I.1 : Ideal (𝓞 K)) = n } :=
Equiv.subtypeEquiv (integerSetEquiv K) fun _ ↦ by
simp_rw [← intNorm_coe, intNorm, Nat.cast_inj, integerSetEquiv_apply_fst, absNorm_span_singleton]
_ ≃ { I : { I : (Ideal (𝓞 K))⁰ // IsPrincipal I.1 } // absNorm (I.1 : Ideal (𝓞 K)) = n } × torsion K :=
Equiv.prodSubtypeFstEquivSubtypeProd (p := fun I : { I : (Ideal (𝓞 K))⁰ // IsPrincipal I.1 } ↦
absNorm (I : Ideal (𝓞 K)) = n)
_ ≃ { I : (Ideal (𝓞 K))⁰ // IsPrincipal (I : Ideal (𝓞 K)) ∧ absNorm (I : Ideal (𝓞 K)) = n } × (torsion K) :=
Equiv.prodCongrLeft fun _ ↦
(Equiv.subtypeSubtypeEquivSubtypeInter (fun I : (Ideal (𝓞 K))⁰ ↦ IsPrincipal I.1) (fun I ↦ absNorm I.1 = n))
