Documentation

Mathlib.FieldTheory.IntermediateField.Basic

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 #

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

instance IntermediateField.instSetLike {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] :
Equations
theorem IntermediateField.neg_mem {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) {x : L} (hx : x S) :
-x S
def IntermediateField.toSubfield {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) :

Reinterpret an IntermediateField as a Subfield.

Equations
theorem IntermediateField.mem_carrier {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {s : IntermediateField K L} {x : L} :
x s.carrier x s
theorem IntermediateField.ext {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {S T : IntermediateField K L} (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} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) :
S.toSubalgebra = S
@[simp]
theorem IntermediateField.coe_toSubfield {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) :
S.toSubfield = S
@[simp]
theorem IntermediateField.coe_type_toSubalgebra {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) :
S.toSubalgebra = S
@[simp]
theorem IntermediateField.coe_type_toSubfield {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) :
S.toSubfield = S
@[simp]
theorem IntermediateField.mem_mk {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (s : Subsemiring L) (hK : ∀ (x : K), (algebraMap K L) 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} [Field K] [Field L] [Algebra K L] (s : IntermediateField K L) (x : L) :
@[simp]
theorem IntermediateField.mem_toSubfield {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (s : IntermediateField K L) (x : L) :
def IntermediateField.copy {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) (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' := }
@[simp]
theorem IntermediateField.coe_copy {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) (s : Set L) (hs : s = S) :
(S.copy s hs) = s
theorem IntermediateField.copy_eq {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) (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} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) (x : K) :
(algebraMap K L) x S

An intermediate field contains the image of the smaller field.

theorem IntermediateField.smul_mem {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) {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} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) :
1 S

An intermediate field contains the ring's 1.

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

An intermediate field contains the ring's 0.

theorem IntermediateField.mul_mem {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) {x 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} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) {x 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} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) {x 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} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) {x : L} :
x Sx⁻¹ S

An intermediate field is closed under inverses.

theorem IntermediateField.div_mem {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) {x 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} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) {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} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) {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} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) (m : Multiset L) :
(∀ 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} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) (m : Multiset L) :
(∀ 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} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) {ι : Type u_4} {t : Finset ι} {f : ιL} (h : ct, f c S) :
it, 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} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) {ι : Type u_4} {t : Finset ι} {f : ιL} (h : ct, f c S) :
it, 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} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) {x : L} (hx : x S) (n : ) :
x ^ n S
theorem IntermediateField.zsmul_mem {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) {x : L} (hx : x S) (n : ) :
n x S
theorem IntermediateField.intCast_mem {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) (n : ) :
n S
theorem IntermediateField.coe_add {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) (x y : S) :
↑(x + y) = x + y
theorem IntermediateField.coe_neg {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) (x : S) :
↑(-x) = -x
theorem IntermediateField.coe_mul {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) (x y : S) :
↑(x * y) = x * y
theorem IntermediateField.coe_inv {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) (x : S) :
x⁻¹ = (↑x)⁻¹
theorem IntermediateField.coe_zero {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) :
0 = 0
theorem IntermediateField.coe_one {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) :
1 = 1
theorem IntermediateField.coe_pow {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) (x : S) (n : ) :
↑(x ^ n) = x ^ n
theorem IntermediateField.natCast_mem {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) (n : ) :
n S
def Subalgebra.toIntermediateField {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : Subalgebra K L) (inv_mem : xS, x⁻¹ S) :

Turn a subalgebra closed under inverses into an intermediate field

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

Turn a subalgebra satisfying IsField into an intermediate_field

Equations
@[simp]
theorem toSubalgebra_toIntermediateField' {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : Subalgebra K L) (hS : IsField S) :
@[simp]
theorem toIntermediateField'_toSubalgebra {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) :
def Subfield.toIntermediateField {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : Subfield L) (algebra_map_mem : ∀ (x : K), (algebraMap K L) x S) :

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

Equations
instance IntermediateField.toField {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) :
Field S

An intermediate field inherits a field structure

Equations
theorem IntermediateField.coe_sum {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) {ι : Type u_4} [Fintype ι] (f : ιS) :
(∑ i : ι, f i) = i : ι, (f i)
theorem IntermediateField.coe_prod {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) {ι : Type u_4} [Fintype ι] (f : ιS) :
(∏ i : ι, f i) = i : ι, (f i)

IntermediateFields inherit structure from their Subfield coercions.

