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) [Field K] [Field L] [Algebra K L] extends Subalgebra K L : 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.carrier → b ∈ self.carrier → a * b ∈ self.carrier
• one_mem' : 1 ∈ self.carrier
• add_mem' {a b : L} : a ∈ self.carrier → b ∈ self.carrier → a + b ∈ self.carrier
• zero_mem' : 0 ∈ self.carrier
• algebraMap_mem' (r : K) : (algebraMap K L) r ∈ self.carrier
• inv_mem' (x : L) : x ∈ self.carrier → x⁻¹ ∈ self.carrier

@[implicit_reducible]

instance IntermediateField.instSetLike {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] : SetLike (IntermediateField K L) L

Equations

• IntermediateField.instSetLike = { coe := fun (S : IntermediateField K L) => S.carrier, coe_injective' := ⋯ }

@[implicit_reducible]

instance IntermediateField.instPartialOrder {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] : PartialOrder (IntermediateField K L)

Equations

• IntermediateField.instPartialOrder = PartialOrder.ofSetLike (IntermediateField K L) L

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

@[reducible]

def IntermediateField.toSubfield {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) : Subfield L

Reinterpret an IntermediateField as a Subfield.

Equations

• S.toSubfield = { toSubsemiring := S.toSubsemiring, neg_mem' := ⋯, inv_mem' := ⋯ }

instance IntermediateField.instSubfieldClass {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] : SubfieldClass (IntermediateField K L) L

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.

theorem IntermediateField.ext_iff {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {S T : IntermediateField K L} : S = T ↔ ∀ (x : L), x ∈ S ↔ x ∈ T

@[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) : x ∈ s.toSubalgebra ↔ x ∈ s

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) : x ∈ s.toSubfield ↔ x ∈ s

theorem IntermediateField.toSubalgebra_strictMono {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] : StrictMono toSubalgebra

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) : IntermediateField K L

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 ∈ S → y ∈ S → x * 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 ∈ S → y ∈ S → x + 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 ∈ S → y ∈ S → x - 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 ∈ S → x⁻¹ ∈ 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 ∈ S → y ∈ S → x / 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} : (∀ x ∈ l, 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} : (∀ x ∈ l, 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) : (∀ a ∈ m, 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) : (∀ a ∈ m, 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 : ∀ c ∈ t, f c ∈ S) : ∏ i ∈ t, 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 : ∀ c ∈ t, f c ∈ S) : ∑ i ∈ t, 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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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)⁻¹

@[simp]

theorem IntermediateField.coe_div {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

@[simp]

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

@[simp]

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

@[simp]

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

instance IntermediateField.instSMulMemClass {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] : SMulMemClass (IntermediateField K L) K L

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

Turn a subalgebra closed under inverses into an intermediate field.

Equations

• S.toIntermediateField inv_mem = { toSubalgebra := S, inv_mem' := inv_mem }

@[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 : ∀ x ∈ S, x⁻¹ ∈ S) : (S.toIntermediateField inv_mem).toSubalgebra = S

@[simp]

theorem toIntermediateField_toSubalgebra {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) : S.toIntermediateField ⋯ = S

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) : IntermediateField K L

Turn a subalgebra satisfying IsField into an intermediate field.

Equations

• S.toIntermediateField' hS = S.toIntermediateField ⋯

@[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) : (S.toIntermediateField' hS).toSubalgebra = S

@[simp]

theorem toIntermediateField'_toSubalgebra {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) : S.toIntermediateField' ⋯ = S

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) : IntermediateField K L

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' := ⋯ }

@[simp]

theorem Subfield.toIntermediateField_toSubfield {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) : (S.toIntermediateField algebra_map_mem).toSubfield = S

@[simp]

theorem Subfield.coe_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) : ↑(S.toIntermediateField algebra_map_mem) = ↑S

@[implicit_reducible]

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

• S.toField = S.toSubfield.toField

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.

@[implicit_reducible]

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

• F.instSMulSubtypeMem = { smul := fun (m : ↥F.toSubfield.toSubsemiring) (a : X) => ↑m • a }

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

@[implicit_reducible]

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

• F.instMulActionSubtypeMem = { toSemigroupAction := (Submonoid.instMulActionSubtypeMem F).toSemigroupAction, one_smul := ⋯ }

@[implicit_reducible]

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) : DistribMulAction (↥F) X

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

