Compatibility of class-group automorphism actions with integral-ideal representatives.

theorem CCDN.fractionalIdeal_ringEquiv_coeIdeal {A : Type u_1} {B : Type u_2} [CommRing A] [IsDomain A] [CommRing B] [IsDomain B] (K : Type u_3) (L : Type u_4) [CommRing K] [CommRing L] [Algebra A K] [Algebra B L] [IsFractionRing A K] [IsFractionRing B L] (g : A ≃+* B) (I : Ideal A) : (FractionalIdeal.ringEquivOfRingEquiv K L g) ↑I = ↑(Ideal.map g I)

Fractional-ideal transport agrees with the map of integral ideals.

theorem CCDN.classGroup_mulEquiv_mk0 {R : Type u_3} {S : Type u_4} [CommRing R] [CommRing S] [IsDedekindDomain R] [IsDedekindDomain S] (g : R ≃+* S) (I : ↥(nonZeroDivisors (Ideal R))) : (ClassGroup.mulEquiv g) (ClassGroup.mk0 I) = ClassGroup.mk0 ⟨Ideal.map g ↑I, ⋯⟩

The class-group action carries an integral ideal to its mapped ideal class.

theorem CCDN.classGroup_mulEquiv_involutive {R : Type u_3} [CommRing R] [IsDomain R] (σ : R ≃+* R) (hσ : Function.Involutive ⇑σ) : Function.Involutive ⇑(ClassGroup.mulEquiv σ)

An involutive ring automorphism acts involutively on the class group.