English
Equality of integerSetToAssociates images corresponds to the existence of a torsion factor relating the representatives in the fund Cone.
Русский
Равенство образов через integerSetToAssociates эквивалентно существованию множителя-торов, связывающего представителя в фундаментальном конусе.
LaTeX
$$$\\operatorname{integerSetToAssociates}\\;K\\;a = \\operatorname{integerSetToAssociates}\\;K\\;b \\iff \\exists \\zeta:\\operatorname{torsion}K, \\; \\zeta\\cdot a = b.$$$
Lean4
/-- The equivalence between `integerSet K` modulo `torsion K` and `Associates (𝓞 K)⁰`. -/
def integerSetQuotEquivAssociates : Quotient (MulAction.orbitRel (torsion K) (integerSet K)) ≃ Associates (𝓞 K)⁰ :=
Equiv.ofBijective
(Quotient.lift (integerSetToAssociates K) fun _ _ h ↦ ((integerSetToAssociates_eq_iff _ _).mpr h).symm)
⟨by
convert Setoid.ker_lift_injective (integerSetToAssociates K)
all_goals
· ext a b
rw [Setoid.ker_def, eq_comm, integerSetToAssociates_eq_iff b a, MulAction.orbitRel_apply,
MulAction.mem_orbit_iff],
(Quot.surjective_lift _).mpr (integerSetToAssociates_surjective K)⟩
