Operations on fractional ideals

Two facts about Mathlib's FractionalIdeal.ringEquivOfRingEquiv, the transport of fractional ideals along a ring equivalence f : R ≃+* R' extended to fraction rings, and two facts about scaling a fractional ideal by a unit: the principal fractional ideal of a unit is a unit, and scaling by a unit is cancelled by scaling by its inverse.

Main results

• FractionalIdeal.canonicalEquiv_eq_ringEquivOfRingEquiv: the canonical equivalence between the fractional ideals of two fraction rings of R is transport along the identity.
• FractionalIdeal.ringEquivOfRingEquiv_coeIdeal: transport sends the fractional ideal of an ideal I to that of Ideal.map f I.
• FractionalIdeal.isUnit_spanSingleton: the principal fractional ideal of a unit is a unit.
• FractionalIdeal.spanSingleton_inv_mul_cancel_left: scaling by a unit and then by its inverse returns the fractional ideal.

theorem FractionalIdeal.canonicalEquiv_eq_ringEquivOfRingEquiv {R : Type u_1} [CommRing R] [IsDomain R] (K : Type u_3) (K' : Type u_4) [CommRing K] [CommRing K'] [Algebra R K] [Algebra R K'] [IsFractionRing R K] [IsFractionRing R K'] : canonicalEquiv (nonZeroDivisors R) K K' = ringEquivOfRingEquiv K K' (RingEquiv.refl R)

The canonical equivalence between the fractional ideals of two fraction fields of R is transport along the identity ring equivalence. This lets a change of fraction field and a transport along a ring equivalence be composed by FractionalIdeal.ringEquivOfRingEquiv_trans_apply.

@[simp]

theorem FractionalIdeal.ringEquivOfRingEquiv_coeIdeal {R : Type u_1} {R' : Type u_2} [CommRing R] [IsDomain R] [CommRing R'] [IsDomain R'] (K : Type u_3) (L : Type u_4) [CommRing K] [CommRing L] [Algebra R K] [Algebra R' L] [IsFractionRing R K] [IsFractionRing R' L] (f : R ≃+* R') (I : Ideal R) : (ringEquivOfRingEquiv K L f) ↑I = ↑(Ideal.map (↑f) I)

Transport of a coeIdeal along FractionalIdeal.ringEquivOfRingEquiv f is the coeIdeal of the pushforward ideal Ideal.map f. This is the fraction-field shadow of Ideal.map.

theorem FractionalIdeal.isUnit_spanSingleton {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] [IsLocalization S P] {x : P} (hx : IsUnit x) : IsUnit (spanSingleton S x)

The principal fractional ideal generated by a unit is a unit.

theorem FractionalIdeal.spanSingleton_inv_mul_cancel_left {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] [IsLocalization S P] (x : Pˣ) (I : FractionalIdeal S P) : spanSingleton S ↑x⁻¹ * (spanSingleton S ↑x * I) = I

Scaling a fractional ideal by a unit and then by its inverse returns the ideal.