Extension of fractional ideals

This file defines the extension of a fractional ideal along a ring homomorphism.

Main definitions

• FractionalIdeal.extended: Let A and B be commutative rings with respective localizations IsLocalization M K and IsLocalization N L. Let f : A →+* B be a ring homomorphism with hf : M ≤ Submonoid.comap f N. If I : FractionalIdeal M K, then the extension of I along f is extended L hf I : FractionalIdeal N L.
• FractionalIdeal.extendedHom': The ring homomorphism version of FractionalIdeal.extended.
• FractionalIdeal.extendedHom: For A ⊆ B an extension of domains, the ring homomorphism that sends a fractional ideal of A to a fractional ideal of B.

Main results

• FractionalIdeal.extendedHom_injective: the map FractionalIdeal.extendedHom is injective.
• Ideal.map_algebraMap_injective: For A ⊆ B an extension of Dedekind domains, the map that sends an ideal I of A to I·B is injective.

Tags

fractional ideal, fractional ideals, extended, extension

def FractionalIdeal.extended {A : Type u_1} [CommRing A] {B : Type u_2} [CommRing B] {f : A →+* B} {K : Type u_3} {M : Submonoid A} [CommRing K] [Algebra A K] [IsLocalization M K] (L : Type u_4) {N : Submonoid B} [CommRing L] [Algebra B L] [IsLocalization N L] (hf : M ≤ Submonoid.comap f N) (I : FractionalIdeal M K) : FractionalIdeal N L

Given commutative rings A and B with respective localizations IsLocalization M K and IsLocalization N L, and a ring homomorphism f : A →+* B satisfying M ≤ Submonoid.comap f N, a fractional ideal I of A can be extended along f to a fractional ideal of B.

Equations

• FractionalIdeal.extended L hf I = ⟨Submodule.span B (⇑(IsLocalization.map L f hf) '' ↑I), ⋯⟩

theorem FractionalIdeal.mem_extended_iff {A : Type u_1} [CommRing A] {B : Type u_2} [CommRing B] {f : A →+* B} {K : Type u_3} {M : Submonoid A} [CommRing K] [Algebra A K] [IsLocalization M K] (L : Type u_4) {N : Submonoid B} [CommRing L] [Algebra B L] [IsLocalization N L] (hf : M ≤ Submonoid.comap f N) (I : FractionalIdeal M K) (x : L) : x ∈ extended L hf I ↔ x ∈ Submodule.span B (⇑(IsLocalization.map L f hf) '' ↑I)

@[simp]

theorem FractionalIdeal.coe_extended_eq_span {A : Type u_1} [CommRing A] {B : Type u_2} [CommRing B] {f : A →+* B} {K : Type u_3} {M : Submonoid A} [CommRing K] [Algebra A K] [IsLocalization M K] (L : Type u_4) {N : Submonoid B} [CommRing L] [Algebra B L] [IsLocalization N L] (hf : M ≤ Submonoid.comap f N) (I : FractionalIdeal M K) : ↑(extended L hf I) = Submodule.span B (⇑(IsLocalization.map L f hf) '' ↑I)

@[simp]

theorem FractionalIdeal.extended_zero {A : Type u_1} [CommRing A] {B : Type u_2} [CommRing B] {f : A →+* B} {K : Type u_3} {M : Submonoid A} [CommRing K] [Algebra A K] [IsLocalization M K] (L : Type u_4) {N : Submonoid B} [CommRing L] [Algebra B L] [IsLocalization N L] (hf : M ≤ Submonoid.comap f N) : extended L hf 0 = 0

