English
The equivalence between integerSetNorm and idealNorm preserves the respective norms under the fundamental cone mapping.
Русский
Эквивалентность между нормой integerSet и нормой идеала сохраняет значения норм через отображение фундаментального конуса.
LaTeX
$$$\\operatorname{intNorm\_norm\_eq}=\\operatorname{norm\_preserve}$$$
Lean4
/-- For an integer `n`, The equivalence between the elements of `idealSet K` of norm `n` and
the product of the set of nonzero principal ideals of `K` divisible by `J` of norm `n` and the
torsion of `K`. -/
def idealSetEquivNorm (n : ℕ) :
{ a : idealSet K J // mixedEmbedding.norm (a : mixedSpace K) = n } ≃
{ I : (Ideal (𝓞 K))⁰ // (J : Ideal (𝓞 K)) ∣ I ∧ IsPrincipal (I : Ideal (𝓞 K)) ∧ absNorm (I : Ideal (𝓞 K)) = n } ×
(torsion K) :=
calc
_ ≃ { a : { a : integerSet K // (preimageOfMemIntegerSet a).1 ∈ J.1 } // mixedEmbedding.norm a.1.1 = n } :=
by
convert (Equiv.subtypeEquivOfSubtype (idealSetEquiv K J).symm).symm using 3
rw [idealSetEquiv_symm_apply]
_ ≃ { a : integerSet K // (preimageOfMemIntegerSet a).1 ∈ J.1 ∧ mixedEmbedding.norm a.1 = n } :=
(Equiv.subtypeSubtypeEquivSubtypeInter (fun a : integerSet K ↦ (preimageOfMemIntegerSet a).1 ∈ J.1)
(fun a ↦ mixedEmbedding.norm a.1 = n))
_ ≃ { a : { a : integerSet K // mixedEmbedding.norm a.1 = n } // (preimageOfMemIntegerSet a.1).1 ∈ J.1 } :=
((Equiv.subtypeSubtypeEquivSubtypeInter (fun a : integerSet K ↦ mixedEmbedding.norm a.1 = n)
(fun a ↦ (preimageOfMemIntegerSet a).1 ∈ J.1)).trans
(Equiv.subtypeEquivRight (fun _ ↦ by simp [and_comm]))).symm
_ ≃ { I : { I : (Ideal (𝓞 K))⁰ // IsPrincipal I.1 ∧ absNorm I.1 = n } × (torsion K) // J.1 ∣ I.1.1 } :=
by
convert Equiv.subtypeEquivOfSubtype (p := fun I ↦ J.1 ∣ I.1) (integerSetEquivNorm K n)
rw [integerSetEquivNorm_apply_fst, dvd_span_singleton]
_ ≃ { I : { I : (Ideal (𝓞 K))⁰ // IsPrincipal I.1 ∧ absNorm I.1 = n } // J.1 ∣ I.1 } × (torsion K) :=
Equiv.prodSubtypeFstEquivSubtypeProd (p := fun I : { I : (Ideal (𝓞 K))⁰ // IsPrincipal I.1 ∧ absNorm I.1 = n } ↦
J.1 ∣ I.1)
_ ≃ { I : (Ideal (𝓞 K))⁰ // (IsPrincipal I.1 ∧ absNorm I.1 = n) ∧ J.1 ∣ I.1 } × (torsion K) :=
(Equiv.prodCongrLeft fun _ ↦
(Equiv.subtypeSubtypeEquivSubtypeInter (fun I : (Ideal (𝓞 K))⁰ ↦ IsPrincipal I.1 ∧ absNorm I.1 = n)
(fun I ↦ J.1 ∣ I.1)))
_ ≃ { I : (Ideal (𝓞 K))⁰ // J.1 ∣ I.1 ∧ IsPrincipal I.1 ∧ absNorm I.1 = n } × (Units.torsion K) :=
Equiv.prodCongrLeft fun _ ↦ Equiv.subtypeEquivRight fun _ ↦ by rw [and_comm]
