A fractional ideal with norm-one scalar comparison to its conjugate can be replaced in its ideal class by an invariant fractional ideal. The norm-one hypothesis isolates the unit obstruction rather than discarding it.

noncomputable def CCDN.fractionalIdealUnitAction {R : Type u_1} {K : Type u_2} [CommRing R] [IsDomain R] [Field K] [Algebra R K] [IsFractionRing R K] (σ : R ≃+* R) : (FractionalIdeal (nonZeroDivisors R) K)ˣ →* (FractionalIdeal (nonZeroDivisors R) K)ˣ

Conjugation of invertible fractional ideals by a ring automorphism.

Equations

• CCDN.fractionalIdealUnitAction σ = Units.map (FractionalIdeal.ringEquivOfRingEquiv K K σ).toMonoidHom

theorem CCDN.fractionalIdealUnitAction_principal {R : Type u_1} {K : Type u_2} [CommRing R] [IsDomain R] [Field K] [Algebra R K] [IsFractionRing R K] (σ : R ≃+* R) (b : Kˣ) : (fractionalIdealUnitAction σ) ((toPrincipalIdeal R K) b) = (toPrincipalIdeal R K) ((Units.map (IsFractionRing.ringEquivOfRingEquiv σ).toMonoidHom) b)

Conjugating the principal fractional ideal generated by b by σ gives the principal fractional ideal generated by the image of b under the induced automorphism of K.

theorem CCDN.classGroup_mk_principal {R : Type u_1} {K : Type u_2} [CommRing R] [IsDomain R] [Field K] [Algebra R K] [IsFractionRing R K] (b : Kˣ) : (ClassGroup.mk K) ((toPrincipalIdeal R K) b) = 1

The class of a principal fractional ideal is trivial.