Adjoining Elements to Fields #

In this file we introduce the notion of adjoining elements to fields. This isn't quite the same as adjoining elements to rings. For example, K[x] might not include x⁻¹.

Notation #

F⟮α⟯: adjoin a single element α to F (in scope IntermediateField).

source

def IntermediateField.adjoin (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : Set E) :

IntermediateField F E

adjoin F S extends a field F by adjoining a set S ⊆ E.

Instances For

source

@[simp]

theorem IntermediateField.adjoin_toSubfield (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : Set E) :

(adjoin F S).toSubfield = Subfield.closure (Set.range ⇑(algebraMap F E) ∪ S)

source

theorem IntermediateField.mem_adjoin_iff_div {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {S : Set E} {x : E} :

x ∈ adjoin F S ↔ ∃ r ∈ Algebra.adjoin F S, ∃ s ∈ Algebra.adjoin F S, x = r / s

source

@[simp]

theorem IntermediateField.adjoin_le_iff {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {S : Set E} {T : IntermediateField F E} :

adjoin F S ≤ T ↔ S ⊆ ↑T

source

theorem IntermediateField.gc {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :

GaloisConnection (adjoin F) fun (x : IntermediateField F E) => ↑x

source

def IntermediateField.gi {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :

GaloisInsertion (adjoin F) fun (x : IntermediateField F E) => ↑x

Galois insertion between adjoin and coe.

Instances For

source

@[implicit_reducible]

instance IntermediateField.instCompleteLattice {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :

CompleteLattice (IntermediateField F E)

source

@[implicit_reducible]

instance IntermediateField.instAlgebraSubtypeMemMin {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (K₁ K₂ : IntermediateField F E) :

Algebra ↥(K₁ ⊓ K₂) ↥K₁

source

@[implicit_reducible]

instance IntermediateField.instAlgebraSubtypeMemMin_1 {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (K₁ K₂ : IntermediateField F E) :

Algebra ↥(K₁ ⊓ K₂) ↥K₂

source

theorem IntermediateField.sup_def {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (S T : IntermediateField F E) :

S ⊔ T = adjoin F (↑S ∪ ↑T)

source

theorem IntermediateField.sSup_def {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : Set (IntermediateField F E)) :

sSup S = adjoin F (⋃₀ (SetLike.coe '' S))

source

@[implicit_reducible]

instance IntermediateField.instInhabited {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :

Inhabited (IntermediateField F E)

source

@[implicit_reducible]

instance IntermediateField.instUnique {F : Type u_1} [Field F] :

Unique (IntermediateField F F)

source

theorem IntermediateField.coe_bot {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :

↑⊥ = Set.range ⇑(algebraMap F E)

source

theorem IntermediateField.mem_bot {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {x : E} :

x ∈ ⊥ ↔ x ∈ Set.range ⇑(algebraMap F E)

source

@[simp]

theorem IntermediateField.bot_toSubalgebra {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :

⊥.toSubalgebra = ⊥

source

theorem IntermediateField.bot_toSubfield {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :

⊥.toSubfield = (algebraMap F E).fieldRange

source

@[simp]

theorem IntermediateField.coe_top {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :

↑⊤ = Set.univ

source

@[simp]

theorem IntermediateField.mem_top {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {x : E} :

x ∈ ⊤

source

@[simp]

theorem IntermediateField.top_toSubalgebra {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :

⊤.toSubalgebra = ⊤

source

@[simp]

theorem IntermediateField.top_toSubfield {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :

⊤.toSubfield = ⊤

source

@[simp]

theorem IntermediateField.coe_inf {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (S T : IntermediateField F E) :

↑(S ⊓ T) = ↑S ∩ ↑T

source

@[simp]

theorem IntermediateField.mem_inf {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {S T : IntermediateField F E} {x : E} :

x ∈ S ⊓ T ↔ x ∈ S ∧ x ∈ T

source

@[simp]

theorem IntermediateField.inf_toSubalgebra {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (S T : IntermediateField F E) :

(S ⊓ T).toSubalgebra = S.toSubalgebra ⊓ T.toSubalgebra

source

@[simp]

theorem IntermediateField.inf_toSubfield {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (S T : IntermediateField F E) :

(S ⊓ T).toSubfield = S.toSubfield ⊓ T.toSubfield

source

@[simp]

theorem IntermediateField.sup_toSubfield {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (S T : IntermediateField F E) :

(S ⊔ T).toSubfield = S.toSubfield ⊔ T.toSubfield

source

@[simp]

theorem IntermediateField.coe_sInf {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : Set (IntermediateField F E)) :

↑(sInf S) = ⋂ s ∈ S, ↑s

source

@[simp]

theorem IntermediateField.mem_sInf {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {S : Set (IntermediateField F E)} {x : E} :

x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p

source

@[simp]

theorem IntermediateField.sInf_toSubalgebra {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : Set (IntermediateField F E)) :

(sInf S).toSubalgebra = sInf (toSubalgebra '' S)

source

@[simp]

theorem IntermediateField.sInf_toSubfield {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : Set (IntermediateField F E)) :

(sInf S).toSubfield = sInf (toSubfield '' S)

source

@[simp]

theorem IntermediateField.sSup_toSubfield {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : Set (IntermediateField F E)) (hS : S.Nonempty) :

(sSup S).toSubfield = sSup (toSubfield '' S)

source

@[simp]

theorem IntermediateField.coe_iInf {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {ι : Sort u_3} (S : ι → IntermediateField F E) :

↑(iInf S) = ⋂ (i : ι), ↑(S i)

source

@[simp]

theorem IntermediateField.iInf_toSubalgebra {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {ι : Sort u_3} (S : ι → IntermediateField F E) :

(iInf S).toSubalgebra = ⨅ (i : ι), (S i).toSubalgebra

source

@[simp]

theorem IntermediateField.iInf_toSubfield {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {ι : Sort u_3} (S : ι → IntermediateField F E) :

(iInf S).toSubfield = ⨅ (i : ι), (S i).toSubfield

source

@[simp]

theorem IntermediateField.iSup_toSubfield {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {ι : Sort u_3} [Nonempty ι] (S : ι → IntermediateField F E) :

(iSup S).toSubfield = ⨆ (i : ι), (S i).toSubfield

source

noncomputable def IntermediateField.botEquiv (F : Type u_1) [Field F] (E : Type u_2) [Field E] [Algebra F E] :

↥⊥ ≃ₐ[F] F

The bottom IntermediateField is isomorphic to the field.

Instances For

source

theorem IntermediateField.botEquiv_def {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (x : F) :

(botEquiv F E) ((algebraMap F ↥⊥) x) = x

source

@[simp]

theorem IntermediateField.botEquiv_symm {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (x : F) :

(botEquiv F E).symm x = (algebraMap F ↥⊥) x

source

@[implicit_reducible]

noncomputable instance IntermediateField.algebraOverBot {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :

Algebra (↥⊥) F

source

theorem IntermediateField.coe_algebraMap_over_bot {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :

⇑(algebraMap (↥⊥) F) = ⇑(botEquiv F E)

source

instance IntermediateField.isScalarTower_over_bot {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :

IsScalarTower (↥⊥) F E

source

def IntermediateField.topEquiv {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :

↥⊤ ≃ₐ[F] E

The top IntermediateField is isomorphic to the field.

This is the intermediate field version of Subalgebra.topEquiv.

Instances For

source

@[simp]

theorem IntermediateField.topEquiv_apply {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (a : ↥⊤) :

topEquiv a = ↑a

source

@[simp]

theorem IntermediateField.topEquiv_symm_apply_coe {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (a : E) :

↑(topEquiv.symm a) = a

source

@[simp]

theorem IntermediateField.restrictScalars_bot_eq_self {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (K : IntermediateField F E) :

restrictScalars F ⊥ = K

source

@[simp]

theorem IntermediateField.restrictScalars_top {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {K : Type u_3} [Field K] [Algebra K E] [Algebra K F] [IsScalarTower K F E] :

restrictScalars K ⊤ = ⊤

source

@[simp]

theorem IntermediateField.restrictScalars_eq_top_iff {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {K : Type u_3} [Field K] [Algebra K E] [Algebra K F] [IsScalarTower K F E] {L : IntermediateField F E} :

restrictScalars K L = ⊤ ↔ L = ⊤

source

theorem IntermediateField.restrictScalars_sup {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (K : Type u_3) [Field K] [Algebra K E] [Algebra K F] [IsScalarTower K F E] (L L' : IntermediateField F E) :

restrictScalars K L ⊔ restrictScalars K L' = restrictScalars K (L ⊔ L')

source

theorem IntermediateField.restrictScalars_inf {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (K : Type u_3) [Field K] [Algebra K E] [Algebra K F] [IsScalarTower K F E] (L L' : IntermediateField F E) :

restrictScalars K L ⊓ restrictScalars K L' = restrictScalars K (L ⊓ L')

source

@[simp]

theorem IntermediateField.map_bot {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {K : Type u_3} [Field K] [Algebra F K] (f : E →ₐ[F] K) :

map f ⊥ = ⊥

source

theorem IntermediateField.map_sup {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {K : Type u_3} [Field K] [Algebra F K] (s t : IntermediateField F E) (f : E →ₐ[F] K) :

map f (s ⊔ t) = map f s ⊔ map f t

source

theorem IntermediateField.map_iSup {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {K : Type u_3} [Field K] [Algebra F K] {ι : Sort u_4} (f : E →ₐ[F] K) (s : ι → IntermediateField F E) :

map f (iSup s) = ⨆ (i : ι), map f (s i)

source

theorem IntermediateField.map_inf {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {K : Type u_3} [Field K] [Algebra F K] (s t : IntermediateField F E) (f : E →ₐ[F] K) :

map f (s ⊓ t) = map f s ⊓ map f t

source

theorem IntermediateField.map_iInf {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {K : Type u_3} [Field K] [Algebra F K] {ι : Sort u_4} [Nonempty ι] (f : E →ₐ[F] K) (s : ι → IntermediateField F E) :

map f (iInf s) = ⨅ (i : ι), map f (s i)

source

theorem AlgHom.fieldRange_eq_map {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {K : Type u_3} [Field K] [Algebra F K] (f : E →ₐ[F] K) :

f.fieldRange = IntermediateField.map f ⊤

source

theorem AlgHom.map_fieldRange {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {K : Type u_3} [Field K] [Algebra F K] {L : Type u_4} [Field L] [Algebra F L] (f : E →ₐ[F] K) (g : K →ₐ[F] L) :

IntermediateField.map g f.fieldRange = (g.comp f).fieldRange

source

theorem AlgHom.fieldRange_eq_top {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {K : Type u_3} [Field K] [Algebra F K] {f : E →ₐ[F] K} :

f.fieldRange = ⊤ ↔ Function.Surjective ⇑f

source

@[simp]

theorem AlgEquiv.fieldRange_eq_top {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {K : Type u_3} [Field K] [Algebra F K] (f : E ≃ₐ[F] K) :

(↑f).fieldRange = ⊤

source

theorem IntermediateField.adjoin_eq_range_algebraMap_adjoin (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : Set E) :

↑(adjoin F S) = Set.range ⇑(algebraMap (↥(adjoin F S)) E)

source

theorem IntermediateField.adjoin.algebraMap_mem (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : Set E) (x : F) :

(algebraMap F E) x ∈ adjoin F S

source

theorem IntermediateField.adjoin.range_algebraMap_subset (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : Set E) :

Set.range ⇑(algebraMap F E) ⊆ ↑(adjoin F S)

source

@[implicit_reducible]

instance IntermediateField.adjoin.fieldCoe (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : Set E) :

CoeTC F ↥(adjoin F S)

source

@[simp]

theorem IntermediateField.subset_adjoin (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : Set E) :

S ⊆ ↑(adjoin F S)

source

theorem IntermediateField.mem_adjoin_of_mem (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] {S : Set E} {s : E} (hs : s ∈ S) :

s ∈ adjoin F S

source

theorem IntermediateField.notMem_of_notMem_adjoin (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] {S : Set E} {s : E} (hs : s ∉ adjoin F S) :

s ∉ S

source

@[implicit_reducible]

instance IntermediateField.adjoin.setCoe (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : Set E) :

CoeTC ↑S ↥(adjoin F S)

source

theorem IntermediateField.adjoin.mono (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (S T : Set E) (h : S ⊆ T) :

adjoin F S ≤ adjoin F T

source

theorem IntermediateField.adjoin_contains_field_as_subfield {E : Type u_2} [Field E] (S : Set E) (F : Subfield E) :

↑F ⊆ ↑(adjoin (↥F) S)

source

theorem IntermediateField.subset_adjoin_of_subset_left {E : Type u_2} [Field E] (S : Set E) {F : Subfield E} {T : Set E} (HT : T ⊆ ↑F) :

T ⊆ ↑(adjoin (↥F) S)

source

theorem IntermediateField.subset_adjoin_of_subset_right (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : Set E) {T : Set E} (H : T ⊆ S) :

T ⊆ ↑(adjoin F S)

source

@[simp]

theorem IntermediateField.adjoin_empty (F : Type u_3) (E : Type u_4) [Field F] [Field E] [Algebra F E] :

F⟮⟯ = ⊥

source

@[simp]

theorem IntermediateField.adjoin_univ (F : Type u_3) (E : Type u_4) [Field F] [Field E] [Algebra F E] :

adjoin F Set.univ = ⊤

source

theorem IntermediateField.adjoin_le_subfield (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : Set E) {K : Subfield E} (HF : Set.range ⇑(algebraMap F E) ⊆ ↑K) (HS : S ⊆ ↑K) :

(adjoin F S).toSubfield ≤ K

If K is a field with F ⊆ K and S ⊆ K then adjoin F S ≤ K.

source

theorem IntermediateField.adjoin_subset_adjoin_iff (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] {F' : Type u_3} [Field F'] [Algebra F' E] {S S' : Set E} :

↑(adjoin F S) ⊆ ↑(adjoin F' S') ↔ Set.range ⇑(algebraMap F E) ⊆ ↑(adjoin F' S') ∧ S ⊆ ↑(adjoin F' S')

source

theorem IntermediateField.adjoin_adjoin_left (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (S T : Set E) :

restrictScalars F (adjoin (↥(adjoin F S)) T) = adjoin F (S ∪ T)

Adjoining S and then T is the same as adjoining S ∪ T.

source

@[simp]

theorem IntermediateField.adjoin_insert_adjoin (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : Set E) (x : E) :

adjoin F (insert x ↑(adjoin F S)) = adjoin F (insert x S)

source

theorem IntermediateField.adjoin_adjoin_comm (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (S T : Set E) :

restrictScalars F (adjoin (↥(adjoin F S)) T) = restrictScalars F (adjoin (↥(adjoin F T)) S)

F[S][T] = F[T][S]

source

theorem IntermediateField.adjoin_map (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : Set E) {E' : Type u_3} [Field E'] [Algebra F E'] (f : E →ₐ[F] E') :

map f (adjoin F S) = adjoin F (⇑f '' S)

source

@[simp]

theorem IntermediateField.lift_adjoin (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (K : IntermediateField F E) (S : Set ↥K) :

lift (adjoin F S) = adjoin F (Subtype.val '' S)

source

theorem IntermediateField.lift_adjoin_simple (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (K : IntermediateField F E) (α : ↥K) :

lift F⟮α⟯ = F⟮↑α⟯

source

@[simp]

theorem IntermediateField.lift_bot (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (K : IntermediateField F E) :

lift ⊥ = ⊥

source

@[simp]

theorem IntermediateField.lift_top (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (K : IntermediateField F E) :

lift ⊤ = K

source

theorem IntermediateField.lift_sup (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (K : IntermediateField F E) (L L' : IntermediateField F ↥K) :

lift (L ⊔ L') = lift L ⊔ lift L'

source

theorem IntermediateField.lift_inf (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (K : IntermediateField F E) (L L' : IntermediateField F ↥K) :

lift (L ⊓ L') = lift L ⊓ lift L'

source

@[simp]

theorem IntermediateField.adjoin_self (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (K : IntermediateField F E) :

adjoin F ↑K = K

source

theorem IntermediateField.restrictScalars_adjoin (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (K : IntermediateField F E) (S : Set E) :

restrictScalars F (adjoin (↥K) S) = adjoin F (↑K ∪ S)

source

theorem IntermediateField.extendScalars_adjoin {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {K : IntermediateField F E} {S : Set E} (h : K ≤ adjoin F S) :

extendScalars h = adjoin (↥K) S

source

theorem IntermediateField.adjoin_union (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] {S T : Set E} :

adjoin F (S ∪ T) = adjoin F S ⊔ adjoin F T

source

theorem IntermediateField.restrictScalars_adjoin_eq_sup (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (K : IntermediateField F E) (S : Set E) :

restrictScalars F (adjoin (↥K) S) = K ⊔ adjoin F S

source

theorem IntermediateField.adjoin_iUnion (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] {ι : Sort u_3} (f : ι → Set E) :

adjoin F (⋃ (i : ι), f i) = ⨆ (i : ι), adjoin F (f i)

source

theorem IntermediateField.iSup_eq_adjoin (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] {ι : Sort u_3} (f : ι → IntermediateField F E) :

⨆ (i : ι), f i = adjoin F (⋃ (i : ι), ↑(f i))

source

theorem IntermediateField.restrictScalars_adjoin_of_algEquiv {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {L : Type u_3} {L' : Type u_4} [Field L] [Field L'] [Algebra F L] [Algebra L E] [Algebra F L'] [Algebra L' E] [IsScalarTower F L E] [IsScalarTower F L' E] (i : L ≃ₐ[F] L') (hi : ⇑(algebraMap L E) = ⇑(algebraMap L' E) ∘ ⇑i) (S : Set E) :

restrictScalars F (adjoin L S) = restrictScalars F (adjoin L' S)

If E / L / F and E / L' / F are two field extension towers, L ≃ₐ[F] L' is an isomorphism compatible with E / L and E / L', then for any subset S of E, L(S) and L'(S) are equal as intermediate fields of E / F.

source

theorem IntermediateField.adjoin_induction (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] {s : Set E} {p : (x : E) → x ∈ adjoin F s → Prop} (mem : ∀ (x : E) (hx : x ∈ s), p x ⋯) (algebraMap : ∀ (x : F), p ((algebraMap F E) x) ⋯) (add : ∀ (x y : E) (hx : x ∈ adjoin F s) (hy : y ∈ adjoin F s), p x hx → p y hy → p (x + y) ⋯) (inv : ∀ (x : E) (hx : x ∈ adjoin F s), p x hx → p x⁻¹ ⋯) (mul : ∀ (x y : E) (hx : x ∈ adjoin F s) (hy : y ∈ adjoin F s), p x hx → p y hy → p (x * y) ⋯) {x : E} (h : x ∈ adjoin F s) :

p x h

source

theorem IntermediateField.adjoin_algHom_ext (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] {K : Type u_3} [Semiring K] [Algebra F K] {s : Set E} ⦃φ₁ φ₂ : ↥(adjoin F s) →ₐ[F] K⦄ (h : ∀ (x : E) (hx : x ∈ s), φ₁ ⟨x, ⋯⟩ = φ₂ ⟨x, ⋯⟩) :

φ₁ = φ₂

source

theorem IntermediateField.algHom_ext_of_eq_adjoin (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] {K : Type u_3} [Semiring K] [Algebra F K] {S : IntermediateField F E} {s : Set E} (hS : S = adjoin F s) ⦃φ₁ φ₂ : ↥S →ₐ[F] K⦄ (h : ∀ (x : E) (hx : x ∈ s), φ₁ ⟨x, ⋯⟩ = φ₂ ⟨x, ⋯⟩) :

φ₁ = φ₂

source

def IntermediateField.«term_⟮_,,⟯» :

Lean.TrailingParserDescr

If x₁ x₂ ... xₙ : E then F⟮x₁,x₂,...,xₙ⟯ is the IntermediateField F E generated by these elements.

Instances For

source

def IntermediateField.delabAdjoinNotation :

Lean.PrettyPrinter.Delaborator.Delab

Instances For

source

theorem IntermediateField.mem_adjoin_simple_self (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (α : E) :

α ∈ F⟮α⟯

source

def IntermediateField.AdjoinSimple.gen (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (α : E) :

↥F⟮α⟯

generator of F⟮α⟯

Instances For

source

@[simp]

theorem IntermediateField.AdjoinSimple.coe_gen (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (α : E) :

↑(gen F α) = α

source

theorem IntermediateField.AdjoinSimple.algebraMap_gen (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (α : E) :

(algebraMap (↥F⟮α⟯) E) (gen F α) = α

source

@[simp]

theorem IntermediateField.AdjoinSimple.coe_aeval_gen_apply (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (α : E) (f : Polynomial F) :

↑((Polynomial.aeval (gen F α)) f) = (Polynomial.aeval α) f

source

theorem IntermediateField.adjoin_simple_adjoin_simple (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (α β : E) :

restrictScalars F (↥F⟮α⟯)⟮β⟯ = F⟮α, β⟯

source

theorem IntermediateField.adjoin_simple_comm (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] (α β : E) :

restrictScalars F (↥F⟮α⟯)⟮β⟯ = restrictScalars F (↥F⟮β⟯)⟮α⟯

source

theorem IntermediateField.adjoin_simple_le_iff {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {α : E} {K : IntermediateField F E} :

F⟮α⟯ ≤ K ↔ α ∈ K

source

theorem IntermediateField.biSup_adjoin_simple {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : Set E) :

⨆ x ∈ S, F⟮x⟯ = adjoin F S

source

def IntermediateField.RingHom.adjoinAlgebraMap {A : Type u_3} {B : Type u_4} {C : Type u_5} [Field A] [Field B] [Field C] [Algebra A B] [Algebra B C] [Algebra A C] [IsScalarTower A B C] (b : B) :

↥A⟮b⟯ →+* ↥A⟮(algebraMap B C) b⟯

Ring homomorphism between A⟮b⟯ and A⟮↑b⟯.

Instances For

source

@[implicit_reducible]

instance IntermediateField.instAlgebraSubtypeMemAdjoinSingletonSetCoeRingHomAlgebraMap {A : Type u_3} {B : Type u_4} {C : Type u_5} [Field A] [Field B] [Field C] [Algebra A B] [Algebra B C] [Algebra A C] [IsScalarTower A B C] (b : B) :

Algebra ↥A⟮b⟯ ↥A⟮(algebraMap B C) b⟯

source

instance IntermediateField.instIsScalarTowerSubtypeMemAdjoinSingletonSetCoeRingHomAlgebraMap {A : Type u_3} {B : Type u_4} {C : Type u_5} [Field A] [Field B] [Field C] [Algebra A B] [Algebra B C] [Algebra A C] [IsScalarTower A B C] (b : B) :

IsScalarTower (↥A⟮b⟯) (↥A⟮(algebraMap B C) b⟯) C

source

@[simp]

theorem IntermediateField.adjoin_eq_bot_iff {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {S : Set E} :

adjoin F S = ⊥ ↔ S ⊆ ↑⊥

source

theorem IntermediateField.adjoin_simple_eq_bot_iff {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {α : E} :

F⟮α⟯ = ⊥ ↔ α ∈ ⊥

source

@[simp]

theorem IntermediateField.adjoin_zero {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :

F⟮0⟯ = ⊥

source

@[simp]

theorem IntermediateField.adjoin_one {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :

F⟮1⟯ = ⊥

source

@[simp]

theorem IntermediateField.adjoin_intCast {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (n : ℤ) :

F⟮↑n⟯ = ⊥

source

@[simp]

theorem IntermediateField.adjoin_natCast {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (n : ℕ) :

F⟮↑n⟯ = ⊥

source

def IntermediateField.FG {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : IntermediateField F E) :

Prop

An intermediate field S is finitely generated if there exists t : Finset E such that IntermediateField.adjoin F t = S.

We use the class Algebra.EssFiniteType F E instead of (⊤ : IntermediateField F E).FG to say that E is finitely generated as an F extension. See IntermediateField.fg_top_iff.

Instances For

source

theorem IntermediateField.fg_adjoin_finset {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (t : Finset E) :

(adjoin F ↑t).FG

source

theorem IntermediateField.fg_def {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {S : IntermediateField F E} :

S.FG ↔ ∃ (t : Set E), t.Finite ∧ adjoin F t = S

source

theorem IntermediateField.fg_adjoin_of_finite {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {t : Set E} (h : t.Finite) :

(adjoin F t).FG

source

theorem IntermediateField.fg_bot {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :

⊥.FG

source

theorem IntermediateField.fg_sup {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {S T : IntermediateField F E} (hS : S.FG) (hT : T.FG) :

(S ⊔ T).FG

source

theorem IntermediateField.fg_iSup {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] {ι : Sort u_3} [Finite ι] {S : ι → IntermediateField F E} (h : ∀ (i : ι), (S i).FG) :

(⨆ (i : ι), S i).FG

source

theorem IntermediateField.induction_on_adjoin_finset {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (S : Finset E) (P : IntermediateField F E → Prop) (base : P ⊥) (ih : ∀ (K : IntermediateField F E), ∀ x ∈ S, P K → P (restrictScalars F (↥K)⟮x⟯)) :

P (adjoin F ↑S)

source

theorem IntermediateField.induction_on_adjoin_fg {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] (P : IntermediateField F E → Prop) (base : P ⊥) (ih : ∀ (K : IntermediateField F E) (x : E), P K → P (restrictScalars F (↥K)⟮x⟯)) (K : IntermediateField F E) (hK : K.FG) :

P K

source

theorem IntermediateField.map_comap_eq {K : Type u_1} {L : Type u_2} {L' : Type u_3} [Field K] [Field L] [Field L'] [Algebra K L] [Algebra K L'] (f : L →ₐ[K] L') (S : IntermediateField K L') :

map f (comap f S) = S ⊓ f.fieldRange

source

theorem IntermediateField.map_comap_eq_self {K : Type u_1} {L : Type u_2} {L' : Type u_3} [Field K] [Field L] [Field L'] [Algebra K L] [Algebra K L'] {f : L →ₐ[K] L'} {S : IntermediateField K L'} (h : S ≤ f.fieldRange) :

map f (comap f S) = S

source

theorem IntermediateField.map_comap_eq_self_of_surjective {K : Type u_1} {L : Type u_2} {L' : Type u_3} [Field K] [Field L] [Field L'] [Algebra K L] [Algebra K L'] {f : L →ₐ[K] L'} (hf : Function.Surjective ⇑f) (S : IntermediateField K L') :

map f (comap f S) = S

source

theorem IntermediateField.comap_map {K : Type u_1} {L : Type u_2} {L' : Type u_3} [Field K] [Field L] [Field L'] [Algebra K L] [Algebra K L'] (f : L →ₐ[K] L') (S : IntermediateField K L) :

comap f (map f S) = S

source

@[simp]

theorem Subfield.extendScalars_self {L : Type u_2} [Field L] (F : Subfield L) :

extendScalars ⋯ = ⊥

source

@[simp]

theorem Subfield.extendScalars_top {L : Type u_2} [Field L] (F : Subfield L) :

extendScalars ⋯ = ⊤

source

theorem Subfield.extendScalars_sup {L : Type u_2} [Field L] {F E E' : Subfield L} (h : F ≤ E) (h' : F ≤ E') :

extendScalars h ⊔ extendScalars h' = extendScalars ⋯

source

theorem Subfield.extendScalars_inf {L : Type u_2} [Field L] {F E E' : Subfield L} (h : F ≤ E) (h' : F ≤ E') :

extendScalars h ⊓ extendScalars h' = extendScalars ⋯

source

@[simp]

theorem IntermediateField.extendScalars_self {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] (F : IntermediateField K L) :

extendScalars ⋯ = ⊥

source

@[simp]

theorem IntermediateField.extendScalars_top {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] (F : IntermediateField K L) :

extendScalars ⋯ = ⊤

source

theorem IntermediateField.extendScalars_sup {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] {F E E' : IntermediateField K L} (h : F ≤ E) (h' : F ≤ E') :

extendScalars h ⊔ extendScalars h' = extendScalars ⋯

source

theorem IntermediateField.extendScalars_inf {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] {F E E' : IntermediateField K L} (h : F ≤ E) (h' : F ≤ E') :

extendScalars h ⊓ extendScalars h' = extendScalars ⋯

Documentation

Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

Adjoining Elements to Fields #

Notation #