Equations

• F.instDistribMulActionSubtypeMem = { toMulAction := F.instMulActionSubtypeMem, smul_zero := ⋯, smul_add := ⋯ }

@[implicit_reducible]

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

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

Equations

• F.instMulDistribMulActionSubtypeMem = { toMulAction := F.instMulActionSubtypeMem, smul_mul := ⋯, smul_one := ⋯ }

@[implicit_reducible]

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

• F.instSMulWithZeroSubtypeMem = { toSMulZeroClass := (Subsemiring.instSMulWithZeroSubtypeMem F).toSMulZeroClass, zero_smul := ⋯ }

@[implicit_reducible]

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) : MulActionWithZero (↥F) X

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

Equations

• F.instMulActionWithZeroSubtypeMem = { toMulAction := F.instMulActionSubtypeMem, smul_zero := ⋯, zero_smul := ⋯ }

@[implicit_reducible]

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

• F.instModuleSubtypeMem = { toDistribMulAction := F.instDistribMulActionSubtypeMem, add_smul := ⋯, zero_smul := ⋯ }

@[implicit_reducible]

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) : MulSemiringAction (↥F) X

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

Equations

• F.instMulSemiringActionSubtypeMem = { toDistribMulAction := F.instDistribMulActionSubtypeMem, smul_one := ⋯, smul_mul := ⋯ }

IntermediateFields inherit structure from their Subalgebra coercions.

@[implicit_reducible]

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

• S.toAlgebra = { toSMul := S.instSMulSubtypeMem, algebraMap := (algebraMap L L).comp (Subsemiring.ofClass S.toSubsemiring).subtype, commutes' := ⋯, smul_def' := ⋯ }

@[implicit_reducible]

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

• S.module' = { toDistribMulAction := (SubmoduleClass.module' S).toDistribMulAction, add_smul := ⋯, zero_smul := ⋯ }

@[implicit_reducible]

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

