English
There is a norm-compatible chain of isomorphisms equating principal-ideal data with norm data across the mixed embedding.
Русский
Существует цепь изоморфизмов, совместимая по норме, между данными главных идеалов и данными порезанных норм.
LaTeX
$$$\\operatorname{idealSetEquivNorm}(K,J,n) : {I\\;|\\; (J∣I) ∧ IsPrincipal(I) ∧ absNorm(I)=n} \\times \\mathrm{torsion}(K) \\simeq {a:\\text{idealSet }K\\,J\\;|\\; \\operatorname{mixedEmbedding.norm}(a)=n}$$$
Lean4
/-- The map `idealSetMap` is actually an equiv between `idealSet K J` and the elements of
`integerSet K` whose preimage lies in `J`. -/
def idealSetEquiv : idealSet K J ≃ {a : integerSet K | (preimageOfMemIntegerSet a : 𝓞 K) ∈ (J : Set (𝓞 K))} :=
Equiv.ofBijective (fun a ↦ ⟨idealSetMap K J a, preimage_of_IdealSetMap K J a⟩)
⟨fun _ _ h ↦
(by
simp_rw [Subtype.ext_iff, idealSetMap_apply] at h
rwa [Subtype.ext_iff]),
fun ⟨a, ha₂⟩ ↦
⟨⟨a.val, mem_idealSet.mpr ⟨a.prop.1, ⟨preimageOfMemIntegerSet a, ha₂, mixedEmbedding_preimageOfMemIntegerSet a⟩⟩⟩,
rfl⟩⟩
