English
There is a canonical isomorphism between the class group and the quotient of the unit group of fractional ideals by the principal-ideals range.
Русский
Существует каноническое изоморфизм между класс-группой и фактор-группой единичных дробных идеалов по диапазону принципиальных идеалов.
LaTeX
$$$\mathrm{ClassGroup.equiv} : \mathrm{ClassGroup}(R) \cong^* \big(\mathrm{Units}(\mathrm{FractionalIdeal}(R^{0},K))\big) / (\mathrm{toPrincipalIdeal}(R,K)).\mathrm{range}$$$
Lean4
/-- The definition of the class group does not depend on the choice of field of fractions. -/
noncomputable def equiv : ClassGroup R ≃* (FractionalIdeal R⁰ K)ˣ ⧸ (toPrincipalIdeal R K).range :=
by
haveI :
Subgroup.map (Units.mapEquiv (canonicalEquiv R⁰ (FractionRing R) K).toMulEquiv).toMonoidHom
(toPrincipalIdeal R (FractionRing R)).range =
(toPrincipalIdeal R K).range :=
by
ext I
simp only [Subgroup.mem_map, mem_principal_ideals_iff]
constructor
· rintro ⟨I, ⟨x, hx⟩, rfl⟩
refine ⟨FractionRing.algEquiv R K x, ?_⟩
simp only [RingEquiv.toMulEquiv_eq_coe, MulEquiv.coe_toMonoidHom, coe_mapEquiv, ← hx, RingEquiv.coe_toMulEquiv,
canonicalEquiv_spanSingleton]
rfl
· rintro ⟨x, hx⟩
refine
⟨Units.mapEquiv (canonicalEquiv R⁰ K (FractionRing R)).toMulEquiv I, ⟨(FractionRing.algEquiv R K).symm x, ?_⟩,
Units.ext ?_⟩
· simp only [RingEquiv.toMulEquiv_eq_coe, coe_mapEquiv, ← hx, RingEquiv.coe_toMulEquiv,
canonicalEquiv_spanSingleton]
rfl
·
simp only [RingEquiv.toMulEquiv_eq_coe, MulEquiv.coe_toMonoidHom, coe_mapEquiv, RingEquiv.coe_toMulEquiv,
canonicalEquiv_canonicalEquiv, canonicalEquiv_self, RingEquiv.refl_apply]
exact
@QuotientGroup.congr (FractionalIdeal R⁰ (FractionRing R))ˣ _ (FractionalIdeal R⁰ K)ˣ _
(toPrincipalIdeal R (FractionRing R)).range (toPrincipalIdeal R K).range _ _
(Units.mapEquiv (FractionalIdeal.canonicalEquiv R⁰ (FractionRing R) K).toMulEquiv) this