• S.algebra' = { toSMul := DistribMulAction.toDistribSMul.toSMul, algebraMap := (algebraMap R' L).codRestrict S.toSubalgebra ⋯, commutes' := ⋯, smul_def' := ⋯ }

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} [SMul R K] [SMul 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 isScalarTower_mid to the common case where the top field is L.

@[implicit_reducible]

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

• S.instAlgebraSubtypeMem = { toSMul := S.instSMulSubtypeMem, algebraMap := (algebraMap L E).comp (Subsemiring.ofClass S.toSubsemiring).subtype, commutes' := ⋯, smul_def' := ⋯ }

@[implicit_reducible]

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

• IntermediateField.instAlgebraSubtypeMem_1 T = T.algebra

@[implicit_reducible]

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

• IntermediateField.instModuleSubtypeMem_1 T = Algebra.toModule

@[implicit_reducible]

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

• IntermediateField.instSMulSubtypeMem_1 T = (IntermediateField.instAlgebraSubtypeMem_1 T).toSMul

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') : 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

• IntermediateField.comap f S = { toSubalgebra := Subalgebra.comap f S.toSubalgebra, inv_mem' := ⋯ }

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) : 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

• IntermediateField.map f S = { toSubalgebra := Subalgebra.map f S.toSubalgebra, inv_mem' := ⋯ }

@[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') : (map f S).toSubalgebra = Subalgebra.map f S.toSubalgebra

@[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') : (map f S).toSubfield = Subfield.map (↑f) S.toSubfield

theorem IntermediateField.map_id {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) : map (AlgHom.id K L) S = S

Mapping intermediate fields along the identity does not change them.

@[simp]

theorem IntermediateField.mem_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'} {y : L'} : y ∈ map f S ↔ ∃ x ∈ S, f x = y

@[simp]

theorem IntermediateField.map_mem_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') {x : L} : f x ∈ map f S ↔ x ∈ S

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') : GaloisConnection (map f) (comap f)

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

• IntermediateField.intermediateFieldMap e E = e.subalgebraMap E.toSubalgebra

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') : IntermediateField K L'

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

Equations

• f.fieldRange = { toSubalgebra := f.range, inv_mem' := ⋯ }

@[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') : f.fieldRange.toSubalgebra = f.range

@[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') : ↑f.fieldRange = Set.range ⇑f

@[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') : f.fieldRange.toSubfield = (↑f).fieldRange

@[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

• S.val = S.val

@[simp]

theorem IntermediateField.coe_val {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) : ⇑S.val = Subtype.val

@[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) : S.val.range = S.toSubalgebra

@[simp]

theorem IntermediateField.fieldRange_val {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) : S.val.fieldRange = S

@[implicit_reducible]

instance IntermediateField.AlgHom.inhabited {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) : Inhabited (↥S →ₐ[K] L)

Equations

• IntermediateField.AlgHom.inhabited S = { default := S.val }

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} [CommSemiring 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

• IntermediateField.inclusion hEF = Subalgebra.inclusion hEF

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) : Function.Injective ⇑(inclusion hEF)

@[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

theorem IntermediateField.toSubalgebra_injective {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] : Function.Injective toSubalgebra

theorem IntermediateField.toSubfield_injective {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] : Function.Injective toSubfield

@[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} : F.toSubalgebra = E.toSubalgebra ↔ F = E

theorem IntermediateField.toSubfield_inj {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {F E : IntermediateField K L} : F.toSubfield = E.toSubfield ↔ F = E

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') : Function.Injective (map f)

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

theorem IntermediateField.fieldRange_le {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) : (algebraMap K L).fieldRange ≤ S.toSubfield

@[simp]

theorem IntermediateField.toSubalgebra_le_toSubalgebra {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {S S' : IntermediateField K L} : S.toSubalgebra ≤ S'.toSubalgebra ↔ S ≤ S'

@[simp]

theorem IntermediateField.toSubalgebra_lt_toSubalgebra {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {S S' : IntermediateField K L} : S.toSubalgebra < S'.toSubalgebra ↔ S < S'

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) : IntermediateField K L

Lift an intermediate field of an intermediate field.

Equations

• IntermediateField.lift E = IntermediateField.map F.val E

theorem IntermediateField.lift_injective {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (F : IntermediateField K L) : Function.Injective lift

@[simp]

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

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) : IntermediateField K 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

• IntermediateField.restrictScalars K E = { carrier := E.carrier, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, algebraMap_mem' := ⋯, inv_mem' := ⋯ }

@[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_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'] [Algebra L' L] [IsScalarTower K L' L] {E : IntermediateField L' L} : (restrictScalars K 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 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).toSubfield = E.toSubfield

@[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} : x ∈ restrictScalars K E ↔ x ∈ E

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] : Function.Injective (restrictScalars K)

@[simp]

theorem IntermediateField.restrictScalars_inj (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 E' : IntermediateField L' L} : restrictScalars K E = restrictScalars K E' ↔ E = E'

def IntermediateField.equivOfEq {F : Type u_4} [Field F] {E : Type u_5} [Field E] [Algebra F E] {S T : IntermediateField F E} (h : S = T) : ↥S ≃ₐ[F] ↥T

Construct an algebra isomorphism from an equality of intermediate fields.

Equations

• IntermediateField.equivOfEq h = S.equivOfEq T.toSubalgebra ⋯

@[simp]

theorem IntermediateField.equivOfEq_apply {F : Type u_4} [Field F] {E : Type u_5} [Field E] [Algebra F E] {S T : IntermediateField F E} (h : S = T) (x : ↥S.toSubalgebra) : (equivOfEq h) x = ⟨↑x, ⋯⟩

@[simp]

theorem IntermediateField.equivOfEq_symm {F : Type u_4} [Field F] {E : Type u_5} [Field E] [Algebra F E] {S T : IntermediateField F E} (h : S = T) : (equivOfEq h).symm = equivOfEq ⋯

@[simp]

theorem IntermediateField.equivOfEq_rfl {F : Type u_4} [Field F] {E : Type u_5} [Field E] [Algebra F E] (S : IntermediateField F E) : equivOfEq ⋯ = AlgEquiv.refl

@[simp]

theorem IntermediateField.equivOfEq_trans {F : Type u_4} [Field F] {E : Type u_5} [Field E] [Algebra F E] {S T U : IntermediateField F E} (hST : S = T) (hTU : T = U) : (equivOfEq hST).trans (equivOfEq hTU) = equivOfEq ⋯

theorem IntermediateField.fieldRange_comp_val {F : Type u_4} [Field F] {E : Type u_5} [Field E] [Algebra F E] {K : Type u_6} [Field K] [Algebra F K] (L : IntermediateField F E) (f : E →ₐ[F] K) : (f.comp L.val).fieldRange = map f L

noncomputable def IntermediateField.equivMap {F : Type u_4} [Field F] {E : Type u_5} [Field E] [Algebra F E] {K : Type u_6} [Field K] [Algebra F K] (L : IntermediateField F E) (f : E →ₐ[F] K) : ↥L ≃ₐ[F] ↥(map f L)

An intermediate field is isomorphic to its image under an AlgHom (which is automatically injective).

Equations

• L.equivMap f = (AlgEquiv.ofInjective (f.comp L.val) ⋯).trans (IntermediateField.equivOfEq ⋯)

@[simp]

theorem IntermediateField.coe_equivMap_apply {F : Type u_4} [Field F] {E : Type u_5} [Field E] [Algebra F E] {K : Type u_6} [Field K] [Algebra F K] (L : IntermediateField F E) (f : E →ₐ[F] K) (x : ↥L) : ↑((L.equivMap f) x) = f ↑x

def Subfield.extendScalars {L : Type u_2} [Field L] {F E : Subfield L} (h : F ≤ E) : IntermediateField (↥F) L

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

• Subfield.extendScalars h = E.toIntermediateField ⋯

@[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) : (extendScalars h).toSubfield = E

@[simp]

theorem Subfield.mem_extendScalars {L : Type u_2} [Field L] {F E : Subfield L} (h : F ≤ E) {x : L} : x ∈ extendScalars h ↔ x ∈ E

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

theorem Subfield.extendScalars_le_iff {L : Type u_2} [Field L] {F E : Subfield L} (h : F ≤ E) (E' : IntermediateField (↥F) L) : extendScalars h ≤ E' ↔ E ≤ E'.toSubfield

theorem Subfield.le_extendScalars_iff {L : Type u_2} [Field L] {F E : Subfield L} (h : F ≤ E) (E' : IntermediateField (↥F) L) : E' ≤ extendScalars h ↔ E'.toSubfield ≤ E

def Subfield.extendScalars.orderIso {L : Type u_2} [Field L] (F : Subfield L) : { E : Subfield L // F ≤ E } ≃o 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_symm_apply {L : Type u_2} [Field L] (F : Subfield L) (E : IntermediateField (↥F) L) : (RelIso.symm (orderIso F)) E = ⟨E.toSubfield, ⋯⟩

@[simp]

theorem Subfield.extendScalars.orderIso_apply {L : Type u_2} [Field L] (F : Subfield L) (E : { E : Subfield L // F ≤ E }) : (orderIso F) E = extendScalars ⋯

theorem Subfield.extendScalars_injective {L : Type u_2} [Field L] (F : Subfield L) : Function.Injective fun (E : { E : Subfield L // F ≤ E }) => extendScalars ⋯

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) : IntermediateField (↥F) L

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

• IntermediateField.extendScalars h = Subfield.extendScalars ⋯

@[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) : (extendScalars h).toSubfield = E.toSubfield

@[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} : x ∈ extendScalars h ↔ x ∈ E

@[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) : restrictScalars K (extendScalars h) = 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') : extendScalars h ≤ extendScalars h' ↔ E ≤ 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) : extendScalars h ≤ E' ↔ E ≤ restrictScalars K E'

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) : E' ≤ extendScalars h ↔ restrictScalars K E' ≤ E

def IntermediateField.extendScalars.orderIso {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (F : IntermediateField K L) : { E : IntermediateField K L // F ≤ E } ≃o 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]

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 }) : (orderIso F) E = extendScalars ⋯

@[simp]

theorem IntermediateField.extendScalars.orderIso_symm_apply_coe {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (F : IntermediateField K L) (E : IntermediateField (↥F) L) : ↑((RelIso.symm (orderIso F)) E) = restrictScalars K E

theorem IntermediateField.extendScalars_injective {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (F : IntermediateField K L) : Function.Injective fun (E : { E : IntermediateField K L // F ≤ E }) => extendScalars ⋯

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) : IntermediateField K ↥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

• IntermediateField.restrict h = (IntermediateField.inclusion h).fieldRange

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) : lift (restrict h) = F

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

• IntermediateField.restrict_algEquiv h = AlgEquiv.ofInjectiveField (IntermediateField.inclusion h)