Mathlib.FieldTheory.IntermediateField.Basic

IntermediateField structure

extends Subalgebra K L

Full source

/-- `S : IntermediateField K L` is a subset of `L` such that there is a field
tower `L / S / K`. -/
structure IntermediateField extends Subalgebra K L where
  inv_mem' : ∀ x ∈ carrier, x⁻¹ ∈ carrier

Intermediate Field

Informal description

An intermediate field between fields $ K $ and $ L $ is a subset $ S $ of $ L $ that forms a field tower $ L / S / K $. This means $ S $ is both a subfield of $ L $ and a subalgebra over $ K $, containing the image of $ K $ in $ L $.

IntermediateField.instSetLike instance

: SetLike (IntermediateField K L) L

Full source

instance : SetLike (IntermediateField K L) L :=
  ⟨fun S => S.toSubalgebra.carrier, by
    rintro ⟨⟨⟩⟩ ⟨⟨⟩⟩
    simp ⟩

Set-like Structure of Intermediate Fields

Informal description

The type of intermediate fields between fields $K$ and $L$ has a set-like structure, where each intermediate field can be viewed as a subset of $L$ with injective coercion.

IntermediateField.neg_mem theorem

{x : L} (hx : x ∈ S) : -x ∈ S

Full source

protected theorem neg_mem {x : L} (hx : x ∈ S) : -x ∈ S := by
  show -x ∈S.toSubalgebra; simpa

Additive Inverse Closure in Intermediate Fields

Informal description

For any element $x$ in an intermediate field $S$ between fields $K$ and $L$, the additive inverse $-x$ is also in $S$.

IntermediateField.toSubfield definition

: Subfield L

Full source

/-- Reinterpret an `IntermediateField` as a `Subfield`. -/
def toSubfield : Subfield L :=
  { S.toSubalgebra with
    neg_mem' := S.neg_mem,
    inv_mem' := S.inv_mem' }

Intermediate field as subfield

Informal description

The function converts an intermediate field $ S $ between fields $ K $ and $ L $ into a subfield of $ L $, preserving the additive inverse and multiplicative inverse operations.

IntermediateField.instSubfieldClass instance

: SubfieldClass (IntermediateField K L) L

Full source

instance : SubfieldClass (IntermediateField K L) L where
  add_mem {s} := s.add_mem'
  zero_mem {s} := s.zero_mem'
  neg_mem {s} := s.neg_mem
  mul_mem {s} := s.mul_mem'
  one_mem {s} := s.one_mem'
  inv_mem {s} := s.inv_mem' _

Intermediate Fields as a Subfield Class

Informal description

The type of intermediate fields between fields $K$ and $L$ forms a subclass of subfields of $L$.

IntermediateField.mem_carrier theorem

{s : IntermediateField K L} {x : L} : x ∈ s.carrier ↔ x ∈ s

Full source

theorem mem_carrier {s : IntermediateField K L} {x : L} : x ∈ s.carrierx ∈ s.carrier ↔ x ∈ s :=
  Iff.rfl

Membership in Intermediate Field Carrier Set

Informal description

For any intermediate field $S$ between fields $K$ and $L$, and any element $x \in L$, we have $x$ belongs to the carrier set of $S$ if and only if $x$ belongs to $S$.

IntermediateField.ext theorem

{S T : IntermediateField K L} (h : ∀ x, x ∈ S ↔ x ∈ T) : S = T

Full source

/-- Two intermediate fields are equal if they have the same elements. -/
@[ext]
theorem ext {S T : IntermediateField K L} (h : ∀ x, x ∈ Sx ∈ S ↔ x ∈ T) : S = T :=
  SetLike.ext h

Extensionality of Intermediate Fields: $S = T \iff \forall x \in L, x \in S \leftrightarrow x \in T$

Informal description

Two intermediate fields $S$ and $T$ between fields $K$ and $L$ are equal if and only if they contain exactly the same elements, i.e., for every $x \in L$, $x \in S$ if and only if $x \in T$.

IntermediateField.coe_toSubalgebra theorem

: (S.toSubalgebra : Set L) = S

Full source

@[simp]
theorem coe_toSubalgebra : (S.toSubalgebra : Set L) = S :=
  rfl

Equality of Intermediate Field and Subalgebra Carrier Sets

Informal description

For any intermediate field $S$ between $K$ and $L$, the underlying set of $S$ (viewed as a subalgebra) is equal to $S$ itself as a set in $L$.

IntermediateField.coe_toSubfield theorem

: (S.toSubfield : Set L) = S

Full source

@[simp]
theorem coe_toSubfield : (S.toSubfield : Set L) = S :=
  rfl

Equality of Intermediate Field and Subfield Carrier Sets

Informal description

For any intermediate field $S$ between fields $K$ and $L$, the underlying set of $S$ (viewed as a subfield) is equal to $S$ itself as a set in $L$.

IntermediateField.coe_type_toSubalgebra theorem

: (S.toSubalgebra : Type _) = S

Full source

@[simp]
theorem coe_type_toSubalgebra : (S.toSubalgebra : Type _) = S :=
  rfl

Type Equality of Intermediate Field and Subalgebra

Informal description

For any intermediate field $S$ between fields $K$ and $L$, the type associated with $S$ viewed as a subalgebra is equal to $S$ itself as a type.

IntermediateField.coe_type_toSubfield theorem

: (S.toSubfield : Type _) = S

Full source

@[simp]
theorem coe_type_toSubfield : (S.toSubfield : Type _) = S :=
  rfl

Type Equality of Intermediate Field and Subfield

Informal description

For any intermediate field $S$ between fields $K$ and $L$, the type associated with $S$ viewed as a subfield is equal to $S$ itself as a type.

IntermediateField.mem_mk theorem

 (s : Subsemiring L) (hK : ∀ x, algebraMap K L x ∈ s) (hi) (x : L) :
  x ∈ IntermediateField.mk (Subalgebra.mk s hK) hi ↔ x ∈ s

Full source

@[simp]
theorem mem_mk (s : Subsemiring L) (hK : ∀ x, algebraMapalgebraMap K L x ∈ s) (hi) (x : L) :
    x ∈ IntermediateField.mk (Subalgebra.mk s hK) hix ∈ IntermediateField.mk (Subalgebra.mk s hK) hi ↔ x ∈ s :=
  Iff.rfl

Membership Criterion for Constructed Intermediate Field

Informal description

Let $s$ be a subsemiring of $L$ such that for every $x \in K$, the image of $x$ under the algebra map $K \to L$ lies in $s$. Let $S$ be the intermediate field constructed from the subalgebra generated by $s$ and the condition $hi$. Then for any $x \in L$, we have $x \in S$ if and only if $x \in s$.

IntermediateField.mem_toSubalgebra theorem

(s : IntermediateField K L) (x : L) : x ∈ s.toSubalgebra ↔ x ∈ s

Full source

@[simp]
theorem mem_toSubalgebra (s : IntermediateField K L) (x : L) : x ∈ s.toSubalgebrax ∈ s.toSubalgebra ↔ x ∈ s :=
  Iff.rfl

Membership in Intermediate Field and its Subalgebra Coincide

Informal description

For any intermediate field $S$ between fields $K$ and $L$, and any element $x \in L$, we have $x \in S$ if and only if $x$ belongs to the underlying subalgebra of $S$.

IntermediateField.mem_toSubfield theorem

(s : IntermediateField K L) (x : L) : x ∈ s.toSubfield ↔ x ∈ s

Full source

@[simp]
theorem mem_toSubfield (s : IntermediateField K L) (x : L) : x ∈ s.toSubfieldx ∈ s.toSubfield ↔ x ∈ s :=
  Iff.rfl

Membership in Intermediate Field and its Subfield Coincide

Informal description

For any intermediate field $S$ between fields $K$ and $L$, and any element $x \in L$, we have $x \in S$ if and only if $x$ belongs to the underlying subfield of $S$.

IntermediateField.copy definition

(S : IntermediateField K L) (s : Set L) (hs : s = ↑S) : IntermediateField K L

Full source

/-- Copy of an intermediate field with a new `carrier` equal to the old one. Useful to fix
definitional equalities. -/
protected def copy (S : IntermediateField K L) (s : Set L) (hs : s = ↑S) :
    IntermediateField K L where
  toSubalgebra := S.toSubalgebra.copy s hs
  inv_mem' := hs.symm ▸ S.inv_mem'

Copy of an intermediate field with a specified carrier set

Informal description

Given an intermediate field $ S $ between fields $ K $ and $ L $, and a subset $ s $ of $ L $ that is definitionally equal to the carrier set of $ S $, the function `IntermediateField.copy` constructs a new intermediate field with carrier set $ s $. This is useful for fixing definitional equalities while preserving the field structure.

IntermediateField.coe_copy theorem

(S : IntermediateField K L) (s : Set L) (hs : s = ↑S) : (S.copy s hs : Set L) = s

Full source

@[simp]
theorem coe_copy (S : IntermediateField K L) (s : Set L) (hs : s = ↑S) :
    (S.copy s hs : Set L) = s :=
  rfl

Carrier Set Equality for Copied Intermediate Field

Informal description

Let $S$ be an intermediate field between fields $K$ and $L$, and let $s$ be a subset of $L$ such that $s = S$ (as sets). Then the carrier set of the intermediate field $S.\text{copy}(s, hs)$ is equal to $s$.

IntermediateField.copy_eq theorem

(S : IntermediateField K L) (s : Set L) (hs : s = ↑S) : S.copy s hs = S

Full source

theorem copy_eq (S : IntermediateField K L) (s : Set L) (hs : s = ↑S) : S.copy s hs = S :=
  SetLike.coe_injective hs

Copy of Intermediate Field Equals Original

Informal description

Let $S$ be an intermediate field between fields $K$ and $L$, and let $s$ be a subset of $L$ such that $s$ equals the underlying set of $S$. Then the copy of $S$ with carrier set $s$ is equal to $S$ itself.

IntermediateField.algebraMap_mem theorem

(x : K) : algebraMap K L x ∈ S

Full source

/-- An intermediate field contains the image of the smaller field. -/
theorem algebraMap_mem (x : K) : algebraMapalgebraMap K L x ∈ S :=
  S.algebraMap_mem' x

Algebra Map Image in Intermediate Field

Informal description

For any intermediate field $S$ between fields $K$ and $L$, and for any element $x \in K$, the image of $x$ under the algebra map from $K$ to $L$ lies in $S$. That is, $\text{algebraMap}_{K,L}(x) \in S$.

IntermediateField.smul_mem theorem

{y : L} : y ∈ S → ∀ {x : K}, x • y ∈ S

Full source

/-- An intermediate field is closed under scalar multiplication. -/
theorem smul_mem {y : L} : y ∈ S → ∀ {x : K}, x • y ∈ S :=
  S.toSubalgebra.smul_mem

Closure of Intermediate Field under Scalar Multiplication

Informal description

Let $S$ be an intermediate field between fields $K$ and $L$. For any element $y \in S$ and any scalar $x \in K$, the scalar multiple $x \cdot y$ is also in $S$.

IntermediateField.one_mem theorem

: (1 : L) ∈ S

Full source

/-- An intermediate field contains the ring's 1. -/
protected theorem one_mem : (1 : L) ∈ S :=
  one_mem S

Multiplicative Identity in Intermediate Field

Informal description

For any intermediate field $S$ between fields $K$ and $L$, the multiplicative identity $1 \in L$ is contained in $S$.

IntermediateField.zero_mem theorem

: (0 : L) ∈ S

Full source

/-- An intermediate field contains the ring's 0. -/
protected theorem zero_mem : (0 : L) ∈ S :=
  zero_mem S

Zero Element Belongs to Intermediate Field

Informal description

For any intermediate field $S$ between fields $K$ and $L$, the zero element $0$ of $L$ is contained in $S$.

IntermediateField.mul_mem theorem

{x y : L} : x ∈ S → y ∈ S → x * y ∈ S

Full source

/-- An intermediate field is closed under multiplication. -/
protected theorem mul_mem {x y : L} : x ∈ S → y ∈ S → x * y ∈ S :=
  mul_mem

Closure of Intermediate Field under Multiplication

Informal description

For any intermediate field $S$ between fields $K$ and $L$, and for any elements $x, y \in L$, if $x \in S$ and $y \in S$, then their product $x \cdot y$ also belongs to $S$.

IntermediateField.add_mem theorem

{x y : L} : x ∈ S → y ∈ S → x + y ∈ S

Full source

/-- An intermediate field is closed under addition. -/
protected theorem add_mem {x y : L} : x ∈ S → y ∈ S → x + y ∈ S :=
  add_mem

Closure of Intermediate Field under Addition

Informal description

For any intermediate field $S$ between fields $K$ and $L$, and for any elements $x, y \in L$, if $x \in S$ and $y \in S$, then $x + y \in S$.

IntermediateField.sub_mem theorem

{x y : L} : x ∈ S → y ∈ S → x - y ∈ S