instance IntermediateField.instSMulSubtypeMem {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {X : Type u_4} [SMul L X] (F : IntermediateField K L) :
SMul (↥F) X

The action by an intermediate field is the action by the underlying field.

Equations
theorem IntermediateField.smul_def {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {X : Type u_4} [SMul L X] {F : IntermediateField K L} (g : F) (m : X) :
g m = g m
instance IntermediateField.smulCommClass_left {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {X : Type u_5} {Y : Type u_4} [SMul L Y] [SMul X Y] [SMulCommClass L X Y] (F : IntermediateField K L) :
SMulCommClass (↥F) X Y
instance IntermediateField.smulCommClass_right {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {X : Type u_4} {Y : Type u_5} [SMul X Y] [SMul L Y] [SMulCommClass X L Y] (F : IntermediateField K L) :
SMulCommClass X (↥F) Y
@[instance 900]
instance IntermediateField.instIsScalarTowerSubtypeMem {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {X : Type u_4} {Y : Type u_5} [SMul X Y] [SMul L X] [SMul L Y] [IsScalarTower L X Y] (F : IntermediateField K L) :
IsScalarTower (↥F) X Y

Note that this provides IsScalarTower F K K which is needed by smul_mul_assoc.

instance IntermediateField.instFaithfulSMulSubtypeMem {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {X : Type u_4} [SMul L X] [FaithfulSMul L X] (F : IntermediateField K L) :
FaithfulSMul (↥F) X
instance IntermediateField.instMulActionSubtypeMem {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {X : Type u_4} [MulAction L X] (F : IntermediateField K L) :
MulAction (↥F) X

The action by an intermediate field is the action by the underlying field.

Equations
instance IntermediateField.instDistribMulActionSubtypeMem {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {X : Type u_4} [AddMonoid X] [DistribMulAction L X] (F : IntermediateField K L) :

The action by an intermediate field is the action by the underlying field.

Equations

The action by an intermediate field is the action by the underlying field.

Equations
instance IntermediateField.instSMulWithZeroSubtypeMem {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {X : Type u_4} [Zero X] [SMulWithZero L X] (F : IntermediateField K L) :
SMulWithZero (↥F) X

The action by an intermediate field is the action by the underlying field.

Equations
instance IntermediateField.instMulActionWithZeroSubtypeMem {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {X : Type u_4} [Zero X] [MulActionWithZero L X] (F : IntermediateField K L) :

The action by an intermediate field is the action by the underlying field.

Equations
instance IntermediateField.instModuleSubtypeMem {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {X : Type u_4} [AddCommMonoid X] [Module L X] (F : IntermediateField K L) :
Module (↥F) X

The action by an intermediate field is the action by the underlying field.

Equations
instance IntermediateField.instMulSemiringActionSubtypeMem {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {X : Type u_4} [Semiring X] [MulSemiringAction L X] (F : IntermediateField K L) :

The action by an intermediate field is the action by the underlying field.

Equations

IntermediateFields inherit structure from their Subalgebra coercions.

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

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

instance IntermediateField.instAlgebraSubtypeMem {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) {E : Type u_4} [Semiring E] [Algebra L E] :
Algebra (↥S) E
Equations
instance IntermediateField.instAlgebraSubtypeMem_1 {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {S : IntermediateField K L} {E : Type u_4} [Field E] [Algebra L E] (T : IntermediateField (↥S) E) :
Algebra S T
Equations
instance IntermediateField.instModuleSubtypeMem_1 {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {S : IntermediateField K L} {E : Type u_4} [Field E] [Algebra L E] (T : IntermediateField (↥S) E) :
Module S T
Equations
instance IntermediateField.instSMulSubtypeMem_1 {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {S : IntermediateField K L} {E : Type u_4} [Field E] [Algebra L E] (T : IntermediateField (↥S) E) :
SMul S T
Equations
instance IntermediateField.instIsScalarTowerSubtypeMem_1 {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {S : IntermediateField K L} {E : Type u_4} [Field E] [Algebra L E] (T : IntermediateField (↥S) E) [Algebra K E] [IsScalarTower K L E] :
IsScalarTower K S T
def IntermediateField.comap {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') :

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
def IntermediateField.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) :

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
@[simp]
theorem IntermediateField.coe_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'] (S : IntermediateField K L) (f : L →ₐ[K] L') :
(map f S) = f '' S
@[simp]
theorem IntermediateField.toSubalgebra_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'] (S : IntermediateField K L) (f : L →ₐ[K] L') :
@[simp]
theorem IntermediateField.toSubfield_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'] (S : IntermediateField K L) (f : L →ₐ[K] L') :
theorem IntermediateField.map_map {K : Type u_4} {L₁ : Type u_5} {L₂ : Type u_6} {L₃ : Type u_7} [Field K] [Field L₁] [Algebra K L₁] [Field L₂] [Algebra K L₂] [Field L₃] [Algebra K L₃] (E : IntermediateField K L₁) (f : L₁ →ₐ[K] L₂) (g : L₂ →ₐ[K] L₃) :
map g (map f E) = map (g.comp f) E
theorem IntermediateField.map_mono {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 T : IntermediateField K L} (h : S T) :
map f S map f T
theorem IntermediateField.map_le_iff_le_comap {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} {t : IntermediateField K L'} :
map f s t s comap f t
theorem IntermediateField.gc_map_comap {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') :
def IntermediateField.intermediateFieldMap {K : Type u_1} {L : Type u_2} {L' : Type u_3} [Field K] [Field L] [Field L'] [Algebra K L] [Algebra K L'] (e : L ≃ₐ[K] L') (E : IntermediateField K L) :
E ≃ₐ[K] (map (↑e) E)

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
theorem IntermediateField.intermediateFieldMap_apply_coe {K : Type u_1} {L : Type u_2} {L' : Type u_3} [Field K] [Field L] [Field L'] [Algebra K L] [Algebra K L'] (e : L ≃ₐ[K] L') (E : IntermediateField K L) (a : E) :
((intermediateFieldMap e E) a) = e a
theorem IntermediateField.intermediateFieldMap_symm_apply_coe {K : Type u_1} {L : Type u_2} {L' : Type u_3} [Field K] [Field L] [Field L'] [Algebra K L] [Algebra K L'] (e : L ≃ₐ[K] L') (E : IntermediateField K L) (a : (map (↑e) E)) :
((intermediateFieldMap e E).symm a) = e.symm a
def AlgHom.fieldRange {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') :

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

Equations
@[simp]
theorem AlgHom.fieldRange_toSubalgebra {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') :
@[simp]
theorem AlgHom.coe_fieldRange {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') :
@[simp]
theorem AlgHom.fieldRange_toSubfield {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') :
@[simp]
theorem AlgHom.mem_fieldRange {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'} {y : L'} :
y f.fieldRange ∃ (x : L), f x = y
def IntermediateField.val {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) :
S →ₐ[K] L

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

Equations
@[simp]
theorem IntermediateField.coe_val {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) :
@[simp]
theorem IntermediateField.val_mk {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) {x : L} (hx : x S) :
S.val x, hx = x
theorem IntermediateField.range_val {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) :
@[simp]
theorem IntermediateField.fieldRange_val {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) :
instance IntermediateField.AlgHom.inhabited {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) :
Equations
theorem IntermediateField.aeval_coe {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) {R : Type u_4} [CommRing R] [Algebra R K] [Algebra R L] [IsScalarTower R K L] (x : S) (P : Polynomial R) :
(Polynomial.aeval x) P = ((Polynomial.aeval x) P)
def IntermediateField.inclusion {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {E F : IntermediateField K L} (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
theorem IntermediateField.inclusion_injective {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {E F : IntermediateField K L} (hEF : E F) :
@[simp]
theorem IntermediateField.inclusion_self {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {E : IntermediateField K L} :
inclusion = AlgHom.id K E
@[simp]
theorem IntermediateField.inclusion_inclusion {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {E F G : IntermediateField K L} (hEF : E F) (hFG : F G) (x : E) :
(inclusion hFG) ((inclusion hEF) x) = (inclusion ) x
@[simp]
theorem IntermediateField.coe_inclusion {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {E F : IntermediateField K L} (hEF : E F) (e : E) :
((inclusion hEF) e) = e
@[simp]
theorem IntermediateField.toSubalgebra_inj {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {F E : IntermediateField K L} :
@[deprecated IntermediateField.toSubalgebra_inj (since := "2024-12-29")]
theorem IntermediateField.toSubalgebra_eq_iff {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {F E : IntermediateField K L} :

Alias of IntermediateField.toSubalgebra_inj.

@[simp]
theorem IntermediateField.toSubfield_inj {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {F E : IntermediateField K L} :
theorem IntermediateField.map_injective {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') :
theorem IntermediateField.set_range_subset {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) :
Set.range (algebraMap K L) S
@[simp]
@[simp]
def IntermediateField.lift {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {F : IntermediateField K L} (E : IntermediateField K F) :

Lift an intermediate_field of an intermediate_field

Equations
theorem IntermediateField.lift_le {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {F : IntermediateField K L} (E : IntermediateField K F) :
lift E F
theorem IntermediateField.mem_lift {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {F : IntermediateField K L} {E : IntermediateField K F} (x : F) :
x lift E x E
def IntermediateField.liftAlgEquiv {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {E : IntermediateField K L} (F : IntermediateField K E) :
F ≃ₐ[K] (lift F)

The algEquiv between an intermediate field and its lift

Equations
  • One or more equations did not get rendered due to their size.
theorem IntermediateField.liftAlgEquiv_apply {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {E : IntermediateField K L} (F : IntermediateField K E) (x : F) :
((liftAlgEquiv F) x) = x
def IntermediateField.restrictScalars (K : Type u_1) {L : Type u_2} {L' : Type u_3} [Field K] [Field L] [Field L'] [Algebra K L] [Algebra K L'] [Algebra L' L] [IsScalarTower K L' L] (E : IntermediateField L' L) :

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
@[simp]
theorem IntermediateField.coe_restrictScalars (K : Type u_1) {L : Type u_2} {L' : Type u_3} [Field K] [Field L] [Field L'] [Algebra K L] [Algebra K L'] [Algebra L' L] [IsScalarTower K L' L] {E : IntermediateField L' L} :
(restrictScalars K E) = E
@[simp]
theorem IntermediateField.restrictScalars_toSubfield (K : Type u_1) {L : Type u_2} {L' : Type u_3} [Field K] [Field L] [Field L'] [Algebra K L] [Algebra K L'] [Algebra L' L] [IsScalarTower K L' L] {E : IntermediateField L' L} :
@[simp]
theorem IntermediateField.mem_restrictScalars (K : Type u_1) {L : Type u_2} {L' : Type u_3} [Field K] [Field L] [Field L'] [Algebra K L] [Algebra K L'] [Algebra L' L] [IsScalarTower K L' L] {E : IntermediateField L' L} {x : L} :
theorem IntermediateField.restrictScalars_injective (K : Type u_1) {L : Type u_2} {L' : Type u_3} [Field K] [Field L] [Field L'] [Algebra K L] [Algebra K L'] [Algebra L' L] [IsScalarTower K L' L] :
def Subfield.extendScalars {L : Type u_2} [Field L] {F E : Subfield L} (h : F E) :

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

Equations
@[simp]
theorem Subfield.coe_extendScalars {L : Type u_2} [Field L] {F E : Subfield L} (h : F E) :
(extendScalars h) = E
@[simp]
theorem Subfield.extendScalars_toSubfield {L : Type u_2} [Field L] {F E : Subfield L} (h : F E) :
@[simp]
theorem Subfield.mem_extendScalars {L : Type u_2} [Field L] {F E : Subfield L} (h : F E) {x : L} :
theorem Subfield.extendScalars_le_extendScalars_iff {L : Type u_2} [Field L] {F E E' : Subfield L} (h : F E) (h' : F E') :
theorem Subfield.extendScalars_le_iff {L : Type u_2} [Field L] {F E : Subfield L} (h : F E) (E' : IntermediateField (↥F) L) :
theorem Subfield.le_extendScalars_iff {L : Type u_2} [Field L] {F E : Subfield L} (h : F E) (E' : IntermediateField (↥F) L) :

Subfield.extendScalars.orderIso bundles Subfield.extendScalars into an order isomorphism from { E : Subfield L // F ≤ E } to IntermediateField F L. Its inverse is IntermediateField.toSubfield.

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem Subfield.extendScalars.orderIso_apply {L : Type u_2} [Field L] (F : Subfield L) (E : { E : Subfield L // F E }) :
def IntermediateField.extendScalars {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {F E : IntermediateField K L} (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
@[simp]
theorem IntermediateField.coe_extendScalars {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {F E : IntermediateField K L} (h : F E) :
(extendScalars h) = E
@[simp]
theorem IntermediateField.extendScalars_toSubfield {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {F E : IntermediateField K L} (h : F E) :
@[simp]
theorem IntermediateField.mem_extendScalars {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {F E : IntermediateField K L} (h : F E) {x : L} :
@[simp]
theorem IntermediateField.extendScalars_restrictScalars {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {F E : IntermediateField K L} (h : F E) :
theorem IntermediateField.extendScalars_le_extendScalars_iff {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {F E E' : IntermediateField K L} (h : F E) (h' : F E') :
theorem IntermediateField.extendScalars_le_iff {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {F E : IntermediateField K L} (h : F E) (E' : IntermediateField (↥F) L) :
theorem IntermediateField.le_extendScalars_iff {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {F E : IntermediateField K L} (h : F E) (E' : IntermediateField (↥F) L) :

IntermediateField.extendScalars.orderIso bundles IntermediateField.extendScalars into 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.
@[simp]
@[simp]
theorem IntermediateField.extendScalars.orderIso_apply {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (F : IntermediateField K L) (E : { E : IntermediateField K L // F E }) :
def IntermediateField.restrict {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {F E : IntermediateField K L} (h : F E) :

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

Equations
theorem IntermediateField.mem_restrict {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {F E : IntermediateField K L} (h : F E) (x : E) :
x restrict h x F
@[simp]
theorem IntermediateField.lift_restrict {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {F E : IntermediateField K L} (h : F E) :
noncomputable def IntermediateField.restrict_algEquiv {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {F E : IntermediateField K L} (h : F E) :
F ≃ₐ[K] (restrict h)

F is equivalent to F as an intermediate field of E / K.

Equations