Functoriality of class groups under ring equivalences

Mathlib defines ClassGroup.mulEquiv f, the multiplicative equivalence on ideal class groups induced by a ring equivalence f : R ≃+* S. This file supplies its basic functorial API: the induced map respects identity, composition, and inverses, and computes on the class of a unit fractional ideal.

This is a prerequisite for the genus-field layer of the multiquadratic roadmap. For a quadratic field, conjugation is a ring automorphism of its ring of integers; the roadmap's proof that conjugation acts on the class group by inversion first needs to treat that action functorially and compute it on ideal classes.

Main results

• ClassGroup.mulEquiv_mk_fractionRing: the simp-usable computation of the induced equivalence on the class of a unit fractional ideal over the canonical fraction field.
• ClassGroup.mulEquiv_mk: the same computation over arbitrary fraction fields, as an rw-form with the target fraction field explicit.
• ClassGroup.mulEquiv_refl: the identity ring equivalence induces the identity on class groups.
• ClassGroup.mulEquiv_trans: induced equivalences respect composition.
• ClassGroup.mulEquiv_symm: the inverse induced equivalence comes from the inverse ring equivalence.
• ClassGroup.mulEquivHom: the induced action bundled as a monoid homomorphism (R ≃+* R) →* MulAut (ClassGroup R).
• ClassGroup.mulEquiv_involutive: an involutive ring equivalence acts involutively on the class group.
• ClassGroup.mulEquiv_mk0: the induced class-group equivalence sends the class ClassGroup.mk0 I of a nonzero ideal to the class of its pushforward ideal Ideal.map f I.
• ClassGroup.mulEquiv_apply_eq_inv_of_isPrincipal_mul_map: if I · (Ideal.map f I) is principal for every nonzero ideal, the induced class-group map is inversion C ↦ C⁻¹.

@[simp]

theorem ClassGroup.mulEquiv_mk_fractionRing {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsDomain R] [IsDomain S] (f : R ≃+* S) (I : (FractionalIdeal (nonZeroDivisors R) (FractionRing R))ˣ) : (mulEquiv f) ((mk (FractionRing R)) I) = (mk (FractionRing S)) ((Units.mapEquiv ↑(FractionalIdeal.ringEquivOfRingEquiv (FractionRing R) (FractionRing S) f)) I)

ClassGroup.mulEquiv f sends the class of a unit fractional ideal I to the class of its image under FractionalIdeal.ringEquivOfRingEquiv f. This is the characteristic computation of the induced map on ideal classes; the functorial laws below are corollaries. Its fully-determined left-hand side makes it the simp-usable form; mulEquiv_mk is the general rw-form over arbitrary fraction fields.

theorem ClassGroup.mulEquiv_mk {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsDomain R] [IsDomain S] {K : Type u_4} (L : Type u_5) [Field K] [Field L] [Algebra R K] [Algebra S L] [IsFractionRing R K] [IsFractionRing S L] (f : R ≃+* S) (I : (FractionalIdeal (nonZeroDivisors R) K)ˣ) : (mulEquiv f) ((mk K) I) = (mk L) ((Units.mapEquiv ↑(FractionalIdeal.ringEquivOfRingEquiv K L f)) I)

ClassGroup.mulEquiv f sends the class of a unit fractional ideal I to the class of its image under FractionalIdeal.ringEquivOfRingEquiv f. This is independent of the chosen fraction fields.

@[simp]

theorem ClassGroup.mulEquiv_refl {R : Type u_1} [CommRing R] [IsDomain R] : mulEquiv (RingEquiv.refl R) = MulEquiv.refl (ClassGroup R)

The identity ring equivalence induces the identity class-group equivalence.

@[simp]

theorem ClassGroup.mulEquiv_trans {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] [IsDomain R] [IsDomain S] [IsDomain T] (f : R ≃+* S) (g : S ≃+* T) : mulEquiv (f.trans g) = (mulEquiv f).trans (mulEquiv g)

Composition of ring equivalences is carried to composition of the induced class-group equivalences.

