English
The value of the equivalence on mk I is given by the quotient image of I under canonical equivalences from fractional ideals.
Русский
Значение отображения эквивалентности на mk I задаётся образом в фактор-группе под каноническими эквивалентностями дробных идеалов.
LaTeX
$$$\mathrm{ClassGroup.equiv}(K')(\mathrm{ClassGroup.mk}(I)) = \mathrm{QuotientGroup.mk'} _ (\mathrm{Units.mapEquiv}(\uparrow\mathrm{(FractionalIdeal.canonicalEquiv)}(R^{0},K,K'))(I)).$$$
Lean4
@[simp]
theorem equiv_mk (K' : Type*) [Field K'] [Algebra R K'] [IsFractionRing R K'] (I : (FractionalIdeal R⁰ K)ˣ) :
ClassGroup.equiv K' (ClassGroup.mk I) =
QuotientGroup.mk' _ (Units.mapEquiv (↑(FractionalIdeal.canonicalEquiv R⁰ K K')) I) :=
by
-- `simp` can't apply `ClassGroup.mk_def` and `rw` can't unfold `ClassGroup`.
rw [ClassGroup.equiv, ClassGroup.mk_def]
simp only [ClassGroup, QuotientGroup.congr_mk']
congr
rw [← Units.val_inj, Units.coe_mapEquiv, Units.coe_mapEquiv, Units.coe_map]
exact FractionalIdeal.canonicalEquiv_canonicalEquiv _ _ _ _ _