Full source

/-- An intermediate field is closed under subtraction -/
protected theorem sub_mem {x y : L} : x ∈ S → y ∈ S → x - y ∈ S :=
  sub_mem

Intermediate Field is Closed Under Subtraction

Informal description

For any intermediate field $S$ between fields $K$ and $L$, and for any elements $x, y \in L$, if $x \in S$ and $y \in S$, then their difference $x - y$ also belongs to $S$.

IntermediateField.inv_mem theorem

{x : L} : x ∈ S → x⁻¹ ∈ S

Full source

/-- An intermediate field is closed under inverses. -/
protected theorem inv_mem {x : L} : x ∈ S → x⁻¹x⁻¹ ∈ S :=
  inv_mem

Closure of Intermediate Field under Inversion

Informal description

For any intermediate field $S$ between fields $K$ and $L$, and for any element $x \in L$, if $x \in S$, then its multiplicative inverse $x^{-1}$ also belongs to $S$.

IntermediateField.div_mem theorem

{x y : L} : x ∈ S → y ∈ S → x / y ∈ S

Full source

/-- An intermediate field is closed under division. -/
protected theorem div_mem {x y : L} : x ∈ S → y ∈ S → x / y ∈ S :=
  div_mem

Intermediate Field is Closed Under Division

Informal description

For any intermediate field $S$ between fields $K$ and $L$, and for any elements $x, y \in L$, if $x \in S$ and $y \in S$, then their quotient $x / y$ also belongs to $S$.

IntermediateField.list_prod_mem theorem

{l : List L} : (∀ x ∈ l, x ∈ S) → l.prod ∈ S

Full source

/-- Product of a list of elements in an intermediate_field is in the intermediate_field. -/
protected theorem list_prod_mem {l : List L} : (∀ x ∈ l, x ∈ S) → l.prod ∈ S :=
  list_prod_mem

Product of List Elements in Intermediate Field Belongs to Intermediate Field

Informal description

Let $L/K$ be a field extension and $S$ an intermediate field between $K$ and $L$. For any list $l$ of elements in $L$, if every element $x \in l$ belongs to $S$, then the product of all elements in $l$ (computed in $L$) also belongs to $S$.

IntermediateField.list_sum_mem theorem

{l : List L} : (∀ x ∈ l, x ∈ S) → l.sum ∈ S

Full source

/-- Sum of a list of elements in an intermediate field is in the intermediate_field. -/
protected theorem list_sum_mem {l : List L} : (∀ x ∈ l, x ∈ S) → l.sum ∈ S :=
  list_sum_mem

Sum of List Elements in Intermediate Field

Informal description

For any list $l$ of elements in a field extension $L$ of $K$, if every element $x$ in $l$ belongs to an intermediate field $S$ between $K$ and $L$, then the sum of all elements in $l$ also belongs to $S$.

IntermediateField.multiset_prod_mem theorem

(m : Multiset L) : (∀ a ∈ m, a ∈ S) → m.prod ∈ S

Full source

/-- Product of a multiset of elements in an intermediate field is in the intermediate_field. -/
protected theorem multiset_prod_mem (m : Multiset L) : (∀ a ∈ m, a ∈ S) → m.prod ∈ S :=
  multiset_prod_mem m

Product of Multiset in Intermediate Field is in Intermediate Field

Informal description

Let $S$ be an intermediate field between fields $K$ and $L$. For any multiset $m$ of elements in $L$, if every element $a \in m$ belongs to $S$, then the product of all elements in $m$ (computed in $L$) also belongs to $S$.

IntermediateField.multiset_sum_mem theorem

(m : Multiset L) : (∀ a ∈ m, a ∈ S) → m.sum ∈ S

Full source

/-- Sum of a multiset of elements in an `IntermediateField` is in the `IntermediateField`. -/
protected theorem multiset_sum_mem (m : Multiset L) : (∀ a ∈ m, a ∈ S) → m.sum ∈ S :=
  multiset_sum_mem m

Sum of Multiset Elements in Intermediate Field

Informal description

Let $L/K$ be a field extension and let $S$ be an intermediate field between $K$ and $L$. For any multiset $m$ of elements of $L$, if every element of $m$ belongs to $S$, then the sum of all elements in $m$ also belongs to $S$.

IntermediateField.prod_mem theorem

{ι : Type*} {t : Finset ι} {f : ι → L} (h : ∀ c ∈ t, f c ∈ S) : (∏ i ∈ t, f i) ∈ S

Full source

/-- Product of elements of an intermediate field indexed by a `Finset` is in the intermediate_field.
-/
protected theorem prod_mem {ι : Type*} {t : Finset ι} {f : ι → L} (h : ∀ c ∈ t, f c ∈ S) :
    (∏ i ∈ t, f i) ∈ S :=
  prod_mem h

Product of Intermediate Field Elements over a Finite Set Belongs to Intermediate Field

Informal description

Let $K \subseteq L$ be a field extension and $S$ an intermediate field between $K$ and $L$. For any finite index set $t$ and function $f : \iota \to L$, if $f(c) \in S$ for every $c \in t$, then the product $\prod_{i \in t} f(i)$ belongs to $S$.

IntermediateField.sum_mem theorem

{ι : Type*} {t : Finset ι} {f : ι → L} (h : ∀ c ∈ t, f c ∈ S) : (∑ i ∈ t, f i) ∈ S

Full source

/-- Sum of elements in an `IntermediateField` indexed by a `Finset` is in the `IntermediateField`.
-/
protected theorem sum_mem {ι : Type*} {t : Finset ι} {f : ι → L} (h : ∀ c ∈ t, f c ∈ S) :
    (∑ i ∈ t, f i) ∈ S :=
  sum_mem h

Sum of Intermediate Field Elements is in Intermediate Field

Informal description

Let $K$ and $L$ be fields with $L$ an extension of $K$, and let $S$ be an intermediate field between $K$ and $L$. For any finite set $t$ (indexed by type $\iota$) and function $f : \iota \to L$ such that $f(c) \in S$ for all $c \in t$, the sum $\sum_{i \in t} f(i)$ belongs to $S$.

IntermediateField.pow_mem theorem

{x : L} (hx : x ∈ S) (n : ℤ) : x ^ n ∈ S

Full source

protected theorem pow_mem {x : L} (hx : x ∈ S) (n : ℤ) : x ^ n ∈ S :=
  zpow_mem hx n

Closure of Intermediate Fields under Integer Powers

Informal description

Let $L/K$ be a field extension and let $S$ be an intermediate field between $K$ and $L$. For any element $x \in S$ and any integer $n$, the power $x^n$ belongs to $S$.

IntermediateField.zsmul_mem theorem

{x : L} (hx : x ∈ S) (n : ℤ) : n • x ∈ S

Full source

protected theorem zsmul_mem {x : L} (hx : x ∈ S) (n : ℤ) : n • x ∈ S :=
  zsmul_mem hx n

Closure of Intermediate Field under Integer Scalar Multiplication

Informal description

For any element $x$ in an intermediate field $S$ between fields $K$ and $L$, and for any integer $n$, the scalar multiple $n \cdot x$ is also in $S$.

IntermediateField.intCast_mem theorem

(n : ℤ) : (n : L) ∈ S

Full source

protected theorem intCast_mem (n : ℤ) : (n : L) ∈ S :=
  intCast_mem S n

Integer Elements Belong to Intermediate Field

Informal description

For any integer $n$, the canonical image of $n$ in $L$ is contained in the intermediate field $S$ between $K$ and $L$.

IntermediateField.coe_add theorem

(x y : S) : (↑(x + y) : L) = ↑x + ↑y

Full source

protected theorem coe_add (x y : S) : (↑(x + y) : L) = ↑x + ↑y :=
  rfl

Addition in Intermediate Field Coerces to Addition in Extension Field

Informal description

For any elements $x$ and $y$ in an intermediate field $S$ between fields $K$ and $L$, the coercion of their sum $x + y$ in $L$ equals the sum of their coercions in $L$, i.e., $(x + y) = x + y$ where the left-hand side is interpreted in $L$.

IntermediateField.coe_neg theorem

(x : S) : (↑(-x) : L) = -↑x

Full source

protected theorem coe_neg (x : S) : (↑(-x) : L) = -↑x :=
  rfl

Negation Commutes with Coercion in Intermediate Fields

Informal description

For any element $x$ in an intermediate field $S$ between fields $K$ and $L$, the coercion of the negation of $x$ to $L$ equals the negation of the coercion of $x$ to $L$, i.e., $(-x : L) = - (x : L)$.

IntermediateField.coe_mul theorem

(x y : S) : (↑(x * y) : L) = ↑x * ↑y

Full source

protected theorem coe_mul (x y : S) : (↑(x * y) : L) = ↑x * ↑y :=
  rfl

Coercion Preserves Multiplication in Intermediate Fields

Informal description

For any elements $x, y$ in an intermediate field $S$ between fields $K$ and $L$, the coercion of their product $x \cdot y$ in $L$ equals the product of their coercions in $L$, i.e., $(x \cdot y)_L = x_L \cdot y_L$.

IntermediateField.coe_inv theorem

(x : S) : (↑x⁻¹ : L) = (↑x)⁻¹

Full source

protected theorem coe_inv (x : S) : (↑x⁻¹ : L) = (↑x)⁻¹ :=
  rfl

Preservation of Multiplicative Inverse in Intermediate Field Inclusion

Informal description

For any element $x$ in an intermediate field $S$ between fields $K$ and $L$, the canonical inclusion map from $S$ to $L$ preserves the multiplicative inverse operation, i.e., the image of $x^{-1}$ in $L$ equals the inverse of the image of $x$ in $L$. In symbols, this is expressed as $\iota(x^{-1}) = (\iota(x))^{-1}$, where $\iota$ denotes the inclusion map from $S$ to $L$.

IntermediateField.coe_zero theorem

: ((0 : S) : L) = 0

Full source

protected theorem coe_zero : ((0 : S) : L) = 0 :=
  rfl

Inclusion of Zero in Intermediate Fields

Informal description

For any intermediate field $S$ between fields $K$ and $L$, the zero element of $S$ maps to the zero element of $L$ under the canonical inclusion map.

IntermediateField.coe_one theorem

: ((1 : S) : L) = 1

Full source

protected theorem coe_one : ((1 : S) : L) = 1 :=
  rfl

Preservation of multiplicative identity in intermediate field inclusion

Informal description

For any intermediate field $S$ between fields $K$ and $L$, the image of the multiplicative identity $1 \in S$ under the canonical inclusion map $S \hookrightarrow L$ equals the multiplicative identity $1 \in L$. In other words, the coercion of $1_S$ to $L$ is $1_L$.

IntermediateField.coe_pow theorem

(x : S) (n : ℕ) : (↑(x ^ n : S) : L) = (x : L) ^ n

Full source

protected theorem coe_pow (x : S) (n : ℕ) : (↑(x ^ n : S) : L) = (x : L) ^ n :=
  SubmonoidClass.coe_pow x n

Power Operation Consistency in Intermediate Fields: $(x^n)_S = x^n_L$

Informal description

For any intermediate field $S$ between fields $K$ and $L$, any element $x \in S$, and any natural number $n$, the $n$-th power of $x$ in $S$ (when viewed as an element of $L$) equals the $n$-th power of $x$ in $L$. In symbols: $(x^n)_S = x^n_L$.

IntermediateField.natCast_mem theorem

(n : ℕ) : (n : L) ∈ S

Full source

theorem natCast_mem (n : ℕ) : (n : L) ∈ S := by simpa using intCast_mem S n

Natural Numbers Belong to Intermediate Field

Informal description

For any natural number $n$, the canonical image of $n$ in $L$ is an element of the intermediate field $S$ between $K$ and $L$.

IntermediateField.instSMulMemClass instance

: SMulMemClass (IntermediateField K L) K L

Full source

instance instSMulMemClass : SMulMemClass (IntermediateField K L) K L where
  smul_mem := fun _ _ hx ↦ IntermediateField.smul_mem _ hx

Closure of Intermediate Fields under Scalar Multiplication

Informal description

Every intermediate field $S$ between fields $K$ and $L$ is closed under scalar multiplication by elements of $K$. That is, for any $x \in K$ and $y \in S$, the scalar multiple $x \cdot y$ is also in $S$.

Subalgebra.toIntermediateField definition

(S : Subalgebra K L) (inv_mem : ∀ x ∈ S, x⁻¹ ∈ S) : IntermediateField K L

Full source