theorem ClassGroup.mulEquiv_trans_apply {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] [IsDomain R] [IsDomain S] [IsDomain T] (f : R ≃+* S) (g : S ≃+* T) (x : ClassGroup R) : (mulEquiv (f.trans g)) x = (mulEquiv g) ((mulEquiv f) x)

Pointwise form of ClassGroup.mulEquiv_trans. This is not a simp lemma because ClassGroup.mulEquiv_apply already rewrites its left-hand side.

theorem ClassGroup.mulEquiv_refl_apply {R : Type u_1} [CommRing R] [IsDomain R] (x : ClassGroup R) : (mulEquiv (RingEquiv.refl R)) x = x

Pointwise form of ClassGroup.mulEquiv_refl. This is not a simp lemma because ClassGroup.mulEquiv_refl already proves the bundled normal form.

@[simp]

theorem ClassGroup.mulEquiv_symm {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsDomain R] [IsDomain S] (f : R ≃+* S) : (mulEquiv f).symm = mulEquiv f.symm

The inverse of the class-group equivalence induced by f is induced by f.symm.

theorem ClassGroup.mulEquiv_symm_apply' {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsDomain R] [IsDomain S] (f : R ≃+* S) (x : ClassGroup S) : (mulEquiv f).symm x = (mulEquiv f.symm) x

Pointwise form of ClassGroup.mulEquiv_symm. This is not a simp lemma because ClassGroup.mulEquiv_apply already rewrites its left-hand side.

noncomputable def ClassGroup.mulEquivHom {R : Type u_1} [CommRing R] [IsDomain R] : (R ≃+* R) →* MulAut (ClassGroup R)

The action of ring automorphisms of R on ClassGroup R, bundled as a monoid homomorphism (R ≃+* R) →* MulAut (ClassGroup R). This is the object the roadmap's Galois action on ideal classes transports along; it is the class-group analogue of IsFractionRing.ringEquivOfRingEquivHom.

Equations

• ClassGroup.mulEquivHom = { toFun := ClassGroup.mulEquiv, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem ClassGroup.mulEquivHom_apply {R : Type u_1} [CommRing R] [IsDomain R] (f : R ≃+* R) : mulEquivHom f = mulEquiv f

ClassGroup.mulEquivHom acts as ClassGroup.mulEquiv on each ring automorphism.

theorem ClassGroup.mulEquiv_involutive {R : Type u_1} [CommRing R] [IsDomain R] {f : R ≃+* R} (hf : Function.Involutive ⇑f) : Function.Involutive ⇑(mulEquiv f)

An involutive ring equivalence induces an involution on the class group. This is the form used for quadratic conjugation; it is the pointwise specialization of ClassGroup.mulEquivHom at an order-two automorphism.

@[simp]

theorem ClassGroup.mulEquiv_mk0 {R : Type u_1} {R' : Type u_2} [CommRing R] [CommRing R'] [IsDedekindDomain R] [IsDedekindDomain R'] (f : R ≃+* R') (I : ↥(nonZeroDivisors (Ideal R))) : (mulEquiv f) (mk0 I) = mk0 ⟨Ideal.map ↑f ↑I, ⋯⟩

The class-group map induced by a ring isomorphism, on ideal classes. For a ring isomorphism f : R ≃+* R' of Dedekind domains, ClassGroup.mulEquiv f sends the class of a nonzero ideal I to the class of its pushforward Ideal.map f I. This is the bridge between the abstract functorial action ClassGroup.mulEquiv and the concrete pushforward of ideals.

theorem ClassGroup.mulEquiv_apply_eq_inv_of_isPrincipal_mul_map {R : Type u_1} [CommRing R] [IsDedekindDomain R] {f : R ≃+* R} (hf : ∀ (I : ↥(nonZeroDivisors (Ideal R))), Submodule.IsPrincipal (↑I * Ideal.map ↑f ↑I)) (C : ClassGroup R) : (mulEquiv f) C = C⁻¹

Inversion criterion for the class-group action. If a ring automorphism f : R ≃+* R of a Dedekind domain makes I · (Ideal.map f I) principal for every nonzero ideal I, then the induced map on the class group is inversion: ClassGroup.mulEquiv f C = C⁻¹.