The conductor ideal

This file defines the conductor ideal of an element x of R-algebra S. This is the ideal of S consisting of all elements a such that for all b in S, the product a * b lies in the Rsubalgebra of S generated by x.

def conductor (R : Type u_1) {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (x : S) : Ideal S

Let S / R be a ring extension and x : S, then the conductor of R<x> is the biggest ideal of S contained in R<x>.

Equations

• conductor R x = { carrier := {a : S | ∀ (b : S), a * b ∈ Algebra.adjoin R {x}}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

theorem conductor_eq_of_eq {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {x y : S} (h : ↑(Algebra.adjoin R {x}) = ↑(Algebra.adjoin R {y})) : conductor R x = conductor R y

theorem conductor_subset_adjoin {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {x : S} : ↑(conductor R x) ⊆ ↑(Algebra.adjoin R {x})

theorem mem_conductor_iff {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {x y : S} : y ∈ conductor R x ↔ ∀ (b : S), y * b ∈ Algebra.adjoin R {x}

theorem conductor_eq_top_of_adjoin_eq_top {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {x : S} (h : Algebra.adjoin R {x} = ⊤) : conductor R x = ⊤

theorem conductor_eq_top_of_powerBasis {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (pb : PowerBasis R S) : conductor R pb.gen = ⊤

theorem adjoin_eq_top_of_conductor_eq_top {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {x : S} (h : conductor R x = ⊤) : Algebra.adjoin R {x} = ⊤

theorem conductor_eq_top_iff_adjoin_eq_top {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {x : S} : conductor R x = ⊤ ↔ Algebra.adjoin R {x} = ⊤

theorem mem_coeSubmodule_conductor {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {L : Type u_3} [CommRing L] [Algebra S L] [Algebra R L] [IsScalarTower R S L] [NoZeroSMulDivisors S L] {x : S} {y : L} : y ∈ IsLocalization.coeSubmodule L (conductor R x) ↔ ∀ (z : S), y * (algebraMap S L) z ∈ Algebra.adjoin R {(algebraMap S L) x}

theorem prod_mem_ideal_map_of_mem_conductor {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {x : S} {I : Ideal R} {p : R} {z : S} (hp : p ∈ Ideal.comap (algebraMap R S) (conductor R x)) (hz' : z ∈ Ideal.map (algebraMap R S) I) : (algebraMap R S) p * z ∈ ⇑(algebraMap (↥(Algebra.adjoin R {x})) S) '' ↑(Ideal.map (algebraMap R ↥(Algebra.adjoin R {x})) I)

This technical lemma tell us that if C is the conductor of R<x> and I is an ideal of R then p * (I * S) ⊆ I * R<x> for any p in C ∩ R

theorem comap_map_eq_map_adjoin_of_coprime_conductor {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {x : S} {I : Ideal R} (hx : Ideal.comap (algebraMap R S) (conductor R x) ⊔ I = ⊤) (h_alg : Function.Injective ⇑(algebraMap (↥(Algebra.adjoin R {x})) S)) : Ideal.comap (algebraMap (↥(Algebra.adjoin R {x})) S) (Ideal.map (algebraMap R S) I) = Ideal.map (algebraMap R ↥(Algebra.adjoin R {x})) I

A technical result telling us that (I * S) ∩ R<x> = I * R<x> for any ideal I of R.

noncomputable def quotAdjoinEquivQuotMap {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {x : S} {I : Ideal R} (hx : Ideal.comap (algebraMap R S) (conductor R x) ⊔ I = ⊤) (h_alg : Function.Injective ⇑(algebraMap (↥(Algebra.adjoin R {x})) S)) : ↥(Algebra.adjoin R {x}) ⧸ Ideal.map (algebraMap R ↥(Algebra.adjoin R {x})) I ≃+* S ⧸ Ideal.map (algebraMap R S) I

The canonical morphism of rings from R<x> ⧸ (I*R<x>) to S ⧸ (I*S) is an isomorphism when I and (conductor R x) ∩ R are coprime.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem quotAdjoinEquivQuotMap_apply_mk {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {x : S} {I : Ideal R} (hx : Ideal.comap (algebraMap R S) (conductor R x) ⊔ I = ⊤) (h_alg : Function.Injective ⇑(algebraMap (↥(Algebra.adjoin R {x})) S)) (a : ↥(Algebra.adjoin R {x})) : (quotAdjoinEquivQuotMap hx h_alg) ((Ideal.Quotient.mk (Ideal.map (algebraMap R ↥(Algebra.adjoin R {x})) I)) a) = (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) ↑a