English
There is an induction principle on the class group: to prove a property for all classes, it suffices to prove it on representatives mk I for all unit fractional ideals I.
Русский
Существует принцип индукции по группе классов: чтобы доказать свойство для всех классов, достаточно доказать его на представителях mk I для всех единичных дробных идеалов I.
LaTeX
$$$\text{Induction: let }P: \mathrm{ClassGroup}(R) \to \mathrm{Prop}.\; (\forall I\;P(\mathrm{ClassGroup.mk}(I)) ) \Rightarrow \forall x\in \mathrm{ClassGroup}(R),\; P(x).$$$
Lean4
/-- Induction principle for the class group: to show something holds for all `x : ClassGroup R`,
we can choose a fraction field `K` and show it holds for the equivalence class of each
`I : FractionalIdeal R⁰ K`. -/
@[elab_as_elim]
theorem induction {P : ClassGroup R → Prop} (h : ∀ I : (FractionalIdeal R⁰ K)ˣ, P (ClassGroup.mk I))
(x : ClassGroup R) : P x :=
QuotientGroup.induction_on x fun I =>
by
have :
I =
(Units.mapEquiv (canonicalEquiv R⁰ K (FractionRing R)).toMulEquiv)
(Units.mapEquiv (canonicalEquiv R⁰ (FractionRing R) K).toMulEquiv I) :=
by simp [← Units.val_inj]
rw [congr_arg (QuotientGroup.mk (s := (toPrincipalIdeal R (FractionRing R)).range)) this]
exact h _
