Extension of fractional ideals

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

Main definition

• 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

• extended_add says that extension commutes with addition.
• extended_mul says that extension commutes with multiplication.

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

@[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_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

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.

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] [CommRing B] [IsDomain B] [Algebra A B] [NoZeroSMulDivisors 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 homomorphisme that extends a fractional ideal of A to a fractional ideal of B for A ⊆ B an extension of domains.

Equations

• FractionalIdeal.extendedHomₐ A K L B = FractionalIdeal.extendedHom L ⋯