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.

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 ∈ FractionalIdeal.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) : ↑(FractionalIdeal.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) : FractionalIdeal.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) : FractionalIdeal.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 : FractionalIdeal M K) (J : FractionalIdeal M K) : FractionalIdeal.extended L hf (I + J) = FractionalIdeal.extended L hf I + FractionalIdeal.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 : FractionalIdeal M K) (J : FractionalIdeal M K) : FractionalIdeal.extended L hf (I * J) = FractionalIdeal.extended L hf I * FractionalIdeal.extended L hf J