Compatibility of conjugation with integral representatives and with the scalar comparisons used in the definition of an ideal class.
theorem
CCDN.fractionalIdeal_conjugate_coeIdeal
{R : Type u_1}
{K : Type u_2}
[CommRing R]
[IsDedekindDomain R]
[Field K]
[Algebra R K]
[IsFractionRing R K]
(σ : R ≃+* R)
(I : Ideal R)
:
Applying a ring automorphism σ of R to the fractional ideal of an integral ideal I gives
the fractional ideal of the integral ideal I.map σ.
theorem
CCDN.integral_ideal_scalar_fractional_comparison
{R : Type u_1}
{K : Type u_2}
[CommRing R]
[IsDedekindDomain R]
[Field K]
[Algebra R K]
[IsFractionRing R K]
(σ : R ≃+* R)
(I : ↥(nonZeroDivisors (Ideal R)))
(x y : R)
(hx : x ≠ 0)
(hy : y ≠ 0)
(hxy : Ideal.span {x} * Ideal.map σ.toRingHom ↑I = Ideal.span {y} * ↑I)
:
(fractionalIdealUnitAction σ) ((FractionalIdeal.mk0 K) I) = (toPrincipalIdeal R K) (Units.mk0 ((algebraMap R K) y) ⋯ / Units.mk0 ((algebraMap R K) x) ⋯) * (FractionalIdeal.mk0 K) I
If (x) * σ(I) = (y) * I for nonzero x y : R, then the conjugate of the fractional ideal of
I under σ equals the principal fractional ideal of y / x times that of I.