# Intermediate fields #

Let L / K be a field extension, given as an instance Algebra K L. This file defines the type of fields in between K and L, IntermediateField K L. An IntermediateField K L is a subfield of L which contains (the image of) K, i.e. it is a Subfield L and a Subalgebra K L.

## Main definitions #

• IntermediateField K L : the type of intermediate fields between K and L.
• Subalgebra.to_intermediateField: turns a subalgebra closed under ⁻¹ into an intermediate field
• Subfield.to_intermediateField: turns a subfield containing the image of K into an intermediate field
• IntermediateField.map: map an intermediate field along an AlgHom
• IntermediateField.restrict_scalars: restrict the scalars of an intermediate field to a smaller field in a tower of fields.

## Implementation notes #

Intermediate fields are defined with a structure extending Subfield and Subalgebra. A Subalgebra is closed under all operations except ⁻¹,

## Tags #

intermediate field, field extension

structure IntermediateField (K : Type u_1) (L : Type u_2) [] [] [Algebra K L] extends :
Type u_2

S : IntermediateField K L is a subset of L such that there is a field tower L / S / K.

• carrier : Set L
• mul_mem' : ∀ {a b : L}, a self.carrierb self.carriera * b self.carrier
• one_mem' : 1 self.carrier
• add_mem' : ∀ {a b : L}, a self.carrierb self.carriera + b self.carrier
• zero_mem' : 0 self.carrier
• algebraMap_mem' : ∀ (r : K), () r self.carrier
• inv_mem' : xself.carrier, x⁻¹ self.carrier
Instances For
theorem IntermediateField.inv_mem' {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (self : ) (x : L) :
x self.carrierx⁻¹ self.carrier
instance IntermediateField.instSetLike {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] :
SetLike () L
Equations
• IntermediateField.instSetLike = { coe := fun (S : ) => S.carrier, coe_injective' := }
theorem IntermediateField.neg_mem {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (S : ) {x : L} (hx : x S) :
-x S
def IntermediateField.toSubfield {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (S : ) :

Reinterpret an IntermediateField as a Subfield.

Equations
• S.toSubfield = let __src := S.toSubalgebra; { toSubsemiring := __src.toSubsemiring, neg_mem' := , inv_mem' := }
Instances For
instance IntermediateField.instSubfieldClass {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] :
Equations
• =
theorem IntermediateField.mem_carrier {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] {s : } {x : L} :
x s.carrier x s
theorem IntermediateField.ext {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] {S : } {T : } (h : ∀ (x : L), x S x T) :
S = T

Two intermediate fields are equal if they have the same elements.

@[simp]
theorem IntermediateField.coe_toSubalgebra {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (S : ) :
S.toSubalgebra = S
@[simp]
theorem IntermediateField.coe_toSubfield {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (S : ) :
S.toSubfield = S
@[simp]
theorem IntermediateField.mem_mk {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (s : ) (hK : ∀ (x : K), () x s) (hi : x{ toSubsemiring := s, algebraMap_mem' := hK }.carrier, x⁻¹ { toSubsemiring := s, algebraMap_mem' := hK }.carrier) (x : L) :
x { toSubsemiring := s, algebraMap_mem' := hK, inv_mem' := hi } x s
@[simp]
theorem IntermediateField.mem_toSubalgebra {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (s : ) (x : L) :
x s.toSubalgebra x s
@[simp]
theorem IntermediateField.mem_toSubfield {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (s : ) (x : L) :
x s.toSubfield x s
def IntermediateField.copy {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (S : ) (s : Set L) (hs : s = S) :

Copy of an intermediate field with a new carrier equal to the old one. Useful to fix definitional equalities.

Equations
• S.copy s hs = { toSubalgebra := S.copy s hs, inv_mem' := }
Instances For
@[simp]
theorem IntermediateField.coe_copy {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (S : ) (s : Set L) (hs : s = S) :
(S.copy s hs) = s
theorem IntermediateField.copy_eq {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (S : ) (s : Set L) (hs : s = S) :
S.copy s hs = S

### Lemmas inherited from more general structures #

The declarations in this section derive from the fact that an IntermediateField is also a subalgebra or subfield. Their use should be replaceable with the corresponding lemma from a subobject class.

theorem IntermediateField.algebraMap_mem {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (S : ) (x : K) :
() x S

An intermediate field contains the image of the smaller field.

theorem IntermediateField.smul_mem {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (S : ) {y : L} :
y S∀ {x : K}, x y S

An intermediate field is closed under scalar multiplication.

theorem IntermediateField.one_mem {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (S : ) :
1 S

An intermediate field contains the ring's 1.

theorem IntermediateField.zero_mem {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (S : ) :
0 S

An intermediate field contains the ring's 0.

theorem IntermediateField.mul_mem {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (S : ) {x : L} {y : L} :
x Sy Sx * y S

An intermediate field is closed under multiplication.

theorem IntermediateField.add_mem {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (S : ) {x : L} {y : L} :
x Sy Sx + y S

An intermediate field is closed under addition.

theorem IntermediateField.sub_mem {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (S : ) {x : L} {y : L} :
x Sy Sx - y S

An intermediate field is closed under subtraction

theorem IntermediateField.inv_mem {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (S : ) {x : L} :
x Sx⁻¹ S

An intermediate field is closed under inverses.

theorem IntermediateField.div_mem {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (S : ) {x : L} {y : L} :
x Sy Sx / y S

An intermediate field is closed under division.

theorem IntermediateField.list_prod_mem {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (S : ) {l : List L} :
(xl, x S)l.prod S

Product of a list of elements in an intermediate_field is in the intermediate_field.

theorem IntermediateField.list_sum_mem {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (S : ) {l : List L} :
(xl, x S)l.sum S

Sum of a list of elements in an intermediate field is in the intermediate_field.

theorem IntermediateField.multiset_prod_mem {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (S : ) (m : ) :
(am, a S)m.prod S

Product of a multiset of elements in an intermediate field is in the intermediate_field.

theorem IntermediateField.multiset_sum_mem {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (S : ) (m : ) :
(am, a S)m.sum S

Sum of a multiset of elements in an IntermediateField is in the IntermediateField.

theorem IntermediateField.prod_mem {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (S : ) {ι : Type u_4} {t : } {f : ιL} (h : ct, f c S) :
(t.prod fun (i : ι) => f i) S

Product of elements of an intermediate field indexed by a Finset is in the intermediate_field.

theorem IntermediateField.sum_mem {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (S : ) {ι : Type u_4} {t : } {f : ιL} (h : ct, f c S) :
(t.sum fun (i : ι) => f i) S

Sum of elements in an IntermediateField indexed by a Finset is in the IntermediateField.

theorem IntermediateField.pow_mem {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (S : ) {x : L} (hx : x S) (n : ) :
x ^ n S
theorem IntermediateField.zsmul_mem {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (S : ) {x : L} (hx : x S) (n : ) :
n x S
theorem IntermediateField.intCast_mem {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (S : ) (n : ) :
n S
theorem IntermediateField.coe_add {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (S : ) (x : S) (y : S) :
(x + y) = x + y
theorem IntermediateField.coe_neg {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (S : ) (x : S) :
(-x) = -x
theorem IntermediateField.coe_mul {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (S : ) (x : S) (y : S) :
(x * y) = x * y
theorem IntermediateField.coe_inv {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (S : ) (x : S) :
x⁻¹ = (x)⁻¹
theorem IntermediateField.coe_zero {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (S : ) :
0 = 0
theorem IntermediateField.coe_one {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (S : ) :
1 = 1
theorem IntermediateField.coe_pow {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (S : ) (x : S) (n : ) :
(x ^ n) = x ^ n
theorem IntermediateField.natCast_mem {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (S : ) (n : ) :
n S
@[deprecated natCast_mem]
theorem IntermediateField.coe_nat_mem {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (S : ) (n : ) :
n S

Alias of IntermediateField.natCast_mem.

@[deprecated intCast_mem]
theorem IntermediateField.coe_int_mem {R : Type u} {S : Type v} [Ring R] [SetLike S R] [hSR : ] (s : S) (n : ) :
n s

Alias of intCast_mem.

def Subalgebra.toIntermediateField {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (S : ) (inv_mem : xS, x⁻¹ S) :

Turn a subalgebra closed under inverses into an intermediate field

Equations
• S.toIntermediateField inv_mem = { toSubalgebra := S, inv_mem' := inv_mem }
Instances For
@[simp]
theorem toSubalgebra_toIntermediateField {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (S : ) (inv_mem : xS, x⁻¹ S) :
(S.toIntermediateField inv_mem).toSubalgebra = S
@[simp]
theorem toIntermediateField_toSubalgebra {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (S : ) :
S.toIntermediateField = S
def Subalgebra.toIntermediateField' {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (S : ) (hS : IsField S) :

Turn a subalgebra satisfying IsField into an intermediate_field

Equations
• S.toIntermediateField' hS = S.toIntermediateField
Instances For
@[simp]
theorem toSubalgebra_toIntermediateField' {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (S : ) (hS : IsField S) :
(S.toIntermediateField' hS).toSubalgebra = S
@[simp]
theorem toIntermediateField'_toSubalgebra {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (S : ) :
S.toIntermediateField' = S
def Subfield.toIntermediateField {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (S : ) (algebra_map_mem : ∀ (x : K), () x S) :

Turn a subfield of L containing the image of K into an intermediate field

Equations
• S.toIntermediateField algebra_map_mem = { toSubsemiring := S.toSubsemiring, algebraMap_mem' := algebra_map_mem, inv_mem' := }
Instances For
instance IntermediateField.toField {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (S : ) :
Field S

An intermediate field inherits a field structure

Equations
• S.toField = S.toSubfield.toField
@[simp]
theorem IntermediateField.coe_sum {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (S : ) {ι : Type u_4} [] (f : ιS) :
(Finset.univ.sum fun (i : ι) => f i) = Finset.univ.sum fun (i : ι) => (f i)
theorem IntermediateField.coe_prod {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (S : ) {ι : Type u_4} [] (f : ιS) :
(Finset.univ.prod fun (i : ι) => f i) = Finset.univ.prod fun (i : ι) => (f i)

IntermediateFields inherit structure from their Subalgebra coercions.

instance IntermediateField.module' {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (S : ) {R : Type u_4} [] [SMul R K] [Module R L] [] :
Module R S
Equations
• S.module' = S.module'
instance IntermediateField.module {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (S : ) :
Module K S
Equations
instance IntermediateField.isScalarTower {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (S : ) {R : Type u_4} [] [SMul R K] [Module R L] [] :
IsScalarTower R K S
Equations
• =
@[simp]
theorem IntermediateField.coe_smul {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (S : ) {R : Type u_4} [] [SMul R K] [Module R L] [] (r : R) (x : S) :
(r x) = r x
instance IntermediateField.algebra {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (S : ) :
Algebra K S
Equations
@[simp]
theorem IntermediateField.algebraMap_apply {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (S : ) (x : S) :
(algebraMap (S) L) x = x
@[simp]
theorem IntermediateField.coe_algebraMap_apply {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (S : ) (x : K) :
((algebraMap K S) x) = () x
instance IntermediateField.isScalarTower_bot {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (S : ) {R : Type u_4} [] [Algebra L R] :
IsScalarTower (S) L R
Equations
• =
instance IntermediateField.isScalarTower_mid {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (S : ) {R : Type u_4} [] [Algebra L R] [Algebra K R] [] :
IsScalarTower K (S) R
Equations
• =
instance IntermediateField.isScalarTower_mid' {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (S : ) :
IsScalarTower K (S) L

Specialize is_scalar_tower_mid to the common case where the top field is L

Equations
• =
instance IntermediateField.instAlgebraSubtypeMem {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] {S : } {E : Type u_4} [] [Algebra L E] (T : IntermediateField (S) E) :
Algebra S T
Equations
• = T.algebra
instance IntermediateField.instModuleSubtypeMem {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] {S : } {E : Type u_4} [] [Algebra L E] (T : IntermediateField (S) E) :
Module S T
Equations
• = Algebra.toModule
instance IntermediateField.instSMulSubtypeMem {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] {S : } {E : Type u_4} [] [Algebra L E] (T : IntermediateField (S) E) :
SMul S T
Equations
• = Algebra.toSMul
instance IntermediateField.instIsScalarTowerSubtypeMem {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] {S : } {E : Type u_4} [] [Algebra L E] (T : IntermediateField (S) E) [Algebra K E] [] :
IsScalarTower K S T
Equations
• =
def IntermediateField.comap {K : Type u_1} {L : Type u_2} {L' : Type u_3} [] [] [Field L'] [Algebra K L] [Algebra K L'] (f : L →ₐ[K] L') (S : ) :

Given f : L →ₐ[K] L', S.comap f is the intermediate field between K and L such that f x ∈ S ↔ x ∈ S.comap f.

Equations
• = let __spread.0 := Subalgebra.comap f S.toSubalgebra; { toSubalgebra := __spread.0, inv_mem' := }
Instances For
def IntermediateField.map {K : Type u_1} {L : Type u_2} {L' : Type u_3} [] [] [Field L'] [Algebra K L] [Algebra K L'] (f : L →ₐ[K] L') (S : ) :

Given f : L →ₐ[K] L', S.map f is the intermediate field between K and L' such that x ∈ S ↔ f x ∈ S.map f.

Equations
• = let __spread.0 := Subalgebra.map f S.toSubalgebra; { toSubalgebra := __spread.0, inv_mem' := }
Instances For
@[simp]
theorem IntermediateField.coe_map {K : Type u_1} {L : Type u_2} {L' : Type u_3} [] [] [Field L'] [Algebra K L] [Algebra K L'] (S : ) (f : L →ₐ[K] L') :
() = f '' S
@[simp]
theorem IntermediateField.toSubalgebra_map {K : Type u_1} {L : Type u_2} {L' : Type u_3} [] [] [Field L'] [Algebra K L] [Algebra K L'] (S : ) (f : L →ₐ[K] L') :
().toSubalgebra = Subalgebra.map f S.toSubalgebra
@[simp]
theorem IntermediateField.toSubfield_map {K : Type u_1} {L : Type u_2} {L' : Type u_3} [] [] [Field L'] [Algebra K L] [Algebra K L'] (S : ) (f : L →ₐ[K] L') :
().toSubfield = Subfield.map (f) S.toSubfield
theorem IntermediateField.map_map {K : Type u_4} {L₁ : Type u_5} {L₂ : Type u_6} {L₃ : Type u_7} [] [Field L₁] [Algebra K L₁] [Field L₂] [Algebra K L₂] [Field L₃] [Algebra K L₃] (E : ) (f : L₁ →ₐ[K] L₂) (g : L₂ →ₐ[K] L₃) :
= IntermediateField.map (g.comp f) E
theorem IntermediateField.map_mono {K : Type u_1} {L : Type u_2} {L' : Type u_3} [] [] [Field L'] [Algebra K L] [Algebra K L'] (f : L →ₐ[K] L') {S : } {T : } (h : S T) :
theorem IntermediateField.map_le_iff_le_comap {K : Type u_1} {L : Type u_2} {L' : Type u_3} [] [] [Field L'] [Algebra K L] [Algebra K L'] {f : L →ₐ[K] L'} {s : } {t : } :
theorem IntermediateField.gc_map_comap {K : Type u_1} {L : Type u_2} {L' : Type u_3} [] [] [Field L'] [Algebra K L] [Algebra K L'] (f : L →ₐ[K] L') :
def IntermediateField.intermediateFieldMap {K : Type u_1} {L : Type u_2} {L' : Type u_3} [] [] [Field L'] [Algebra K L] [Algebra K L'] (e : L ≃ₐ[K] L') (E : ) :
E ≃ₐ[K] ()

Given an equivalence e : L ≃ₐ[K] L' of K-field extensions and an intermediate field E of L/K, intermediateFieldMap e E is the induced equivalence between E and E.map e

Equations
• = e.subalgebraMap E.toSubalgebra
Instances For
@[simp]
theorem IntermediateField.intermediateFieldMap_apply_coe {K : Type u_1} {L : Type u_2} {L' : Type u_3} [] [] [Field L'] [Algebra K L] [Algebra K L'] (e : L ≃ₐ[K] L') (E : ) (a : E) :
() = e a
@[simp]
theorem IntermediateField.intermediateFieldMap_symm_apply_coe {K : Type u_1} {L : Type u_2} {L' : Type u_3} [] [] [Field L'] [Algebra K L] [Algebra K L'] (e : L ≃ₐ[K] L') (E : ) (a : ()) :
(.symm a) = e.symm a
@[simp]
theorem AlgHom.fieldRange_toSubalgebra {K : Type u_1} {L : Type u_2} {L' : Type u_3} [] [] [Field L'] [Algebra K L] [Algebra K L'] (f : L →ₐ[K] L') :
f.fieldRange.toSubalgebra = f.range
def AlgHom.fieldRange {K : Type u_1} {L : Type u_2} {L' : Type u_3} [] [] [Field L'] [Algebra K L] [Algebra K L'] (f : L →ₐ[K] L') :

The range of an algebra homomorphism, as an intermediate field.

Equations
• f.fieldRange = let __src := f.range; let __src_1 := (f).fieldRange; { toSubalgebra := __src, inv_mem' := }
Instances For
@[simp]
theorem AlgHom.coe_fieldRange {K : Type u_1} {L : Type u_2} {L' : Type u_3} [] [] [Field L'] [Algebra K L] [Algebra K L'] (f : L →ₐ[K] L') :
f.fieldRange =
@[simp]
theorem AlgHom.fieldRange_toSubfield {K : Type u_1} {L : Type u_2} {L' : Type u_3} [] [] [Field L'] [Algebra K L] [Algebra K L'] (f : L →ₐ[K] L') :
f.fieldRange.toSubfield = (f).fieldRange
@[simp]
theorem AlgHom.mem_fieldRange {K : Type u_1} {L : Type u_2} {L' : Type u_3} [] [] [Field L'] [Algebra K L] [Algebra K L'] {f : L →ₐ[K] L'} {y : L'} :
y f.fieldRange ∃ (x : L), f x = y
def IntermediateField.val {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (S : ) :
S →ₐ[K] L

The embedding from an intermediate field of L / K to L.

Equations
• S.val = S.val
Instances For
@[simp]
theorem IntermediateField.coe_val {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (S : ) :
S.val = Subtype.val
@[simp]
theorem IntermediateField.val_mk {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (S : ) {x : L} (hx : x S) :
S.val x, hx = x
theorem IntermediateField.range_val {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (S : ) :
S.val.range = S.toSubalgebra
@[simp]
theorem IntermediateField.fieldRange_val {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (S : ) :
S.val.fieldRange = S
instance IntermediateField.AlgHom.inhabited {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (S : ) :
Equations
• = { default := S.val }
theorem IntermediateField.aeval_coe {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (S : ) {R : Type u_4} [] [Algebra R K] [Algebra R L] [] (x : S) (P : ) :
() P = (() P)
theorem IntermediateField.coe_isIntegral_iff {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (S : ) {R : Type u_4} [] [Algebra R K] [Algebra R L] [] {x : S} :
IsIntegral R x
def IntermediateField.inclusion {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] {E : } {F : } (hEF : E F) :
E →ₐ[K] F

The map E → F when E is an intermediate field contained in the intermediate field F.

This is the intermediate field version of Subalgebra.inclusion.

Equations
Instances For
theorem IntermediateField.inclusion_injective {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] {E : } {F : } (hEF : E F) :
@[simp]
theorem IntermediateField.inclusion_self {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] {E : } :
@[simp]
theorem IntermediateField.inclusion_inclusion {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] {E : } {F : } {G : } (hEF : E F) (hFG : F G) (x : E) :
( x) =
@[simp]
theorem IntermediateField.coe_inclusion {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] {E : } {F : } (hEF : E F) (e : E) :
( e) = e
theorem IntermediateField.toSubalgebra_injective {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] :
Function.Injective IntermediateField.toSubalgebra
theorem IntermediateField.map_injective {K : Type u_1} {L : Type u_2} {L' : Type u_3} [] [] [Field L'] [Algebra K L] [Algebra K L'] (f : L →ₐ[K] L') :
theorem IntermediateField.set_range_subset {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (S : ) :
Set.range () S
theorem IntermediateField.fieldRange_le {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (S : ) :
().fieldRange S.toSubfield
@[simp]
theorem IntermediateField.toSubalgebra_le_toSubalgebra {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] {S : } {S' : } :
S.toSubalgebra S'.toSubalgebra S S'
@[simp]
theorem IntermediateField.toSubalgebra_lt_toSubalgebra {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] {S : } {S' : } :
S.toSubalgebra < S'.toSubalgebra S < S'
def IntermediateField.lift {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] {F : } (E : ) :

Lift an intermediate_field of an intermediate_field

Equations
Instances For
instance IntermediateField.hasLift {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] {F : } :
CoeOut () ()
Equations
• IntermediateField.hasLift = { coe := IntermediateField.lift }
theorem IntermediateField.lift_injective {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (F : ) :
Function.Injective IntermediateField.lift
def IntermediateField.restrictScalars (K : Type u_1) {L : Type u_2} {L' : Type u_3} [] [] [Field L'] [Algebra K L] [Algebra K L'] [Algebra L' L] [IsScalarTower K L' L] (E : ) :

Given a tower L / ↥E / L' / K of field extensions, where E is an L'-intermediate field of L, reinterpret E as a K-intermediate field of L.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem IntermediateField.coe_restrictScalars (K : Type u_1) {L : Type u_2} {L' : Type u_3} [] [] [Field L'] [Algebra K L] [Algebra K L'] [Algebra L' L] [IsScalarTower K L' L] {E : } :
= E
@[simp]
theorem IntermediateField.restrictScalars_toSubalgebra (K : Type u_1) {L : Type u_2} {L' : Type u_3} [] [] [Field L'] [Algebra K L] [Algebra K L'] [Algebra L' L] [IsScalarTower K L' L] {E : } :
.toSubalgebra = Subalgebra.restrictScalars K E.toSubalgebra
@[simp]
theorem IntermediateField.restrictScalars_toSubfield (K : Type u_1) {L : Type u_2} {L' : Type u_3} [] [] [Field L'] [Algebra K L] [Algebra K L'] [Algebra L' L] [IsScalarTower K L' L] {E : } :
.toSubfield = E.toSubfield
@[simp]
theorem IntermediateField.mem_restrictScalars (K : Type u_1) {L : Type u_2} {L' : Type u_3} [] [] [Field L'] [Algebra K L] [Algebra K L'] [Algebra L' L] [IsScalarTower K L' L] {E : } {x : L} :
x E
theorem IntermediateField.restrictScalars_injective (K : Type u_1) {L : Type u_2} {L' : Type u_3} [] [] [Field L'] [Algebra K L] [Algebra K L'] [Algebra L' L] [IsScalarTower K L' L] :
def IntermediateField.extendScalars {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] {F : } {E : } (h : F E) :

If F ≤ E are two intermediate fields of L / K, then E is also an intermediate field of L / F. It can be viewed as an inverse to IntermediateField.restrictScalars.

Equations
• = E.toSubfield.toIntermediateField
Instances For
@[simp]
theorem IntermediateField.coe_extendScalars {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] {F : } {E : } (h : F E) :
@[simp]
theorem IntermediateField.extendScalars_toSubfield {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] {F : } {E : } (h : F E) :
.toSubfield = E.toSubfield
@[simp]
theorem IntermediateField.mem_extendScalars {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] {F : } {E : } (h : F E) {x : L} :
x E
@[simp]
theorem IntermediateField.extendScalars_restrictScalars {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] {F : } {E : } (h : F E) :
theorem IntermediateField.extendScalars_le_extendScalars_iff {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] {F : } {E : } {E' : } (h : F E) (h' : F E') :
theorem IntermediateField.extendScalars_le_iff {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] {F : } {E : } (h : F E) (E' : IntermediateField (F) L) :
theorem IntermediateField.le_extendScalars_iff {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] {F : } {E : } (h : F E) (E' : IntermediateField (F) L) :
def IntermediateField.extendScalars.orderIso {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (F : ) :
{ E : // F E } ≃o IntermediateField (F) L

IntermediateField.extendScalars is an order isomorphism from { E : IntermediateField K L // F ≤ E } to IntermediateField F L. Its inverse is IntermediateField.restrictScalars.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem IntermediateField.extendScalars_injective {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (F : ) :
Function.Injective fun (E : { E : // F E }) =>
instance IntermediateField.finiteDimensional_left {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (F : ) [] :
Equations
• =
instance IntermediateField.finiteDimensional_right {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (F : ) [] :
Equations
• =
@[simp]
theorem IntermediateField.rank_eq_rank_subalgebra {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (F : ) :
Module.rank K F.toSubalgebra = Module.rank K F
@[simp]
theorem IntermediateField.finrank_eq_finrank_subalgebra {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (F : ) :
FiniteDimensional.finrank K F.toSubalgebra =
@[simp]
theorem IntermediateField.toSubalgebra_eq_iff {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] {F : } {E : } :
F.toSubalgebra = E.toSubalgebra F = E
theorem IntermediateField.eq_of_le_of_finrank_le {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] {F : } {E : } [hfin : ] (h_le : F E) (h_finrank : ) :
F = E

If F ≤ E are two intermediate fields of L / K such that [E : K] ≤ [F : K] are finite, then F = E.

theorem IntermediateField.eq_of_le_of_finrank_eq {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] {F : } {E : } [] (h_le : F E) (h_finrank : ) :
F = E

If F ≤ E are two intermediate fields of L / K such that [F : K] = [E : K] are finite, then F = E.

theorem IntermediateField.eq_of_le_of_finrank_le' {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] {F : } {E : } [FiniteDimensional (F) L] (h_le : F E) (h_finrank : ) :
F = E

If F ≤ E are two intermediate fields of L / K such that [L : F] ≤ [L : E] are finite, then F = E.

theorem IntermediateField.eq_of_le_of_finrank_eq' {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] {F : } {E : } [FiniteDimensional (F) L] (h_le : F E) (h_finrank : = ) :
F = E

If F ≤ E are two intermediate fields of L / K such that [L : F] = [L : E] are finite, then F = E.

theorem IntermediateField.isAlgebraic_iff {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] {S : } {x : S} :
theorem IntermediateField.isIntegral_iff {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] {S : } {x : S} :
IsIntegral K x
theorem IntermediateField.minpoly_eq {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] {S : } (x : S) :
minpoly K x = minpoly K x
def subalgebraEquivIntermediateField {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] [] :

If L/K is algebraic, the K-subalgebras of L are all fields.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem mem_subalgebraEquivIntermediateField {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] [] {S : } {x : L} :
x subalgebraEquivIntermediateField S x S
@[simp]
theorem mem_subalgebraEquivIntermediateField_symm {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] [] {S : } {x : L} :
x subalgebraEquivIntermediateField.symm S x S