English
The map integerSetToAssociates is surjective onto Associates((𝓞 K)⁰): every associate class arises from some a ∈ integerSet(K).
Русский
Отображение integerSetToAssociates сюръективно на Associates((𝓞 K)⁰): каждый ассоциативный класс появляется как образ некоторого a из integerSet(K).
LaTeX
$$$\\operatorname{integerSetToAssociates}\\;K:\\;\\text{Surjective}(K).$$$
Lean4
theorem integerSetToAssociates_surjective : Function.Surjective (integerSetToAssociates K) :=
by
rintro ⟨x⟩
obtain ⟨u, hu⟩ : ∃ u : (𝓞 K)ˣ, u • mixedEmbedding K (x : 𝓞 K) ∈ integerSet K :=
by
refine exists_unitSMul_mem_integerSet ?_ ⟨(x : 𝓞 K), Set.mem_range_self _, rfl⟩
exact (map_ne_zero _).mpr <| RingOfIntegers.coe_ne_zero_iff.mpr (nonZeroDivisors.coe_ne_zero _)
refine ⟨⟨u • mixedEmbedding K (x : 𝓞 K), hu⟩, Quotient.sound ⟨unitsNonZeroDivisorsEquiv.symm u⁻¹, ?_⟩⟩
simp_rw [Subtype.ext_iff, RingOfIntegers.ext_iff, ← (mixedEmbedding_injective K).eq_iff, Submonoid.coe_mul, map_mul,
mixedEmbedding_preimageOfMemIntegerSet, unitSMul_smul, ← map_mul, mul_comm, map_inv,
val_inv_unitsNonZeroDivisorsEquiv_symm_apply_coe, Units.mul_inv_cancel_right]