theorem FractionalIdeal.extended_ne_zero {A : Type u_1} [CommRing A] {B : Type u_2} [CommRing B] {f : A →+* B} {K : Type u_3} {M : Submonoid A} [CommRing K] [Algebra A K] [IsLocalization M K] (L : Type u_4) {N : Submonoid B} [CommRing L] [Algebra B L] [IsLocalization N L] (hf : M ≤ Submonoid.comap f N) {I : FractionalIdeal M K} [IsDomain B] (hf' : Function.Injective ⇑f) (hI : I ≠ 0) (hN : 0 ∉ N) : extended L hf I ≠ 0

@[simp]

theorem FractionalIdeal.extended_eq_zero_iff {A : Type u_1} [CommRing A] {B : Type u_2} [CommRing B] {f : A →+* B} {K : Type u_3} {M : Submonoid A} [CommRing K] [Algebra A K] [IsLocalization M K] (L : Type u_4) {N : Submonoid B} [CommRing L] [Algebra B L] [IsLocalization N L] (hf : M ≤ Submonoid.comap f N) {I : FractionalIdeal M K} [IsDomain B] (hf' : Function.Injective ⇑f) (hN : 0 ∉ N) : extended L hf I = 0 ↔ I = 0

@[simp]

theorem FractionalIdeal.extended_one {A : Type u_1} [CommRing A] {B : Type u_2} [CommRing B] {f : A →+* B} {K : Type u_3} {M : Submonoid A} [CommRing K] [Algebra A K] [IsLocalization M K] (L : Type u_4) {N : Submonoid B} [CommRing L] [Algebra B L] [IsLocalization N L] (hf : M ≤ Submonoid.comap f N) : extended L hf 1 = 1

theorem FractionalIdeal.extended_le_one_of_le_one {A : Type u_1} [CommRing A] {B : Type u_2} [CommRing B] {f : A →+* B} {K : Type u_3} {M : Submonoid A} [CommRing K] [Algebra A K] [IsLocalization M K] (L : Type u_4) {N : Submonoid B} [CommRing L] [Algebra B L] [IsLocalization N L] (hf : M ≤ Submonoid.comap f N) (I : FractionalIdeal M K) (hI : I ≤ 1) : extended L hf I ≤ 1

theorem FractionalIdeal.one_le_extended_of_one_le {A : Type u_1} [CommRing A] {B : Type u_2} [CommRing B] {f : A →+* B} {K : Type u_3} {M : Submonoid A} [CommRing K] [Algebra A K] [IsLocalization M K] (L : Type u_4) {N : Submonoid B} [CommRing L] [Algebra B L] [IsLocalization N L] (hf : M ≤ Submonoid.comap f N) (I : FractionalIdeal M K) (hI : 1 ≤ I) : 1 ≤ extended L hf I

theorem FractionalIdeal.extended_add {A : Type u_1} [CommRing A] {B : Type u_2} [CommRing B] {f : A →+* B} {K : Type u_3} {M : Submonoid A} [CommRing K] [Algebra A K] [IsLocalization M K] (L : Type u_4) {N : Submonoid B} [CommRing L] [Algebra B L] [IsLocalization N L] (hf : M ≤ Submonoid.comap f N) (I J : FractionalIdeal M K) : extended L hf (I + J) = extended L hf I + extended L hf J

theorem FractionalIdeal.extended_mul {A : Type u_1} [CommRing A] {B : Type u_2} [CommRing B] {f : A →+* B} {K : Type u_3} {M : Submonoid A} [CommRing K] [Algebra A K] [IsLocalization M K] (L : Type u_4) {N : Submonoid B} [CommRing L] [Algebra B L] [IsLocalization N L] (hf : M ≤ Submonoid.comap f N) (I J : FractionalIdeal M K) : extended L hf (I * J) = extended L hf I * extended L hf J

@[simp]

theorem FractionalIdeal.extended_coeIdeal_eq_map {A : Type u_1} [CommRing A] {B : Type u_2} [CommRing B] {f : A →+* B} {K : Type u_3} {M : Submonoid A} [CommRing K] [Algebra A K] [IsLocalization M K] (L : Type u_4) {N : Submonoid B} [CommRing L] [Algebra B L] [IsLocalization N L] (hf : M ≤ Submonoid.comap f N) (I₀ : Ideal A) : extended L hf ↑I₀ = ↑(Ideal.map f I₀)

def FractionalIdeal.extendedHom' {A : Type u_1} [CommRing A] {B : Type u_2} [CommRing B] {f : A →+* B} {K : Type u_3} {M : Submonoid A} [CommRing K] [Algebra A K] [IsLocalization M K] (L : Type u_4) {N : Submonoid B} [CommRing L] [Algebra B L] [IsLocalization N L] (hf : M ≤ Submonoid.comap f N) : FractionalIdeal M K →+* FractionalIdeal N L

The ring homomorphism version of FractionalIdeal.extended. See FractionalIdeal.extendedHom for a more convient version that is often enough.

Equations

• FractionalIdeal.extendedHom' L hf = { toFun := FractionalIdeal.extended L hf, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem FractionalIdeal.extendedHom'_apply {A : Type u_1} [CommRing A] {B : Type u_2} [CommRing B] {f : A →+* B} {K : Type u_3} {M : Submonoid A} [CommRing K] [Algebra A K] [IsLocalization M K] (L : Type u_4) {N : Submonoid B} [CommRing L] [Algebra B L] [IsLocalization N L] (hf : M ≤ Submonoid.comap f N) (I : FractionalIdeal M K) : (extendedHom' L hf) I = extended L hf I

@[reducible, inline]

abbrev FractionalIdeal.extendedHom {A : Type u_1} {K : Type u_2} (L : Type u_3) (B : Type u_4) [CommRing A] [IsDomain A] [CommRing B] [IsDomain B] [Algebra A B] [Module.IsTorsionFree A B] [Field K] [Field L] [Algebra A K] [Algebra B L] [IsFractionRing A K] [IsFractionRing B L] : FractionalIdeal (nonZeroDivisors A) K →+* FractionalIdeal (nonZeroDivisors B) L

The ring homomorphism that extends a fractional ideal of A to a fractional ideal of B for an extension of domains A ⊆ B.

Equations

• FractionalIdeal.extendedHom L B = FractionalIdeal.extendedHom' L ⋯

@[deprecated FractionalIdeal.extendedHom (since := "2026-04-16")]

def FractionalIdeal.extendedHomₐ {A : Type u_1} {K : Type u_2} (L : Type u_3) (B : Type u_4) [CommRing A] [IsDomain A] [CommRing B] [IsDomain B] [Algebra A B] [Module.IsTorsionFree A B] [Field K] [Field L] [Algebra A K] [Algebra B L] [IsFractionRing A K] [IsFractionRing B L] : FractionalIdeal (nonZeroDivisors A) K →+* FractionalIdeal (nonZeroDivisors B) L

Alias of FractionalIdeal.extendedHom.

---

The ring homomorphism that extends a fractional ideal of A to a fractional ideal of B for an extension of domains A ⊆ B.

Equations

• @FractionalIdeal.extendedHomₐ = @FractionalIdeal.extendedHom

theorem FractionalIdeal.extendedHom_eq_zero_iff {A : Type u_1} {K : Type u_2} (L : Type u_3) (B : Type u_4) [CommRing A] [IsDomain A] [CommRing B] [IsDomain B] [Algebra A B] [Module.IsTorsionFree A B] [Field K] [Field L] [Algebra A K] [Algebra B L] [IsFractionRing A K] [IsFractionRing B L] {I : FractionalIdeal (nonZeroDivisors A) K} : (extendedHom L B) I = 0 ↔ I = 0

@[deprecated FractionalIdeal.extendedHom_eq_zero_iff (since := "2026-04-16")]

theorem FractionalIdeal.extendedHomₐ_eq_zero_iff {A : Type u_1} {K : Type u_2} (L : Type u_3) (B : Type u_4) [CommRing A] [IsDomain A] [CommRing B] [IsDomain B] [Algebra A B] [Module.IsTorsionFree A B] [Field K] [Field L] [Algebra A K] [Algebra B L] [IsFractionRing A K] [IsFractionRing B L] {I : FractionalIdeal (nonZeroDivisors A) K} : (extendedHom L B) I = 0 ↔ I = 0

Alias of FractionalIdeal.extendedHom_eq_zero_iff.

theorem FractionalIdeal.extendedHom_coeIdeal_eq_map {A : Type u_1} {K : Type u_2} (L : Type u_3) (B : Type u_4) [CommRing A] [IsDomain A] [CommRing B] [IsDomain B] [Algebra A B] [Module.IsTorsionFree A B] [Field K] [Field L] [Algebra A K] [Algebra B L] [IsFractionRing A K] [IsFractionRing B L] (I : Ideal A) : (extendedHom L B) ↑I = ↑(Ideal.map (algebraMap A B) I)

@[deprecated FractionalIdeal.extendedHom_coeIdeal_eq_map (since := "2026-04-16")]

theorem FractionalIdeal.extendedHomₐ_coeIdeal_eq_map {A : Type u_1} {K : Type u_2} (L : Type u_3) (B : Type u_4) [CommRing A] [IsDomain A] [CommRing B] [IsDomain B] [Algebra A B] [Module.IsTorsionFree A B] [Field K] [Field L] [Algebra A K] [Algebra B L] [IsFractionRing A K] [IsFractionRing B L] (I : Ideal A) : (extendedHom L B) ↑I = ↑(Ideal.map (algebraMap A B) I)

Alias of FractionalIdeal.extendedHom_coeIdeal_eq_map.

theorem FractionalIdeal.coe_extendedHom_eq_span {A : Type u_1} {K : Type u_2} (L : Type u_3) (B : Type u_4) [CommRing A] [IsDomain A] [CommRing B] [IsDomain B] [Algebra A B] [Module.IsTorsionFree A B] [Field K] [Field L] [Algebra A K] [Algebra B L] [IsFractionRing A K] [IsFractionRing B L] [Algebra K L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [Algebra.IsIntegral A B] (I : FractionalIdeal (nonZeroDivisors A) K) : ↑((extendedHom L B) I) = Submodule.span B (⇑(algebraMap K L) '' ↑I)

@[deprecated FractionalIdeal.coe_extendedHom_eq_span (since := "2026-04-16")]

theorem FractionalIdeal.coe_extendedHomₐ_eq_span {A : Type u_1} {K : Type u_2} (L : Type u_3) (B : Type u_4) [CommRing A] [IsDomain A] [CommRing B] [IsDomain B] [Algebra A B] [Module.IsTorsionFree A B] [Field K] [Field L] [Algebra A K] [Algebra B L] [IsFractionRing A K] [IsFractionRing B L] [Algebra K L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [Algebra.IsIntegral A B] (I : FractionalIdeal (nonZeroDivisors A) K) : ↑((extendedHom L B) I) = Submodule.span B (⇑(algebraMap K L) '' ↑I)

Alias of FractionalIdeal.coe_extendedHom_eq_span.

theorem FractionalIdeal.le_one_of_extendedHom_le_one {A : Type u_1} {K : Type u_2} (L : Type u_3) (B : Type u_4) [CommRing A] [IsDomain A] [CommRing B] [IsDomain B] [Algebra A B] [Module.IsTorsionFree A B] [Field K] [Field L] [Algebra A K] [Algebra B L] [IsFractionRing A K] [IsFractionRing B L] {I : FractionalIdeal (nonZeroDivisors A) K} [Algebra K L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [Algebra.IsIntegral A B] [IsIntegrallyClosed A] [IsIntegrallyClosed B] (hI : (extendedHom L B) I ≤ 1) : I ≤ 1

@[deprecated FractionalIdeal.le_one_of_extendedHom_le_one (since := "2026-04-16")]

theorem FractionalIdeal.le_one_of_extendedHomₐ_le_one {A : Type u_1} {K : Type u_2} (L : Type u_3) (B : Type u_4) [CommRing A] [IsDomain A] [CommRing B] [IsDomain B] [Algebra A B] [Module.IsTorsionFree A B] [Field K] [Field L] [Algebra A K] [Algebra B L] [IsFractionRing A K] [IsFractionRing B L] {I : FractionalIdeal (nonZeroDivisors A) K} [Algebra K L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [Algebra.IsIntegral A B] [IsIntegrallyClosed A] [IsIntegrallyClosed B] (hI : (extendedHom L B) I ≤ 1) : I ≤ 1

Alias of FractionalIdeal.le_one_of_extendedHom_le_one.

theorem FractionalIdeal.extendedHom_le_one_iff {A : Type u_1} {K : Type u_2} (L : Type u_3) (B : Type u_4) [CommRing A] [IsDomain A] [CommRing B] [IsDomain B] [Algebra A B] [Module.IsTorsionFree A B] [Field K] [Field L] [Algebra A K] [Algebra B L] [IsFractionRing A K] [IsFractionRing B L] {I : FractionalIdeal (nonZeroDivisors A) K} [Algebra K L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [Algebra.IsIntegral A B] [IsIntegrallyClosed A] [IsIntegrallyClosed B] : (extendedHom L B) I ≤ 1 ↔ I ≤ 1

@[deprecated FractionalIdeal.extendedHom_le_one_iff (since := "2026-04-16")]

theorem FractionalIdeal.extendedHomₐ_le_one_iff {A : Type u_1} {K : Type u_2} (L : Type u_3) (B : Type u_4) [CommRing A] [IsDomain A] [CommRing B] [IsDomain B] [Algebra A B] [Module.IsTorsionFree A B] [Field K] [Field L] [Algebra A K] [Algebra B L] [IsFractionRing A K] [IsFractionRing B L] {I : FractionalIdeal (nonZeroDivisors A) K} [Algebra K L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [Algebra.IsIntegral A B] [IsIntegrallyClosed A] [IsIntegrallyClosed B] : (extendedHom L B) I ≤ 1 ↔ I ≤ 1

Alias of FractionalIdeal.extendedHom_le_one_iff.

theorem FractionalIdeal.one_le_extendedHom_iff {A : Type u_1} {K : Type u_2} (L : Type u_3) (B : Type u_4) [CommRing A] [IsDomain A] [CommRing B] [IsDomain B] [Algebra A B] [Module.IsTorsionFree A B] [Field K] [Field L] [Algebra A K] [Algebra B L] [IsFractionRing A K] [IsFractionRing B L] {I : FractionalIdeal (nonZeroDivisors A) K} [Algebra K L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [Algebra.IsIntegral A B] [IsDedekindDomain A] [IsDedekindDomain B] (hI : I ≠ 0) : 1 ≤ (extendedHom L B) I ↔ 1 ≤ I

@[deprecated FractionalIdeal.one_le_extendedHom_iff (since := "2026-04-16")]

theorem FractionalIdeal.one_le_extendedHomₐ_iff {A : Type u_1} {K : Type u_2} (L : Type u_3) (B : Type u_4) [CommRing A] [IsDomain A] [CommRing B] [IsDomain B] [Algebra A B] [Module.IsTorsionFree A B] [Field K] [Field L] [Algebra A K] [Algebra B L] [IsFractionRing A K] [IsFractionRing B L] {I : FractionalIdeal (nonZeroDivisors A) K} [Algebra K L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [Algebra.IsIntegral A B] [IsDedekindDomain A] [IsDedekindDomain B] (hI : I ≠ 0) : 1 ≤ (extendedHom L B) I ↔ 1 ≤ I

Alias of FractionalIdeal.one_le_extendedHom_iff.

theorem FractionalIdeal.extendedHom_eq_one_iff {A : Type u_1} {K : Type u_2} (L : Type u_3) (B : Type u_4) [CommRing A] [IsDomain A] [CommRing B] [IsDomain B] [Algebra A B] [Module.IsTorsionFree A B] [Field K] [Field L] [Algebra A K] [Algebra B L] [IsFractionRing A K] [IsFractionRing B L] {I : FractionalIdeal (nonZeroDivisors A) K} [Algebra K L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [Algebra.IsIntegral A B] [IsDedekindDomain A] [IsDedekindDomain B] (hI : I ≠ 0) : (extendedHom L B) I = 1 ↔ I = 1

@[deprecated FractionalIdeal.extendedHom_eq_one_iff (since := "2026-04-16")]

theorem FractionalIdeal.extendedHomₐ_eq_one_iff {A : Type u_1} {K : Type u_2} (L : Type u_3) (B : Type u_4) [CommRing A] [IsDomain A] [CommRing B] [IsDomain B] [Algebra A B] [Module.IsTorsionFree A B] [Field K] [Field L] [Algebra A K] [Algebra B L] [IsFractionRing A K] [IsFractionRing B L] {I : FractionalIdeal (nonZeroDivisors A) K} [Algebra K L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [Algebra.IsIntegral A B] [IsDedekindDomain A] [IsDedekindDomain B] (hI : I ≠ 0) : (extendedHom L B) I = 1 ↔ I = 1

Alias of FractionalIdeal.extendedHom_eq_one_iff.

theorem FractionalIdeal.extendedHom_injective (A : Type u_1) (K : Type u_2) (L : Type u_3) (B : Type u_4) [CommRing A] [IsDomain A] [CommRing B] [IsDomain B] [Algebra A B] [Module.IsTorsionFree A B] [Field K] [Field L] [Algebra A K] [Algebra B L] [IsFractionRing A K] [IsFractionRing B L] [Algebra K L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [Algebra.IsIntegral A B] [IsDedekindDomain A] [IsDedekindDomain B] : Function.Injective fun (I : FractionalIdeal (nonZeroDivisors A) K) => (extendedHom L B) I

@[deprecated FractionalIdeal.extendedHom_injective (since := "2026-04-16")]

theorem FractionalIdeal.extendedHomₐ_injective (A : Type u_1) (K : Type u_2) (L : Type u_3) (B : Type u_4) [CommRing A] [IsDomain A] [CommRing B] [IsDomain B] [Algebra A B] [Module.IsTorsionFree A B] [Field K] [Field L] [Algebra A K] [Algebra B L] [IsFractionRing A K] [IsFractionRing B L] [Algebra K L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [Algebra.IsIntegral A B] [IsDedekindDomain A] [IsDedekindDomain B] : Function.Injective fun (I : FractionalIdeal (nonZeroDivisors A) K) => (extendedHom L B) I

Alias of FractionalIdeal.extendedHom_injective.