# 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, `Algebra.adjoin 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`.

Equations

- IntermediateField.adjoin F S = { toSubsemiring := (Subfield.closure (Set.range ⇑(algebraMap F E) ∪ S)).toSubsemiring, algebraMap_mem' := ⋯, inv_mem' := ⋯ }

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`.

Equations

- IntermediateField.gi = { choice := fun (s : Set E) (hs : ↑(IntermediateField.adjoin F s) ≤ s) => (IntermediateField.adjoin F s).copy s ⋯, gc := ⋯, le_l_u := ⋯, choice_eq := ⋯ }

Instances For

source
instance IntermediateField.instCompleteLattice {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :
CompleteLattice (IntermediateField F E)
Equations

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

source
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₁
Equations

- K₁.instAlgebraSubtypeMemMin K₂ = inferInstanceAs (Algebra ↥(K₁.toSubalgebra ⊓ K₂.toSubalgebra) ↥K₁.toSubalgebra)

source
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₂
Equations

- K₁.instAlgebraSubtypeMemMin_1 K₂ = inferInstanceAs (Algebra ↥(K₁.toSubalgebra ⊓ K₂.toSubalgebra) ↥K₂.toSubalgebra)

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
instance IntermediateField.instInhabited {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :
Inhabited (IntermediateField F E)
Equations

- IntermediateField.instInhabited = { default := ⊤ }

source
instance IntermediateField.instUnique {F : Type u_1} [Field F] :
Unique (IntermediateField F F)
Equations

- IntermediateField.instUnique = { toInhabited := inferInstanceAs (Inhabited (IntermediateField F F)), uniq := ⋯ }

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) = sInf ((fun (x : IntermediateField F E) => ↑x) '' S)
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 intermediate_field is isomorphic to the field.

Equations

- IntermediateField.botEquiv F E = (⊥.equivOfEq ⊥ ⋯).trans (Algebra.botEquiv F E)

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
noncomputable instance IntermediateField.algebraOverBot {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] :
Algebra (↥⊥) F
Equations

- IntermediateField.algebraOverBot = (↑(IntermediateField.botEquiv F E)).toAlgebra

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`.

Equations

- IntermediateField.topEquiv = Subalgebra.topEquiv

Instances For

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.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.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
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)
Equations

- IntermediateField.adjoin.fieldCoe F S = { coe := fun (x : F) => ⟨(algebraMap F E) x, ⋯⟩ }

source
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
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)
Equations

- IntermediateField.adjoin.setCoe F S = { coe := fun (x : ↑S) => ⟨↑x, ⋯⟩ }

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.

Equations

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

Instances For

source
def IntermediateField.delabAdjoinNotation :
Lean.PrettyPrinter.Delaborator.Delab
Equations

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

Instances For

source
partial def IntermediateField.delabAdjoinNotation.delabInsertArray :
Lean.PrettyPrinter.Delaborator.DelabM (List Lean.Term)
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⟮α⟯`

Equations

- IntermediateField.AdjoinSimple.gen 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
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
@[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`.

Equations

- S.FG = ∃ (t : Finset E), IntermediateField.adjoin F ↑t = S

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 ⋯