/-- Turn a subalgebra closed under inverses into an intermediate field -/
def Subalgebra.toIntermediateField (S : Subalgebra K L) (inv_mem : ∀ x ∈ S, x⁻¹ ∈ S) :
    IntermediateField K L :=
  { S with
    inv_mem' := inv_mem }

Subalgebra to intermediate field conversion

Informal description

Given a subalgebra $ S $ of $ L $ over $ K $ that is closed under multiplicative inverses (i.e., for every $ x \in S $, $ x^{-1} \in S $), the function `Subalgebra.toIntermediateField` constructs an intermediate field between $ K $ and $ L $ from $ S $.

toSubalgebra_toIntermediateField theorem

(S : Subalgebra K L) (inv_mem : ∀ x ∈ S, x⁻¹ ∈ S) : (S.toIntermediateField inv_mem).toSubalgebra = S

Full source

@[simp]
theorem toSubalgebra_toIntermediateField (S : Subalgebra K L) (inv_mem : ∀ x ∈ S, x⁻¹ ∈ S) :
    (S.toIntermediateField inv_mem).toSubalgebra = S := by
  ext
  rfl

Subalgebra Structure Preservation in Intermediate Field Construction

Informal description

Let $K$ and $L$ be fields with $K \subseteq L$, and let $S$ be a $K$-subalgebra of $L$ that is closed under taking inverses (i.e., for every $x \in S$, $x^{-1} \in S$). Then the subalgebra structure of the intermediate field obtained from $S$ via `Subalgebra.toIntermediateField` is equal to $S$ itself.

toIntermediateField_toSubalgebra theorem

(S : IntermediateField K L) : (S.toSubalgebra.toIntermediateField fun _ => S.inv_mem) = S

Full source

@[simp]
theorem toIntermediateField_toSubalgebra (S : IntermediateField K L) :
    (S.toSubalgebra.toIntermediateField fun _ => S.inv_mem) = S := by
  ext
  rfl

Intermediate Field-Subalgebra Roundtrip Identity

Informal description

For any intermediate field $S$ between fields $K$ and $L$, the intermediate field obtained by first converting $S$ to a subalgebra and then back to an intermediate field (using the closure under inverses property of $S$) is equal to $S$ itself.

Subalgebra.toIntermediateField' definition

(S : Subalgebra K L) (hS : IsField S) : IntermediateField K L

Full source

/-- Turn a subalgebra satisfying `IsField` into an intermediate_field -/
def Subalgebra.toIntermediateField' (S : Subalgebra K L) (hS : IsField S) : IntermediateField K L :=
  S.toIntermediateField fun x hx => by
    by_cases hx0 : x = 0
    · rw [hx0, inv_zero]
      exact S.zero_mem
    letI hS' := hS.toField
    obtain ⟨y, hy⟩ := hS.mul_inv_cancel (show (⟨x, hx⟩ : S) ≠ 0 from Subtype.coe_ne_coe.1 hx0)
    rw [Subtype.ext_iff, S.coe_mul, S.coe_one, Subtype.coe_mk, mul_eq_one_iff_inv_eq₀ hx0] at hy
    exact hy.symm ▸ y.2

Conversion of a field subalgebra to an intermediate field

Informal description

Given a subalgebra $ S $ of $ L $ over $ K $ that is a field (i.e., $ S $ satisfies `IsField`), the function `Subalgebra.toIntermediateField'` constructs an intermediate field between $ K $ and $ L $ from $ S $. Specifically, for any nonzero element $ x \in S $, its multiplicative inverse $ x^{-1} $ also lies in $ S $.

toSubalgebra_toIntermediateField' theorem

(S : Subalgebra K L) (hS : IsField S) : (S.toIntermediateField' hS).toSubalgebra = S

Full source

@[simp]
theorem toSubalgebra_toIntermediateField' (S : Subalgebra K L) (hS : IsField S) :
    (S.toIntermediateField' hS).toSubalgebra = S := by
  ext
  rfl

Subalgebra-Intermediate Field Roundtrip Equality

Informal description

Let $K$ be a field and $L$ a field extension of $K$. For any subalgebra $S$ of $L$ over $K$ that is itself a field, the subalgebra obtained from the intermediate field constructed from $S$ is equal to $S$ itself. In other words, the composition of `toIntermediateField'` followed by `toSubalgebra` is the identity on $S$.

toIntermediateField'_toSubalgebra theorem

(S : IntermediateField K L) : S.toSubalgebra.toIntermediateField' (Field.toIsField S) = S

Full source

@[simp]
theorem toIntermediateField'_toSubalgebra (S : IntermediateField K L) :
    S.toSubalgebra.toIntermediateField' (Field.toIsField S) = S := by
  ext
  rfl

Intermediate Field to Subalgebra and Back is Identity

Informal description

For any intermediate field $S$ between fields $K$ and $L$, the composition of converting $S$ to a subalgebra and then back to an intermediate field (via `Subalgebra.toIntermediateField'`) yields $S$ itself. In other words, $S.\text{toSubalgebra}.\text{toIntermediateField}' (\text{Field.toIsField } S) = S$.

Subfield.toIntermediateField definition

(S : Subfield L) (algebra_map_mem : ∀ x, algebraMap K L x ∈ S) : IntermediateField K L

Full source

/-- Turn a subfield of `L` containing the image of `K` into an intermediate field -/
def Subfield.toIntermediateField (S : Subfield L) (algebra_map_mem : ∀ x, algebraMapalgebraMap K L x ∈ S) :
    IntermediateField K L :=
  { S with
    algebraMap_mem' := algebra_map_mem }

Subfield to Intermediate Field Construction

Informal description

Given a subfield $ S $ of $ L $ that contains the image of the algebra map $ K \to L $, this function constructs an intermediate field between $ K $ and $ L $ by equipping $ S $ with the necessary structure inherited from being both a subfield of $ L $ and a subalgebra over $ K $.

IntermediateField.toField instance

: Field S

Full source

/-- An intermediate field inherits a field structure -/
instance toField : Field S :=
  S.toSubfield.toField

Field Structure on Intermediate Fields

Informal description

For any intermediate field $S$ between fields $K$ and $L$, $S$ inherits a field structure from $L$.

IntermediateField.coe_sum theorem

{ι : Type*} [Fintype ι] (f : ι → S) : (↑(∑ i, f i) : L) = ∑ i, (f i : L)

Full source

@[norm_cast]
theorem coe_sum {ι : Type*} [Fintype ι] (f : ι → S) : (↑(∑ i, f i) : L) = ∑ i, (f i : L) := by
  classical
    induction' (Finset.univ : Finset ι) using Finset.induction_on with i s hi H
    · simp
    · rw [Finset.sum_insert hi, AddMemClass.coe_add, H, Finset.sum_insert hi]

Sum Inclusion in Intermediate Fields

Informal description

Let $S$ be an intermediate field between fields $K$ and $L$, and let $\iota$ be a finite type. For any function $f \colon \iota \to S$, the image of the sum $\sum_{i} f(i)$ under the inclusion map $S \hookrightarrow L$ equals the sum $\sum_{i} (f(i) \colon L)$ in $L$.

IntermediateField.coe_prod theorem

{ι : Type*} [Fintype ι] (f : ι → S) : (↑(∏ i, f i) : L) = ∏ i, (f i : L)

Full source

@[norm_cast]
theorem coe_prod {ι : Type*} [Fintype ι] (f : ι → S) : (↑(∏ i, f i) : L) = ∏ i, (f i : L) := by
  classical
    induction' (Finset.univ : Finset ι) using Finset.induction_on with i s hi H
    · simp
    · rw [Finset.prod_insert hi, MulMemClass.coe_mul, H, Finset.prod_insert hi]

Inclusion of Intermediate Field Preserves Finite Products

Informal description

For any finite type $\iota$ and any function $f \colon \iota \to S$ from $\iota$ to an intermediate field $S$ between $K$ and $L$, the canonical inclusion map from $S$ to $L$ preserves products. That is, the image of the product $\prod_{i} f(i)$ in $S$ under the inclusion map equals the product $\prod_{i} (f(i) : L)$ in $L$.

IntermediateField.instSMulSubtypeMem instance

[SMul L X] (F : IntermediateField K L) : SMul F X

Full source

/-- The action by an intermediate field is the action by the underlying field. -/
instance [SMul L X] (F : IntermediateField K L) : SMul F X :=
  inferInstanceAs (SMul F.toSubfield X)

Scalar Multiplication Action on Intermediate Fields

Informal description

For any field extension $L/K$ and any intermediate field $F$ between $K$ and $L$, if $L$ has a scalar multiplication action on a type $X$, then $F$ inherits a scalar multiplication action on $X$ via the inclusion $F \subseteq L$.

IntermediateField.smul_def theorem

[SMul L X] {F : IntermediateField K L} (g : F) (m : X) : g • m = (g : L) • m

Full source

theorem smul_def [SMul L X] {F : IntermediateField K L} (g : F) (m : X) : g • m = (g : L) • m :=
  rfl

Scalar Multiplication in Intermediate Field Equals Scalar Multiplication in Extension Field

Informal description

Let $L/K$ be a field extension, and let $F$ be an intermediate field between $K$ and $L$. Suppose $L$ has a scalar multiplication action on a type $X$. Then for any element $g \in F$ and any $m \in X$, the scalar multiplication $g \cdot m$ in $F$ is equal to the scalar multiplication $(g : L) \cdot m$ in $L$, where $(g : L)$ denotes the inclusion of $g$ into $L$.

IntermediateField.smulCommClass_left instance

[SMul L Y] [SMul X Y] [SMulCommClass L X Y] (F : IntermediateField K L) : SMulCommClass F X Y

Full source

instance smulCommClass_left [SMul L Y] [SMul X Y] [SMulCommClass L X Y]
    (F : IntermediateField K L) : SMulCommClass F X Y :=
  inferInstanceAs (SMulCommClass F.toSubfield X Y)

Commutativity of Scalar Multiplication for Intermediate Fields and $X$ on $Y$

Informal description

For any field extension $L/K$ and any intermediate field $F$ between $K$ and $L$, if $L$ has a scalar multiplication action on a type $Y$, and $X$ also has a scalar multiplication action on $Y$ such that the actions of $L$ and $X$ on $Y$ commute (i.e., for all $l \in L$, $x \in X$, $y \in Y$, we have $l \cdot (x \cdot y) = x \cdot (l \cdot y)$), then the actions of $F$ and $X$ on $Y$ also commute.

IntermediateField.smulCommClass_right instance

[SMul X Y] [SMul L Y] [SMulCommClass X L Y] (F : IntermediateField K L) : SMulCommClass X F Y

Full source

instance smulCommClass_right [SMul X Y] [SMul L Y] [SMulCommClass X L Y]
    (F : IntermediateField K L) : SMulCommClass X F Y :=
  inferInstanceAs (SMulCommClass X F.toSubfield Y)

Commutativity of Scalar Multiplication with Intermediate Fields

Informal description

For any field extension $L/K$ and intermediate field $F$ between $K$ and $L$, if there is a scalar multiplication action of $X$ on $Y$ and of $L$ on $Y$ such that the actions of $X$ and $L$ on $Y$ commute, then the actions of $X$ and $F$ on $Y$ also commute.

IntermediateField.instIsScalarTowerSubtypeMem instance

[SMul X Y] [SMul L X] [SMul L Y] [IsScalarTower L X Y] (F : IntermediateField K L) : IsScalarTower F X Y

Full source

/-- Note that this provides `IsScalarTower F K K` which is needed by `smul_mul_assoc`. -/
instance (priority := 900) [SMul X Y] [SMul L X] [SMul L Y] [IsScalarTower L X Y]
    (F : IntermediateField K L) : IsScalarTower F X Y :=
  inferInstanceAs (IsScalarTower F.toSubfield X Y)

Intermediate Fields Inherit Scalar Tower Structure

Informal description

For any field extension $L/K$ and intermediate field $F$ between $K$ and $L$, if $L$ acts as a scalar tower on types $X$ and $Y$ (i.e., the scalar multiplication operations satisfy the compatibility condition $(l \cdot x) \cdot y = l \cdot (x \cdot y)$ for all $l \in L$, $x \in X$, $y \in Y$), then $F$ also acts as a scalar tower on $X$ and $Y$.

IntermediateField.instFaithfulSMulSubtypeMem instance

[SMul L X] [FaithfulSMul L X] (F : IntermediateField K L) : FaithfulSMul F X

Full source

instance [SMul L X] [FaithfulSMul L X] (F : IntermediateField K L) : FaithfulSMul F X :=
  inferInstanceAs (FaithfulSMul F.toSubfield X)

Faithfulness of Scalar Multiplication Restricted to Intermediate Fields

Informal description

For any field extension $L/K$, intermediate field $F$ between $K$ and $L$, and type $X$ with a scalar multiplication action by $L$, if the action of $L$ on $X$ is faithful (i.e., distinct elements of $L$ act differently on $X$), then the restricted action of $F$ on $X$ is also faithful.

IntermediateField.instMulActionSubtypeMem instance

[MulAction L X] (F : IntermediateField K L) : MulAction F X

Full source

/-- The action by an intermediate field is the action by the underlying field. -/
instance [MulAction L X] (F : IntermediateField K L) : MulAction F X :=
  inferInstanceAs (MulAction F.toSubfield X)

Restriction of Multiplicative Action to Intermediate Fields

Informal description

For any intermediate field $F$ between fields $K$ and $L$, and any type $X$ with a multiplicative action by $L$, the multiplicative action on $X$ restricts to a multiplicative action by $F$.

IntermediateField.instDistribMulActionSubtypeMem instance

[AddMonoid X] [DistribMulAction L X] (F : IntermediateField K L) : DistribMulAction F X

Full source

/-- The action by an intermediate field is the action by the underlying field. -/
instance [AddMonoid X] [DistribMulAction L X] (F : IntermediateField K L) : DistribMulAction F X :=
  inferInstanceAs (DistribMulAction F.toSubfield X)

Distributive Multiplicative Action on Intermediate Fields

Informal description

For any field extension $L/K$, an intermediate field $F$ between $K$ and $L$, and an additive monoid $X$ equipped with a distributive multiplicative action by $L$, the intermediate field $F$ inherits a distributive multiplicative action on $X$.

IntermediateField.instMulDistribMulActionSubtypeMem instance

[Monoid X] [MulDistribMulAction L X] (F : IntermediateField K L) : MulDistribMulAction F X

Full source

/-- The action by an intermediate field is the action by the underlying field. -/
instance [Monoid X] [MulDistribMulAction L X] (F : IntermediateField K L) :
    MulDistribMulAction F X :=
  inferInstanceAs (MulDistribMulAction F.toSubfield X)

Multiplicative Distributive Action on Intermediate Fields

Informal description

For any intermediate field $F$ between fields $K$ and $L$, and any monoid $X$ equipped with a multiplicative distributive action by $L$, the intermediate field $F$ inherits a multiplicative distributive action on $X$. This means that for any $a, b \in F$ and $x \in X$, the action satisfies $(a \cdot b) \cdot x = a \cdot (b \cdot x)$ and $(a + b) \cdot x = a \cdot x + b \cdot x$.

IntermediateField.instSMulWithZeroSubtypeMem instance

[Zero X] [SMulWithZero L X] (F : IntermediateField K L) : SMulWithZero F X

Full source

/-- The action by an intermediate field is the action by the underlying field. -/
instance [Zero X] [SMulWithZero L X] (F : IntermediateField K L) : SMulWithZero F X :=
  inferInstanceAs (SMulWithZero F.toSubfield X)

Zero-Preserving Scalar Multiplication for Intermediate Fields

Informal description

For any intermediate field $ F $ between fields $ K $ and $ L $, and any type $ X $ with a zero element and a scalar multiplication operation by $ L $ that preserves zero, the intermediate field $ F $ inherits a scalar multiplication operation on $ X $ that also preserves zero.

IntermediateField.instMulActionWithZeroSubtypeMem instance

[Zero X] [MulActionWithZero L X] (F : IntermediateField K L) : MulActionWithZero F X

Full source

/-- The action by an intermediate field is the action by the underlying field. -/
instance [Zero X] [MulActionWithZero L X] (F : IntermediateField K L) : MulActionWithZero F X :=
  inferInstanceAs (MulActionWithZero F.toSubfield X)

Scalar Multiplication with Zero and Action Compatibility for Intermediate Fields

Informal description

For any intermediate field $F$ between fields $K$ and $L$, and any type $X$ with a zero element and a scalar multiplication operation by $L$ that preserves zero and is compatible with multiplication, the intermediate field $F$ inherits a scalar multiplication operation on $X$ that also preserves zero and is compatible with multiplication.

IntermediateField.instModuleSubtypeMem instance

[AddCommMonoid X] [Module L X] (F : IntermediateField K L) : Module F X

Full source

/-- The action by an intermediate field is the action by the underlying field. -/
instance [AddCommMonoid X] [Module L X] (F : IntermediateField K L) : Module F X :=
  inferInstanceAs (Module F.toSubfield X)

Module Structure on Intermediate Fields

Informal description

For any intermediate field $F$ between fields $K$ and $L$, and any additive commutative monoid $X$ equipped with a module structure over $L$, the intermediate field $F$ inherits a module structure over $X$.

IntermediateField.instMulSemiringActionSubtypeMem instance

[Semiring X] [MulSemiringAction L X] (F : IntermediateField K L) : MulSemiringAction F X

Full source

/-- The action by an intermediate field is the action by the underlying field. -/
instance [Semiring X] [MulSemiringAction L X] (F : IntermediateField K L) : MulSemiringAction F X :=
  inferInstanceAs (MulSemiringAction F.toSubfield X)

Multiplicative Semiring Action on Intermediate Fields

Informal description

For any semiring $X$ equipped with a multiplicative semiring action by $L$, and any intermediate field $F$ between $K$ and $L$, $F$ inherits a multiplicative semiring action on $X$ from $L$.

IntermediateField.toAlgebra instance

: Algebra S L

Full source

instance toAlgebra : Algebra S L :=
  inferInstanceAs (Algebra S.toSubalgebra L)

Algebra Structure on Intermediate Fields

Informal description

For any intermediate field $S$ between fields $K$ and $L$, there is a canonical algebra structure on $S$ over $L$.

IntermediateField.module' instance

{R} [Semiring R] [SMul R K] [Module R L] [IsScalarTower R K L] : Module R S

Full source

instance module' {R} [Semiring R] [SMul R K] [Module R L] [IsScalarTower R K L] : Module R S :=
  inferInstanceAs (Module R S.toSubalgebra)

Module Structure on Intermediate Fields via Scalar Tower

Informal description

For any intermediate field $S$ between fields $K$ and $L$, and any semiring $R$ with a scalar multiplication action on $K$ and a module structure on $L$ such that $R$, $K$, and $L$ form a scalar tower, $S$ inherits an $R$-module structure from $L$.

IntermediateField.algebra' instance

 {R' K L : Type*} [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

Full source

instance algebra' {R' K L : Type*} [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 :=
  inferInstanceAs (Algebra R' S.toSubalgebra)

Algebra Structure on Intermediate Fields from Scalar Tower

Informal description

For any intermediate field $S$ between fields $K$ and $L$, and any commutative semiring $R'$ with a scalar multiplication action on $K$ and an algebra structure on $L$ such that $R' \to K \to L$ forms a scalar tower, there exists a canonical algebra structure of $R'$ on $S$.

IntermediateField.isScalarTower instance

{R} [Semiring R] [SMul R K] [Module R L] [IsScalarTower R K L] : IsScalarTower R K S

Full source

instance isScalarTower {R} [Semiring R] [SMul R K] [Module R L] [IsScalarTower R K L] :
    IsScalarTower R K S :=
  inferInstanceAs (IsScalarTower R K S.toSubalgebra)

Scalar Tower Property for Intermediate Fields

Informal description

For any semiring $R$ with a scalar multiplication action on a field $K$, and a module structure on a field extension $L$ of $K$ such that $R$, $K$, and $L$ form a scalar tower, any intermediate field $S$ between $K$ and $L$ also forms a scalar tower $R \to K \to S$.

IntermediateField.coe_smul theorem

{R} [SMul R K] [SMul R L] [IsScalarTower R K L] (r : R) (x : S) : ↑(r • x : S) = (r • (x : L))

Full source

@[simp]
theorem coe_smul {R} [SMul R K] [SMul R L] [IsScalarTower R K L] (r : R) (x : S) :
    ↑(r • x : S) = (r • (x : L)) :=
  rfl

Compatibility of scalar multiplication with coercion in intermediate fields: $(r \cdot x : S) = r \cdot (x : L)$

Informal description

Let $K$ and $L$ be fields with $L$ an extension of $K$ via an algebra structure, and let $S$ be an intermediate field between $K$ and $L$. For any scalar $r$ in a type $R$ with compatible scalar multiplication actions on $K$ and $L$ (forming a scalar tower $R \to K \to L$), and any element $x \in S$, the coercion of the scalar multiple $r \cdot x$ in $S$ equals the scalar multiple $r \cdot x$ in $L$.

IntermediateField.algebraMap_apply theorem

(x : S) : algebraMap S L x = x

Full source

@[simp] lemma algebraMap_apply (x : S) : algebraMap S L x = x := rfl

Algebra Map Identity on Intermediate Fields

Informal description

For any element $x$ in an intermediate field $S$ between fields $K$ and $L$, the algebra map from $S$ to $L$ evaluated at $x$ is equal to $x$ itself, i.e., $\text{algebraMap}_{S \to L}(x) = x$.

IntermediateField.coe_algebraMap_apply theorem

(x : K) : ↑(algebraMap K S x) = algebraMap K L x

Full source

@[simp] lemma coe_algebraMap_apply (x : K) : ↑(algebraMap K S x) = algebraMap K L x := rfl

Compatibility of Algebra Maps in Intermediate Fields: $\iota_{S \to L} \circ \text{algebraMap}_{K \to S} = \text{algebraMap}_{K \to L}$

Informal description

For any element $x$ in the field $K$, the image of $x$ under the algebra map from $K$ to an intermediate field $S$ (when coerced to $L$) equals the image of $x$ under the algebra map from $K$ directly to $L$. That is, $\iota_{S \to L}(\text{algebraMap}_{K \to S}(x)) = \text{algebraMap}_{K \to L}(x)$, where $\iota_{S \to L}$ denotes the inclusion map from $S$ to $L$.

IntermediateField.isScalarTower_bot instance

{R : Type*} [Semiring R] [Algebra L R] : IsScalarTower S L R

Full source

instance isScalarTower_bot {R : Type*} [Semiring R] [Algebra L R] : IsScalarTower S L R :=
  IsScalarTower.subalgebra _ _ _ S.toSubalgebra

Scalar Tower Property for Intermediate Fields

Informal description

For any intermediate field $S$ in a field extension $L/K$ and any semiring $R$ with an algebra structure over $L$, the scalar multiplication operations satisfy the tower property $S \to L \to R$.

IntermediateField.isScalarTower_mid instance

{R : Type*} [Semiring R] [Algebra L R] [Algebra K R] [IsScalarTower K L R] : IsScalarTower K S R

Full source

instance isScalarTower_mid {R : Type*} [Semiring R] [Algebra L R] [Algebra K R]
    [IsScalarTower K L R] : IsScalarTower K S R :=
  IsScalarTower.subalgebra' _ _ _ S.toSubalgebra

Scalar Tower Property for Intermediate Fields in Middle Position

Informal description

For any intermediate field $S$ in a field extension $L/K$ and any semiring $R$ with algebra structures over both $K$ and $L$ such that $K \to L \to R$ forms a scalar tower, the scalar multiplication operations also satisfy the tower property $K \to S \to R$.

IntermediateField.isScalarTower_mid' instance

: IsScalarTower K S L

Full source

/-- Specialize `is_scalar_tower_mid` to the common case where the top field is `L` -/
instance isScalarTower_mid' : IsScalarTower K S L :=
  inferInstance

Scalar Tower Property for Intermediate Fields in $L/K$

Informal description

For any intermediate field $S$ in a field extension $L/K$, the scalar multiplication operations satisfy the tower property $K \to S \to L$.

IntermediateField.instAlgebraSubtypeMem instance

{E} [Semiring E] [Algebra L E] : Algebra S E

Full source

instance {E} [Semiring E] [Algebra L E] : Algebra S E := inferInstanceAs (Algebra S.toSubalgebra E)

Algebra Structure on Semirings via Intermediate Fields

Informal description

For any intermediate field $S$ between fields $K$ and $L$, and any semiring $E$ equipped with an $L$-algebra structure, there is a canonical $S$-algebra structure on $E$.

IntermediateField.instAlgebraSubtypeMem_1 instance

: Algebra S T

Full source

instance : Algebra S T := T.algebra

Algebra Structure on Intermediate Fields

Informal description

For any intermediate fields $S$ and $T$ between fields $K$ and $L$, there is a canonical $S$-algebra structure on $T$.

IntermediateField.instModuleSubtypeMem_1 instance

: Module S T

Full source

instance : Module S T := Algebra.toModule

Module Structure on Intermediate Fields

Informal description

For any intermediate fields $S$ and $T$ between fields $K$ and $L$, $T$ has a canonical $S$-module structure.

IntermediateField.instSMulSubtypeMem_1 instance

: SMul S T

Full source

instance : SMul S T := Algebra.toSMul

Scalar Multiplication on Intermediate Fields

Informal description

For any intermediate fields $S$ and $T$ between fields $K$ and $L$, there is a canonical scalar multiplication operation $\cdot : S \times T \to T$ defined by restricting the scalar multiplication of $L$ on $T$ to $S$.

IntermediateField.instIsScalarTowerSubtypeMem_1 instance

[Algebra K E] [IsScalarTower K L E] : IsScalarTower K S T

Full source

instance [Algebra K E] [IsScalarTower K L E] : IsScalarTower K S T := T.isScalarTower

Scalar Tower Property for Intermediate Fields in a Field Extension

Informal description

For any intermediate fields $S$ and $T$ between fields $K$ and $L$, and any algebra $E$ over $K$ with a scalar tower structure $K \to L \to E$, the scalar multiplication operations satisfy the tower property $K \to S \to T$.

IntermediateField.comap definition

(f : L →ₐ[K] L') (S : IntermediateField K L') : IntermediateField K L

Full source

/-- 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`. -/
def comap (f : L →ₐ[K] L') (S : IntermediateField K L') : IntermediateField K L where
  __ := S.toSubalgebra.comap f
  inv_mem' x hx := show f x⁻¹ ∈ S by rw [map_inv₀ f x]; exact S.inv_mem hx

Preimage of an intermediate field under an algebra homomorphism

Informal description

Given a field extension $ L / K $ and an algebra homomorphism $ f : L \to L' $ over $ K $, the comap of an intermediate field $ S $ between $ K $ and $ L' $ is the intermediate field between $ K $ and $ L $ consisting of all elements $ x \in L $ such that $ f(x) \in S $. More precisely, for any $ x \in L $, $ x $ belongs to $ \text{comap } f S $ if and only if $ f(x) $ belongs to $ S $.

IntermediateField.map definition

(f : L →ₐ[K] L') (S : IntermediateField K L) : IntermediateField K L'

Full source

/-- 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`. -/
def map (f : L →ₐ[K] L') (S : IntermediateField K L) : IntermediateField K L' where
  __ := S.toSubalgebra.map f
  inv_mem' := by
    rintro _ ⟨x, hx, rfl⟩
    exact ⟨x⁻¹, S.inv_mem hx, map_inv₀ f x⟩

Image of an intermediate field under an algebra homomorphism

Informal description

Given an algebra homomorphism $ f : L \to L' $ over $ K $ and an intermediate field $ S $ between $ K $ and $ L $, the map $ S \mapsto f(S) $ defines an intermediate field between $ K $ and $ L' $. Specifically, an element $ y \in L' $ is in $ f(S) $ if and only if there exists $ x \in S $ such that $ f(x) = y $. The inverse of $ y $ is given by $ f(x^{-1}) $ for $ x \in S $.

IntermediateField.coe_map theorem

(f : L →ₐ[K] L') : (S.map f : Set L') = f '' S

Full source

@[simp]
theorem coe_map (f : L →ₐ[K] L') : (S.map f : Set L') = f '' S :=
  rfl

Image of Intermediate Field Under Algebra Homomorphism Equals Function Image

Informal description

For any algebra homomorphism $f \colon L \to L'$ over $K$ and any intermediate field $S$ between $K$ and $L$, the underlying set of the image intermediate field $S.map f$ is equal to the image of $S$ under $f$, i.e., $(S.map f : \text{Set } L') = f(S)$.

IntermediateField.toSubalgebra_map theorem

(f : L →ₐ[K] L') : (S.map f).toSubalgebra = S.toSubalgebra.map f

Full source

@[simp]
theorem toSubalgebra_map (f : L →ₐ[K] L') : (S.map f).toSubalgebra = S.toSubalgebra.map f :=
  rfl

Subalgebra Structure Preservation under Field Homomorphism

Informal description

For any algebra homomorphism $f \colon L \to L'$ over $K$ and any intermediate field $S$ between $K$ and $L$, the subalgebra structure of the image $f(S)$ is equal to the image of the subalgebra structure of $S$ under $f$. In other words, $(f(S)).\text{toSubalgebra} = f(S.\text{toSubalgebra})$.

IntermediateField.toSubfield_map theorem

(f : L →ₐ[K] L') : (S.map f).toSubfield = S.toSubfield.map f

Full source

@[simp]
theorem toSubfield_map (f : L →ₐ[K] L') : (S.map f).toSubfield = S.toSubfield.map f :=
  rfl

Subfield Structure Preservation under Field Homomorphism

Informal description

For any algebra homomorphism $ f : L \to L' $ over $ K $ and any intermediate field $ S $ between $ K $ and $ L $, the subfield structure of the image $ f(S) $ is equal to the image of the subfield structure of $ S $ under $ f $. In other words, $ (f(S)).\text{toSubfield} = f(S.\text{toSubfield}) $.

IntermediateField.map_map theorem

 {K L₁ L₂ L₃ : Type*} [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₃) : (E.map f).map g = E.map (g.comp f)

Full source

theorem map_map {K L₁ L₂ L₃ : Type*} [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₃) :
    (E.map f).map g = E.map (g.comp f) :=
  SetLike.coe_injective <| Set.image_image _ _ _

Composition of Intermediate Field Images under Algebra Homomorphisms

Informal description

Let $K$ be a field and $L_1$, $L_2$, $L_3$ be field extensions of $K$ with corresponding algebra structures. For any intermediate field $E$ between $K$ and $L_1$, and any $K$-algebra homomorphisms $f \colon L_1 \to L_2$ and $g \colon L_2 \to L_3$, the following equality holds: $$(E \cdot f) \cdot g = E \cdot (g \circ f).$$ Here, $\cdot$ denotes the image of the intermediate field under the respective homomorphism.

IntermediateField.map_mono theorem

(f : L →ₐ[K] L') {S T : IntermediateField K L} (h : S ≤ T) : S.map f ≤ T.map f

Full source

theorem map_mono (f : L →ₐ[K] L') {S T : IntermediateField K L} (h : S ≤ T) :
    S.map f ≤ T.map f :=
  SetLike.coe_mono (Set.image_subset f h)

Monotonicity of Intermediate Field Images under Algebra Homomorphisms

Informal description

Let $ K $ be a field and $ L, L' $ be field extensions of $ K $. Given a $ K $-algebra homomorphism $ f : L \to L' $ and intermediate fields $ S $ and $ T $ between $ K $ and $ L $ such that $ S \subseteq T $, then the image of $ S $ under $ f $ is contained in the image of $ T $ under $ f $, i.e., $ f(S) \subseteq f(T) $.

IntermediateField.map_le_iff_le_comap theorem

{f : L →ₐ[K] L'} {s : IntermediateField K L} {t : IntermediateField K L'} : s.map f ≤ t ↔ s ≤ t.comap f

Full source

theorem map_le_iff_le_comap {f : L →ₐ[K] L'}
    {s : IntermediateField K L} {t : IntermediateField K L'} :
    s.map f ≤ t ↔ s ≤ t.comap f :=
  Set.image_subset_iff

Image-Preimage Order Correspondence for Intermediate Fields

Informal description

Let $L/K$ and $L'/K$ be field extensions, and let $f \colon L \to L'$ be a $K$-algebra homomorphism. For any intermediate field $S$ between $K$ and $L$ and any intermediate field $T$ between $K$ and $L'$, the image of $S$ under $f$ is contained in $T$ if and only if $S$ is contained in the preimage of $T$ under $f$. In symbols: \[ f(S) \leq T \leftrightarrow S \leq f^{-1}(T). \]

IntermediateField.gc_map_comap theorem

(f : L →ₐ[K] L') : GaloisConnection (map f) (comap f)

Full source

theorem gc_map_comap (f : L →ₐ[K] L') : GaloisConnection (map f) (comap f) :=
  fun _ _ ↦ map_le_iff_le_comap

Galois Connection Between Intermediate Field Maps and Preimages

Informal description

Let $L/K$ and $L'/K$ be field extensions, and let $f \colon L \to L'$ be a $K$-algebra homomorphism. Then the pair of functions $(S \mapsto f(S), T \mapsto f^{-1}(T))$ forms a Galois connection between the lattices of intermediate fields of $L/K$ and $L'/K$. That is, for any intermediate field $S$ between $K$ and $L$ and any intermediate field $T$ between $K$ and $L'$, we have: \[ f(S) \subseteq T \quad \text{if and only if} \quad S \subseteq f^{-1}(T). \]

IntermediateField.intermediateFieldMap definition

(e : L ≃ₐ[K] L') (E : IntermediateField K L) : E ≃ₐ[K] E.map e.toAlgHom

Full source

/-- 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` -/
def intermediateFieldMap (e : L ≃ₐ[K] L') (E : IntermediateField K L) : E ≃ₐ[K] E.map e.toAlgHom :=
  e.subalgebraMap E.toSubalgebra

Equivalence of Intermediate Fields under Algebra Extension Isomorphism

Informal description

Given a field extension $ L/K $ and an intermediate field $ E $ between $ K $ and $ L $, and given an equivalence $ e : L \simeq L' $ of $ K $-algebra extensions, the function `intermediateFieldMap` constructs an equivalence $ E \simeq E' $ where $ E' $ is the image of $ E $ under $ e $. Specifically, for any $ a \in E $, the equivalence maps $ a $ to $ e(a) \in E' $, and its inverse maps $ b \in E' $ to $ e^{-1}(b) \in E $.

IntermediateField.intermediateFieldMap_apply_coe theorem

(e : L ≃ₐ[K] L') (E : IntermediateField K L) (a : E) : ↑(intermediateFieldMap e E a) = e a

Full source

theorem intermediateFieldMap_apply_coe (e : L ≃ₐ[K] L') (E : IntermediateField K L) (a : E) :
    ↑(intermediateFieldMap e E a) = e a :=
  rfl

Image of Intermediate Field Element under Extension Isomorphism

Informal description

Let $L/K$ and $L'/K$ be field extensions, and let $e : L \simeq L'$ be a $K$-algebra isomorphism. For any intermediate field $E$ between $K$ and $L$, and any element $a \in E$, the image of $a$ under the induced isomorphism $\text{intermediateFieldMap}\, e\, E$ equals $e(a)$ when viewed as elements of $L'$.

IntermediateField.intermediateFieldMap_symm_apply_coe theorem

 (e : L ≃ₐ[K] L') (E : IntermediateField K L) (a : E.map e.toAlgHom) : ↑((intermediateFieldMap e E).symm a) = e.symm a

Full source

theorem intermediateFieldMap_symm_apply_coe (e : L ≃ₐ[K] L') (E : IntermediateField K L)
    (a : E.map e.toAlgHom) : ↑((intermediateFieldMap e E).symm a) = e.symm a :=
  rfl

Inverse of Intermediate Field Map Under Algebra Isomorphism

Informal description

Let $L/K$ and $L'/K$ be field extensions, and let $e : L \simeq L'$ be a $K$-algebra isomorphism. For any intermediate field $E$ between $K$ and $L$, and any element $a$ in the image $e(E)$ of $E$ under $e$, the underlying element of the inverse map $(e(E) \simeq E)^{-1}(a)$ in $L$ is equal to $e^{-1}(a)$.

AlgHom.fieldRange definition

: IntermediateField K L'

Full source

/-- The range of an algebra homomorphism, as an intermediate field. -/
@[simps toSubalgebra]
def fieldRange : IntermediateField K L' :=
  { f.range, (f : L →+* L').fieldRange with }

Range of an algebra homomorphism as an intermediate field

Informal description

Given a field extension $ L / K $ and an algebra homomorphism $ f \colon L \to L' $, the range of $ f $ forms an intermediate field between $ K $ and $ L' $. This intermediate field consists of all elements in $ L' $ that are images of elements in $ L $ under $ f $.

AlgHom.coe_fieldRange theorem

: ↑f.fieldRange = Set.range f

Full source

@[simp]
theorem coe_fieldRange : ↑f.fieldRange = Set.range f :=
  rfl

Range of an Algebra Homomorphism as an Intermediate Field

Informal description

For an algebra homomorphism $f \colon L \to L'$ between field extensions $L/K$ and $L'/K$, the underlying set of the intermediate field $\mathrm{fieldRange}(f)$ is equal to the range of $f$, i.e., $\mathrm{fieldRange}(f) = \{f(x) \mid x \in L\}$.

AlgHom.fieldRange_toSubfield theorem

: f.fieldRange.toSubfield = (f : L →+* L').fieldRange

Full source

@[simp]
theorem fieldRange_toSubfield : f.fieldRange.toSubfield = (f : L →+* L').fieldRange :=
  rfl

Equality of Field Ranges: Intermediate Field vs. Ring Homomorphism

Informal description

For an algebra homomorphism $f \colon L \to L'$ between field extensions $L/K$ and $L'/K$, the subfield associated with the intermediate field $\mathrm{fieldRange}(f)$ is equal to the field range of $f$ considered as a ring homomorphism from $L$ to $L'$.

AlgHom.mem_fieldRange theorem

{y : L'} : y ∈ f.fieldRange ↔ ∃ x, f x = y

Full source

@[simp]
theorem mem_fieldRange {y : L'} : y ∈ f.fieldRangey ∈ f.fieldRange ↔ ∃ x, f x = y :=
  Iff.rfl

Characterization of Elements in the Range of an Algebra Homomorphism

Informal description

For any element $y$ in the codomain $L'$ of an algebra homomorphism $f \colon L \to L'$, $y$ belongs to the range of $f$ as an intermediate field if and only if there exists an element $x$ in $L$ such that $f(x) = y$.

IntermediateField.val definition

: S →ₐ[K] L

Full source

/-- The embedding from an intermediate field of `L / K` to `L`. -/
def val : S →ₐ[K] L :=
  S.toSubalgebra.val

Inclusion homomorphism of an intermediate field

Informal description

The canonical algebra homomorphism from an intermediate field $ S $ between $ K $ and $ L $ to $ L $, which is the inclusion map $ S \hookrightarrow L $ preserving the $ K $-algebra structure.

IntermediateField.coe_val theorem

: ⇑S.val = ((↑) : S → L)

Full source

@[simp]
theorem coe_val : ⇑S.val = ((↑) : S → L) :=
  rfl

Inclusion Homomorphism Coincides with Coercion in Intermediate Fields

Informal description

The underlying function of the inclusion algebra homomorphism $S.\text{val} \colon S \to L$ is equal to the coercion map $(\cdot) \colon S \to L$.

IntermediateField.val_mk theorem

{x : L} (hx : x ∈ S) : S.val ⟨x, hx⟩ = x

Full source

@[simp]
theorem val_mk {x : L} (hx : x ∈ S) : S.val ⟨x, hx⟩ = x :=
  rfl

Inclusion Homomorphism Preserves Elements in Intermediate Fields

Informal description

For any element $x$ in the field $L$ that belongs to an intermediate field $S$ between $K$ and $L$, the inclusion homomorphism $\text{val} \colon S \to L$ maps the element $\langle x, hx \rangle$ (where $hx$ is the proof that $x \in S$) to $x$ itself.

IntermediateField.range_val theorem

: S.val.range = S.toSubalgebra

Full source

theorem range_val : S.val.range = S.toSubalgebra :=
  S.toSubalgebra.range_val

Range of Intermediate Field Inclusion Equals Subalgebra

Informal description

For an intermediate field $S$ between fields $K$ and $L$, the range of the inclusion homomorphism $S.\text{val} \colon S \to L$ is equal to $S$ viewed as a subalgebra of $L$.

IntermediateField.fieldRange_val theorem

: S.val.fieldRange = S

Full source

@[simp]
theorem fieldRange_val : S.val.fieldRange = S :=
  SetLike.ext' Subtype.range_val

Range of Intermediate Field Inclusion Equals Itself

Informal description

For any intermediate field $S$ between fields $K$ and $L$, the range of the inclusion homomorphism $S \hookrightarrow L$ is equal to $S$ itself.

IntermediateField.AlgHom.inhabited instance

: Inhabited (S →ₐ[K] L)

Full source

instance AlgHom.inhabited : Inhabited (S →ₐ[K] L) :=
  ⟨S.val⟩

Existence of Algebra Homomorphisms from Intermediate Fields

Informal description

For any intermediate field $S$ between fields $K$ and $L$, the type of $K$-algebra homomorphisms from $S$ to $L$ is inhabited.

IntermediateField.aeval_coe theorem

 {R : Type*} [CommSemiring R] [Algebra R K] [Algebra R L] [IsScalarTower R K L] (x : S) (P : R[X]) :
  aeval (x : L) P = aeval x P

Full source

theorem aeval_coe {R : Type*} [CommSemiring R] [Algebra R K] [Algebra R L] [IsScalarTower R K L]
    (x : S) (P : R[X]) : aeval (x : L) P = aeval x P :=
  aeval_algHom_apply (S.val.restrictScalars R) x P

Compatibility of Polynomial Evaluation with Intermediate Field Inclusion

Informal description

Let $K$ and $L$ be fields with an algebra structure $[Algebra K L]$, and let $S$ be an intermediate field between $K$ and $L$. For any commutative semiring $R$ with algebra structures $[Algebra R K]$ and $[Algebra R L]$ forming a scalar tower $R \to K \to L$, and for any polynomial $P \in R[X]$ and element $x \in S$, the evaluation of $P$ at $x$ (viewed as an element of $L$) equals the evaluation of $P$ at $x$ (viewed as an element of $S$). In other words, the algebraic evaluation commutes with the inclusion map $S \hookrightarrow L$. Symbolically, this is expressed as: \[ \text{aeval} (x : L) P = \text{aeval} (x : S) P \]

IntermediateField.inclusion definition

{E F : IntermediateField K L} (hEF : E ≤ F) : E →ₐ[K] F

Full source

/-- 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`. -/
def inclusion {E F : IntermediateField K L} (hEF : E ≤ F) : E →ₐ[K] F :=
  Subalgebra.inclusion hEF

Inclusion map of intermediate fields

Informal description

Given two intermediate fields $ E $ and $ F $ between fields $ K $ and $ L $ with $ E \subseteq F $, the function $ \text{inclusion} $ is the canonical algebra homomorphism from $ E $ to $ F $ over $ K $. This map is the intermediate field version of the subalgebra inclusion map.

IntermediateField.inclusion_injective theorem

{E F : IntermediateField K L} (hEF : E ≤ F) : Function.Injective (inclusion hEF)

Full source

theorem inclusion_injective {E F : IntermediateField K L} (hEF : E ≤ F) :
    Function.Injective (inclusion hEF) :=
  Subalgebra.inclusion_injective hEF

Injectivity of Intermediate Field Inclusion Map

Informal description

For any intermediate fields $E$ and $F$ between fields $K$ and $L$ with $E \subseteq F$, the inclusion map $\text{inclusion} : E \to F$ is injective.

IntermediateField.inclusion_self theorem

{E : IntermediateField K L} : inclusion (le_refl E) = AlgHom.id K E

Full source

@[simp]
theorem inclusion_self {E : IntermediateField K L} : inclusion (le_refl E) = AlgHom.id K E :=
  Subalgebra.inclusion_self

Identity Property of Intermediate Field Inclusion

Informal description

For any intermediate field $E$ between fields $K$ and $L$, the inclusion map of $E$ into itself is equal to the identity algebra homomorphism on $E$ over $K$.

IntermediateField.inclusion_inclusion theorem

 {E F G : IntermediateField K L} (hEF : E ≤ F) (hFG : F ≤ G) (x : E) :
  inclusion hFG (inclusion hEF x) = inclusion (le_trans hEF hFG) x

Full source

@[simp]
theorem inclusion_inclusion {E F G : IntermediateField K L} (hEF : E ≤ F) (hFG : F ≤ G) (x : E) :
    inclusion hFG (inclusion hEF x) = inclusion (le_trans hEF hFG) x :=
  Subalgebra.inclusion_inclusion hEF hFG x

Composition of Intermediate Field Inclusions

Informal description

Let $K \subseteq E \subseteq F \subseteq G \subseteq L$ be a tower of intermediate fields between fields $K$ and $L$. For any element $x \in E$, the composition of inclusion maps $E \hookrightarrow F \hookrightarrow G$ equals the direct inclusion map $E \hookrightarrow G$, i.e., $\text{inclusion}_{F \subseteq G} \circ \text{inclusion}_{E \subseteq F}(x) = \text{inclusion}_{E \subseteq G}(x)$.

IntermediateField.coe_inclusion theorem

{E F : IntermediateField K L} (hEF : E ≤ F) (e : E) : (inclusion hEF e : L) = e

Full source

@[simp]
theorem coe_inclusion {E F : IntermediateField K L} (hEF : E ≤ F) (e : E) :
    (inclusion hEF e : L) = e :=
  rfl

Inclusion Map Preserves Elements in Intermediate Fields

Informal description

Let $K$ and $L$ be fields with $L$ an extension of $K$, and let $E$ and $F$ be intermediate fields between $K$ and $L$ such that $E \subseteq F$. For any element $e \in E$, the image of $e$ under the inclusion map $\text{inclusion}_{hEF} : E \to F$ equals $e$ when viewed as an element of $L$.

IntermediateField.toSubalgebra_injective theorem

: Function.Injective (toSubalgebra : IntermediateField K L → _)

Full source

theorem toSubalgebra_injective : Function.Injective (toSubalgebra : IntermediateField K L → _) := by
  intro _ _ h
  ext
  simp_rw [← mem_toSubalgebra, h]

Injectivity of Intermediate Field to Subalgebra Map

Informal description

The canonical map from an intermediate field $S$ between $K$ and $L$ to its underlying subalgebra is injective. In other words, if two intermediate fields $S$ and $T$ have the same underlying subalgebra structure, then $S = T$.

IntermediateField.toSubfield_injective theorem

: Function.Injective (toSubfield : IntermediateField K L → _)

Full source

theorem toSubfield_injective : Function.Injective (toSubfield : IntermediateField K L → _) := by
  intro _ _ h
  ext
  simp_rw [← mem_toSubfield, h]

Injectivity of Intermediate Field to Subfield Map

Informal description

The canonical map from an intermediate field $S$ between $K$ and $L$ to its underlying subfield is injective. In other words, if two intermediate fields $S$ and $T$ have the same underlying subfield structure, then $S = T$.

IntermediateField.toSubalgebra_inj theorem

: F.toSubalgebra = E.toSubalgebra ↔ F = E

Full source

@[simp]
theorem toSubalgebra_inj : F.toSubalgebra = E.toSubalgebra ↔ F = E := toSubalgebra_injective.eq_iff

Equality of Intermediate Fields via Subalgebra Equality

Informal description

For any two intermediate fields $E$ and $F$ between $K$ and $L$, the underlying subalgebras of $E$ and $F$ are equal if and only if $E = F$.

IntermediateField.toSubfield_inj theorem

: F.toSubfield = E.toSubfield ↔ F = E

Full source

@[simp]
theorem toSubfield_inj : F.toSubfield = E.toSubfield ↔ F = E := toSubfield_injective.eq_iff

Equality of Intermediate Fields via Subfield Equality

Informal description

For any two intermediate fields $E$ and $F$ between $K$ and $L$, the equality of their underlying subfields is equivalent to the equality of the intermediate fields themselves, i.e., $E.\text{toSubfield} = F.\text{toSubfield}$ if and only if $E = F$.

IntermediateField.map_injective theorem

(f : L →ₐ[K] L') : Function.Injective (map f)

Full source

theorem map_injective (f : L →ₐ[K] L') : Function.Injective (map f) := by
  intro _ _ h
  rwa [← toSubalgebra_injective.eq_iff, toSubalgebra_map, toSubalgebra_map,
    (Subalgebra.map_injective f.injective).eq_iff, toSubalgebra_inj] at h

Injectivity of Intermediate Field Mapping under Algebra Homomorphism

Informal description

Given a field extension $L/K$ and an algebra homomorphism $f \colon L \to L'$ over $K$, the induced map on intermediate fields is injective. That is, for any intermediate fields $S, T$ between $K$ and $L$, if $f(S) = f(T)$ as intermediate fields between $K$ and $L'$, then $S = T$.

IntermediateField.set_range_subset theorem

: Set.range (algebraMap K L) ⊆ S

Full source

theorem set_range_subset : Set.rangeSet.range (algebraMap K L) ⊆ S :=
  S.toSubalgebra.range_subset

Range of Algebra Map is Contained in Intermediate Field

Informal description

For an intermediate field $S$ between fields $K$ and $L$, the range of the algebra map from $K$ to $L$ is contained in $S$, i.e., $\text{range}(\text{algebraMap}\, K\, L) \subseteq S$.

IntermediateField.fieldRange_le theorem

: (algebraMap K L).fieldRange ≤ S.toSubfield

Full source

theorem fieldRange_le : (algebraMap K L).fieldRange ≤ S.toSubfield := fun x hx =>
  S.toSubalgebra.range_subset (by rwa [Set.mem_range, ← RingHom.mem_fieldRange])

Inclusion of Field Range in Intermediate Field

Informal description

For an intermediate field $S$ between fields $K$ and $L$, the field range of the algebra map from $K$ to $L$ is contained in $S$ when viewed as a subfield of $L$, i.e., $\text{fieldRange}(\text{algebraMap}\, K\, L) \leq S$.

IntermediateField.toSubalgebra_le_toSubalgebra theorem

{S S' : IntermediateField K L} : S.toSubalgebra ≤ S'.toSubalgebra ↔ S ≤ S'

Full source

@[simp]
theorem toSubalgebra_le_toSubalgebra {S S' : IntermediateField K L} :
    S.toSubalgebra ≤ S'.toSubalgebra ↔ S ≤ S' :=
  Iff.rfl

Subalgebra Containment in Intermediate Fields is Equivalent to Intermediate Field Containment

Informal description

For any intermediate fields $S$ and $S'$ between fields $K$ and $L$, the subalgebra $S$ is contained in the subalgebra $S'$ if and only if $S$ is contained in $S'$ as intermediate fields. In other words, $S \leq S'$ holds if and only if $S.\text{toSubalgebra} \leq S'.\text{toSubalgebra}$.

IntermediateField.toSubalgebra_lt_toSubalgebra theorem

{S S' : IntermediateField K L} : S.toSubalgebra < S'.toSubalgebra ↔ S < S'

Full source

@[simp]
theorem toSubalgebra_lt_toSubalgebra {S S' : IntermediateField K L} :
    S.toSubalgebra < S'.toSubalgebra ↔ S < S' :=
  Iff.rfl

Strict Inclusion of Intermediate Fields via Subalgebras

Informal description

For any intermediate fields $S$ and $S'$ between fields $K$ and $L$, the strict inclusion $S < S'$ holds if and only if the corresponding strict inclusion holds for their underlying subalgebras, i.e., $S.\text{toSubalgebra} < S'.\text{toSubalgebra}$.

IntermediateField.lift definition

{F : IntermediateField K L} (E : IntermediateField K F) : IntermediateField K L

Full source

/-- Lift an intermediate_field of an intermediate_field -/
def lift {F : IntermediateField K L} (E : IntermediateField K F) : IntermediateField K L :=
  E.map (val F)

Lift of intermediate field through field extension

Informal description

Given a field extension $L/K$ and an intermediate field $F$ between $K$ and $L$, the function lifts any intermediate field $E$ between $K$ and $F$ to an intermediate field between $K$ and $L$ by applying the inclusion homomorphism $F \hookrightarrow L$ to $E$. More precisely, for $E$ an intermediate field of $F/K$, the lift $\text{lift}(E)$ is the image of $E$ under the canonical inclusion $F \to L$, which forms an intermediate field between $K$ and $L$.

IntermediateField.lift_injective theorem

(F : IntermediateField K L) : Function.Injective F.lift

Full source

theorem lift_injective (F : IntermediateField K L) : Function.Injective F.lift :=
  map_injective F.val

Injectivity of Intermediate Field Lifting

Informal description

For any intermediate field $F$ between fields $K$ and $L$, the lifting map $\text{lift} \colon \text{IntermediateField}\, K\, F \to \text{IntermediateField}\, K\, L$ is injective. That is, for any intermediate fields $E_1, E_2$ between $K$ and $F$, if $\text{lift}(E_1) = \text{lift}(E_2)$, then $E_1 = E_2$.

IntermediateField.lift_le theorem

{F : IntermediateField K L} (E : IntermediateField K F) : lift E ≤ F

Full source

theorem lift_le {F : IntermediateField K L} (E : IntermediateField K F) : lift E ≤ F := by
  rintro _ ⟨x, _, rfl⟩
  exact x.2

Lift of Intermediate Field is Contained in Original Field

Informal description

For any intermediate field $F$ between $K$ and $L$, and any intermediate field $E$ between $K$ and $F$, the lift of $E$ to an intermediate field between $K$ and $L$ is contained in $F$. In other words, if $E$ is an intermediate field of $F/K$, then $\text{lift}(E) \leq F$.

IntermediateField.mem_lift theorem

{F : IntermediateField K L} {E : IntermediateField K F} (x : F) : x.1 ∈ lift E ↔ x ∈ E

Full source

theorem mem_lift {F : IntermediateField K L} {E : IntermediateField K F} (x : F) :
    x.1 ∈ lift Ex.1 ∈ lift E ↔ x ∈ E :=
  Subtype.val_injective.mem_set_image

Membership Criterion for Lifted Intermediate Field

Informal description

Let $L/K$ be a field extension and let $F$ be an intermediate field between $K$ and $L$. For any intermediate field $E$ between $K$ and $F$ and any element $x \in F$, the inclusion $x \in \text{lift}(E)$ holds if and only if $x \in E$.

IntermediateField.liftAlgEquiv definition

{E : IntermediateField K L} (F : IntermediateField K E) : ↥F ≃ₐ[K] lift F

Full source

/-- The algEquiv between an intermediate field and its lift -/
def liftAlgEquiv {E : IntermediateField K L} (F : IntermediateField K E) : ↥F ≃ₐ[K] lift F where
  toFun x := ⟨x.1.1, (mem_lift x.1).mpr x.2⟩
  invFun x := ⟨⟨x.1, lift_le F x.2⟩, (mem_lift ⟨x.1, lift_le F x.2⟩).mp x.2⟩
  left_inv := congrFun rfl
  right_inv := congrFun rfl
  map_mul' _ _ := rfl
  map_add' _ _ := rfl
  commutes' _ := rfl

Algebra equivalence between an intermediate field and its lift

Informal description

Given an intermediate field $ E $ between $ K $ and $ L $, and an intermediate field $ F $ between $ K $ and $ E $, the function `IntermediateField.liftAlgEquiv` constructs an algebra equivalence between $ F $ and its lift to an intermediate field between $ K $ and $ L $. More precisely, the lift of $ F $ is the image of $ F $ under the canonical inclusion $ E \hookrightarrow L $, and the equivalence states that $ F $ is isomorphic (as a $ K $-algebra) to its lift in $ L $.

IntermediateField.liftAlgEquiv_apply theorem

{E : IntermediateField K L} (F : IntermediateField K E) (x : F) : (liftAlgEquiv F x).1 = x

Full source

lemma liftAlgEquiv_apply {E : IntermediateField K L} (F : IntermediateField K E) (x : F) :
    (liftAlgEquiv F x).1 = x := rfl

Projection Property of Algebra Equivalence for Lifted Intermediate Fields

Informal description

Let $L/K$ be a field extension with an intermediate field $E$ between $K$ and $L$, and let $F$ be an intermediate field between $K$ and $E$. For any element $x \in F$, the first projection of the algebra equivalence $\text{liftAlgEquiv}(F)(x)$ equals $x$ itself.

IntermediateField.restrictScalars definition

(E : IntermediateField L' L) : IntermediateField K L

Full source

/-- 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`. -/
def restrictScalars (E : IntermediateField L' L) : IntermediateField K L :=
  { E.toSubfield, E.toSubalgebra.restrictScalars K with
    carrier := E.carrier }

Restriction of scalars for intermediate fields

Informal description

Given a tower of field extensions $ L / E / L' / K $, where $ E $ is an intermediate field between $ L' $ and $ L $, the function `IntermediateField.restrictScalars` reinterprets $ E $ as an intermediate field between $ K $ and $ L $. This means that $ E $ is viewed as a $ K $-subalgebra of $ L $ while retaining its field structure.

IntermediateField.coe_restrictScalars theorem

{E : IntermediateField L' L} : (restrictScalars K E : Set L) = (E : Set L)

Full source

@[simp]
theorem coe_restrictScalars {E : IntermediateField L' L} :
    (restrictScalars K E : Set L) = (E : Set L) :=
  rfl

Equality of Underlying Sets in Restriction of Scalars for Intermediate Fields

Informal description

For any intermediate field $E$ between $L'$ and $L$ in a field extension tower $L/L'/K$, the underlying set of $E$ viewed as an intermediate field over $K$ via restriction of scalars is equal to the underlying set of $E$ itself. In other words, $(\text{restrictScalars}_K E : \text{Set } L) = (E : \text{Set } L)$.

IntermediateField.restrictScalars_toSubalgebra theorem

{E : IntermediateField L' L} : (E.restrictScalars K).toSubalgebra = E.toSubalgebra.restrictScalars K

Full source

@[simp]
theorem restrictScalars_toSubalgebra {E : IntermediateField L' L} :
    (E.restrictScalars K).toSubalgebra = E.toSubalgebra.restrictScalars K :=
  SetLike.coe_injective rfl

Subalgebra Structure Preservation under Scalar Restriction for Intermediate Fields

Informal description

For any intermediate field $E$ between $L'$ and $L$ in a tower of field extensions $L / E / L' / K$, the underlying subalgebra structure of $E$ when restricted to scalars from $K$ is equal to the restriction of scalars of the subalgebra structure of $E$ from $L'$ to $K$.

IntermediateField.restrictScalars_toSubfield theorem

{E : IntermediateField L' L} : (E.restrictScalars K).toSubfield = E.toSubfield

Full source

@[simp]
theorem restrictScalars_toSubfield {E : IntermediateField L' L} :
    (E.restrictScalars K).toSubfield = E.toSubfield :=
  SetLike.coe_injective rfl

Subfield Structure Preservation under Scalar Restriction

Informal description

For any intermediate field $E$ between $L'$ and $L$, the subfield structure obtained by restricting scalars from $L'$ to $K$ is equal to the original subfield structure of $E$. In other words, $(E.\text{restrictScalars}\ K).\text{toSubfield} = E.\text{toSubfield}$.

IntermediateField.mem_restrictScalars theorem

{E : IntermediateField L' L} {x : L} : x ∈ restrictScalars K E ↔ x ∈ E

Full source

@[simp]
theorem mem_restrictScalars {E : IntermediateField L' L} {x : L} :
    x ∈ restrictScalars K Ex ∈ restrictScalars K E ↔ x ∈ E :=
  Iff.rfl

Membership in Restricted Scalars Intermediate Field

Informal description

For any intermediate field $E$ between $L'$ and $L$, and any element $x \in L$, we have $x \in \text{restrictScalars}_K E$ if and only if $x \in E$.

IntermediateField.restrictScalars_injective theorem

: Function.Injective (restrictScalars K : IntermediateField L' L → IntermediateField K L)

Full source

theorem restrictScalars_injective :
    Function.Injective (restrictScalars K : IntermediateField L' L → IntermediateField K L) :=
  fun U V H => ext fun x => by rw [← mem_restrictScalars K, H, mem_restrictScalars]

Injectivity of Scalar Restriction for Intermediate Fields

Informal description

The scalar restriction map from intermediate fields between $L'$ and $L$ to intermediate fields between $K$ and $L$ is injective. That is, for any intermediate fields $E_1, E_2$ between $L'$ and $L$, if $\text{restrictScalars}_K E_1 = \text{restrictScalars}_K E_2$, then $E_1 = E_2$.

Subfield.extendScalars definition

: IntermediateField F L

Full source

/-- 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`. -/
def extendScalars : IntermediateField F L := E.toIntermediateField fun ⟨_, hf⟩ ↦ h hf

Extension of scalars for subfields to intermediate fields

Informal description

Given a field extension $ L / F $ and a subfield $ E $ of $ L $ containing $ F $, the function constructs an intermediate field between $ F $ and $ L $ by extending the scalars of $ E $ to include $ F $. This ensures that $ E $ is both a subfield of $ L $ and a subalgebra over $ F $.

Subfield.coe_extendScalars theorem

: (extendScalars h : Set L) = (E : Set L)

Full source

@[simp]
theorem coe_extendScalars : (extendScalars h : Set L) = (E : Set L) := rfl

Underlying Set Equality in Scalar Extension of Subfield to Intermediate Field

Informal description

For a field extension $L/F$ and a subfield $E$ of $L$ containing $F$, the underlying set of the intermediate field obtained by extending scalars from $F$ to $E$ is equal to $E$ as a subset of $L$.

Subfield.extendScalars_toSubfield theorem

: (extendScalars h).toSubfield = E

Full source

@[simp]
theorem extendScalars_toSubfield : (extendScalars h).toSubfield = E := SetLike.coe_injective rfl

Subfield Conversion of Scalar Extension Equals Original Subfield

Informal description

For a field extension $L/F$ and a subfield $E$ of $L$ containing $F$, the subfield obtained by converting the intermediate field `extendScalars h` back to a subfield equals $E$.

Subfield.mem_extendScalars theorem

: x ∈ extendScalars h ↔ x ∈ E

Full source

@[simp]
theorem mem_extendScalars : x ∈ extendScalars hx ∈ extendScalars h ↔ x ∈ E := Iff.rfl

Membership in Extended Scalar Intermediate Field Equals Membership in Original Subfield

Informal description

For any element $x$ in the field extension $L$, $x$ belongs to the intermediate field obtained by extending scalars of $E$ (with $F \subseteq E \subseteq L$) if and only if $x$ belongs to $E$.

Subfield.extendScalars_le_extendScalars_iff theorem

: extendScalars h ≤ extendScalars h' ↔ E ≤ E'

Full source

theorem extendScalars_le_extendScalars_iff : extendScalarsextendScalars h ≤ extendScalars h' ↔ E ≤ E' := Iff.rfl

Order of Scalar Extensions Reflects Order of Subfields

Informal description

For two subfields $E$ and $E'$ of $L$ containing $F$, the scalar extension of $E$ is contained in the scalar extension of $E'$ if and only if $E$ is contained in $E'$.

Subfield.extendScalars_le_iff theorem

(E' : IntermediateField F L) : extendScalars h ≤ E' ↔ E ≤ E'.toSubfield

Full source

theorem extendScalars_le_iff (E' : IntermediateField F L) :
    extendScalarsextendScalars h ≤ E' ↔ E ≤ E'.toSubfield := Iff.rfl

Comparison of Extended Scalar Intermediate Field with Subfield Inclusion

Informal description

Let $L/F$ be a field extension, and let $E$ be a subfield of $L$ containing $F$. For any intermediate field $E'$ between $F$ and $L$, the extension of scalars of $E$ is contained in $E'$ if and only if $E$ is contained in the subfield corresponding to $E'$. In other words: \[ \text{extendScalars}(E) \leq E' \leftrightarrow E \leq E'.\text{toSubfield} \]

Subfield.le_extendScalars_iff theorem

(E' : IntermediateField F L) : E' ≤ extendScalars h ↔ E'.toSubfield ≤ E

Full source

theorem le_extendScalars_iff (E' : IntermediateField F L) :
    E' ≤ extendScalars h ↔ E'.toSubfield ≤ E := Iff.rfl

Order Relation Between Intermediate Field and Scalar Extension

Informal description

For any intermediate field $E'$ between $F$ and $L$, the inclusion $E' \leq \text{extendScalars}(h)$ holds if and only if the underlying subfield of $E'$ is contained in $E$.

Subfield.extendScalars.orderIso definition

: { E : Subfield L // F ≤ E } ≃o IntermediateField F L

Full source

/-- `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`. -/
@[simps]
def extendScalars.orderIso :
    { E : Subfield L // F ≤ E }{ E : Subfield L // F ≤ E } ≃o IntermediateField F L where
  toFun E := extendScalars E.2
  invFun E := ⟨E.toSubfield, fun x hx ↦ E.algebraMap_mem ⟨x, hx⟩⟩
  left_inv _ := rfl
  right_inv _ := rfl
  map_rel_iff' {E E'} := by
    simp only [Equiv.coe_fn_mk]
    exact extendScalars_le_extendScalars_iff _ _

Order isomorphism between subfields containing $ F $ and intermediate fields over $ F $

Informal description

The function `Subfield.extendScalars.orderIso` defines an order isomorphism between the partially ordered set of subfields $ E $ of $ L $ containing $ F $ (i.e., $\{ E : \text{Subfield } L \mid F \leq E \}$) and the partially ordered set of intermediate fields between $ F $ and $ L $. The isomorphism maps a subfield $ E $ to the intermediate field obtained by extending the scalars of $ E $ to include $ F $, and its inverse maps an intermediate field back to its underlying subfield. This isomorphism preserves the order structure, meaning $ E \leq E' $ if and only if the corresponding intermediate fields satisfy the same inequality.

Subfield.extendScalars_injective theorem

: Function.Injective fun E : { E : Subfield L // F ≤ E } ↦ extendScalars E.2

Full source

theorem extendScalars_injective :
    Function.Injective fun E : { E : Subfield L // F ≤ E } ↦ extendScalars E.2 :=
  (extendScalars.orderIso F).injective

Injectivity of Scalar Extension for Subfields Containing $F$

Informal description

The map sending each subfield $E$ of $L$ containing $F$ to the intermediate field obtained by extending scalars from $F$ to $E$ is injective. In other words, if two subfields $E_1$ and $E_2$ of $L$ both contain $F$ and their scalar extensions to intermediate fields are equal, then $E_1 = E_2$.

IntermediateField.extendScalars definition

: IntermediateField F L

Full source

/-- 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`. -/
def extendScalars : IntermediateField F L :=
  Subfield.extendScalars (show F.toSubfield ≤ E.toSubfield from h)

Extension of scalars for intermediate fields

Informal description

Given a field extension $ L / F $ and a subfield $ E $ of $ L $ containing $ F $, the function `IntermediateField.extendScalars` constructs an intermediate field between $ F $ and $ L $ by extending the scalars of $ E $ to include $ F $. This ensures that $ E $ is both a subfield of $ L $ and a subalgebra over $ F $.

IntermediateField.coe_extendScalars theorem

: (extendScalars h : Set L) = (E : Set L)

Full source

@[simp]
theorem coe_extendScalars : (extendScalars h : Set L) = (E : Set L) := rfl

Equality of Underlying Sets in Scalar Extension of Intermediate Fields

Informal description

For an intermediate field $E$ between fields $F$ and $L$, the underlying set of the extended scalars construction equals the underlying set of $E$ itself, i.e., $(\text{extendScalars}\,h : \text{Set}\,L) = (E : \text{Set}\,L)$.

IntermediateField.extendScalars_toSubfield theorem

: (extendScalars h).toSubfield = E.toSubfield

Full source

@[simp]
theorem extendScalars_toSubfield : (extendScalars h).toSubfield = E.toSubfield :=
  SetLike.coe_injective rfl

Equality of Subfield Structures After Scalar Extension

Informal description

For any intermediate field $E$ between fields $K$ and $L$, and any field extension $L/F$ where $F \subseteq E$, the subfield structure obtained from extending scalars of $E$ to $F$ is equal to the subfield structure of $E$ itself. That is, $(\text{extendScalars}\ h).\text{toSubfield} = E.\text{toSubfield}$.

IntermediateField.mem_extendScalars theorem

: x ∈ extendScalars h ↔ x ∈ E

Full source

@[simp]
theorem mem_extendScalars : x ∈ extendScalars hx ∈ extendScalars h ↔ x ∈ E := Iff.rfl

Membership in Scalar Extension of Intermediate Field

Informal description

For any element $x$ in the field extension $L$ and any intermediate field $E$ between $K$ and $L$, $x$ belongs to the extension of scalars of $E$ if and only if $x$ belongs to $E$.

IntermediateField.extendScalars_restrictScalars theorem

: (extendScalars h).restrictScalars K = E

Full source

@[simp]
theorem extendScalars_restrictScalars : (extendScalars h).restrictScalars K = E := rfl

Extension-Restriction Scalar Identity for Intermediate Fields

Informal description

Given a field extension $L / K$ and an intermediate field $E$ between $K$ and $L$, the restriction of scalars of the extension of scalars of $E$ back to $K$ equals $E$ itself. That is, $(\text{extendScalars}\ h).\text{restrictScalars}\ K = E$.

IntermediateField.extendScalars_le_extendScalars_iff theorem

: extendScalars h ≤ extendScalars h' ↔ E ≤ E'

Full source

theorem extendScalars_le_extendScalars_iff : extendScalarsextendScalars h ≤ extendScalars h' ↔ E ≤ E' := Iff.rfl

Extension of Scalars Preserves Partial Order on Intermediate Fields

Informal description

For intermediate fields $ E $ and $ E' $ between fields $ K $ and $ L $, the extension of scalars $ \text{extendScalars}(h) $ is less than or equal to $ \text{extendScalars}(h') $ if and only if $ E $ is less than or equal to $ E' $ in the partial order of intermediate fields.

IntermediateField.extendScalars_le_iff theorem

(E' : IntermediateField F L) : extendScalars h ≤ E' ↔ E ≤ E'.restrictScalars K

Full source

theorem extendScalars_le_iff (E' : IntermediateField F L) :
    extendScalarsextendScalars h ≤ E' ↔ E ≤ E'.restrictScalars K := Iff.rfl

Extension of Scalars Containment Criterion for Intermediate Fields

Informal description

Let $L/K$ be a field extension and $F$ be an intermediate field between $K$ and $L$. For any intermediate field $E'$ between $F$ and $L$, the extension of scalars $\text{extendScalars}(h)$ is contained in $E'$ if and only if $E$ is contained in the restriction of scalars of $E'$ to $K$.

IntermediateField.le_extendScalars_iff theorem

(E' : IntermediateField F L) : E' ≤ extendScalars h ↔ E'.restrictScalars K ≤ E

Full source

theorem le_extendScalars_iff (E' : IntermediateField F L) :
    E' ≤ extendScalars h ↔ E'.restrictScalars K ≤ E := Iff.rfl

Order Relation Between Intermediate Fields and Their Scalar Extensions

Informal description

Let $L/K$ be a field extension with an intermediate field $E$ such that $F \leq E \leq L$. For any intermediate field $E'$ between $F$ and $L$, we have $E' \leq \text{extendScalars}(h)$ if and only if $E'.\text{restrictScalars}(K) \leq E$.

IntermediateField.extendScalars.orderIso definition

: { E : IntermediateField K L // F ≤ E } ≃o IntermediateField F L

Full source

/-- `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`. -/
@[simps]
def extendScalars.orderIso : { E : IntermediateField K L // F ≤ E }{ E : IntermediateField K L // F ≤ E } ≃o IntermediateField F L where
  toFun E := extendScalars E.2
  invFun E := ⟨E.restrictScalars K, fun x hx ↦ E.algebraMap_mem ⟨x, hx⟩⟩
  left_inv _ := rfl
  right_inv _ := rfl
  map_rel_iff' {E E'} := by
    simp only [Equiv.coe_fn_mk]
    exact extendScalars_le_extendScalars_iff _ _

Order isomorphism between intermediate fields via scalar extension and restriction

Informal description

The function `IntermediateField.extendScalars.orderIso` defines an order isomorphism between the partially ordered set of intermediate fields $ E $ between $ K $ and $ L $ containing $ F $ (i.e., $ F \leq E \leq L $) and the partially ordered set of intermediate fields between $ F $ and $ L $. The isomorphism maps an intermediate field $ E $ to its extension of scalars $ \text{extendScalars}(E) $, and its inverse maps an intermediate field $ E' $ between $ F $ and $ L $ to its restriction of scalars $ \text{restrictScalars}(E') $ viewed as an intermediate field between $ K $ and $ L $. This isomorphism preserves the order structure, meaning $ E_1 \leq E_2 $ if and only if $ \text{extendScalars}(E_1) \leq \text{extendScalars}(E_2) $.

IntermediateField.extendScalars_injective theorem

: Function.Injective fun E : { E : IntermediateField K L // F ≤ E } ↦ extendScalars E.2

Full source

theorem extendScalars_injective :
    Function.Injective fun E : { E : IntermediateField K L // F ≤ E } ↦ extendScalars E.2 :=
  (extendScalars.orderIso F).injective

Injectivity of Scalar Extension for Intermediate Fields

Informal description

The function that extends scalars from an intermediate field $E$ (where $F \leq E \leq L$) to an intermediate field between $F$ and $L$ is injective. That is, if two intermediate fields $E_1$ and $E_2$ containing $F$ have the same scalar extension, then $E_1 = E_2$.

IntermediateField.restrict definition

: IntermediateField K E

Full source

/--
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`.
-/
def restrict : IntermediateField K E :=
  (IntermediateField.inclusion h).fieldRange

Restriction of an intermediate field to a smaller extension

Informal description

Given a field extension $ L / K $ and an intermediate field $ F $ between $ K $ and $ L $, the restriction of $ F $ to an intermediate field $ E $ (where $ K \leq E \leq L $) is the intermediate field of $ E / K $ consisting of all elements of $ E $ that are also in $ F $. This is constructed as the field range of the inclusion map from $ E $ to $ L $ restricted to $ F $.

IntermediateField.mem_restrict theorem

(x : E) : x ∈ restrict h ↔ x.1 ∈ F

Full source

theorem mem_restrict (x : E) : x ∈ restrict hx ∈ restrict h ↔ x.1 ∈ F :=
  Set.ext_iff.mp (Set.range_inclusion h) x

Membership Criterion for Restricted Intermediate Field

Informal description

For any element $x$ in the intermediate field $E$ (where $K \leq E \leq L$), $x$ belongs to the restriction of $F$ to $E$ if and only if $x$ (viewed as an element of $L$) belongs to $F$.

IntermediateField.lift_restrict theorem

: lift (restrict h) = F

Full source

@[simp]
theorem lift_restrict : lift (restrict h) = F := by
  ext x
  refine ⟨fun hx ↦ ?_, fun hx ↦ ?_⟩
  · let y : E := ⟨x, lift_le (restrict h) hx⟩
    exact (mem_restrict h y).1 ((mem_lift y).1 hx)
  · let y : E := ⟨x, h hx⟩
    exact (mem_lift y).2 ((mem_restrict h y).2 hx)

Lift-Restrict Identity for Intermediate Fields: $\text{lift}(\text{restrict}(F)) = F$

Informal description

Given a field extension $ L / K $ and an intermediate field $ F $ between $ K $ and $ L $, the lift of the restriction of $ F $ to an intermediate field $ E $ (where $ K \leq E \leq L $) is equal to $ F $. In other words, for any intermediate field $ F $ between $ K $ and $ L $, we have $\text{lift}(\text{restrict}(F)) = F$.

IntermediateField.restrict_algEquiv definition

: F ≃ₐ[K] ↥(IntermediateField.restrict h)

Full source

/--
`F` is equivalent to `F` as an intermediate field of `E / K`.
-/
noncomputable def restrict_algEquiv :
    F ≃ₐ[K] ↥(IntermediateField.restrict h) :=
  AlgEquiv.ofInjectiveField _

Algebraic equivalence between an intermediate field and its restriction

Informal description

Given a field extension $ L / K $ and an intermediate field $ F $ between $ K $ and $ L $, the restriction of $ F $ to an intermediate field $ E $ (where $ K \leq E \leq L $) is algebraically equivalent to $ F $ over $ K $. In other words, there exists a field isomorphism $ F \cong \text{restrict } h $ as $ K $-algebras, where $ \text{restrict } h $ is the intermediate field of $ E / K $ consisting of all elements of $ E $ that are also in $ F $.

Mathlib.FieldTheory.IntermediateField.Basic

Main definitions

Implementation notes

Tags