An invariant fractional ideal has an invariant integral representative in the same ideal class. Multiplying a denominator by its conjugate makes the denominator clearing compatible with the involution.

theorem CCDN.exists_invariant_integral_ideal_representative {R : Type u_1} {K : Type u_2} [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] (σ : R ≃+* R) (hσ : Function.Involutive ⇑σ) (J : (FractionalIdeal (nonZeroDivisors R) K)ˣ) (hJ : (fractionalIdealUnitAction σ) J = J) : ∃ (I : ↥(nonZeroDivisors (Ideal R))), Ideal.map σ.toRingHom ↑I = ↑I ∧ ClassGroup.mk0 I = (ClassGroup.mk K) J

For an involutive ring automorphism σ of R, every σ-invariant invertible fractional ideal J has a σ-invariant nonzero integral ideal I in the same ideal class.