Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

IntermediateField.adjoin definition

: IntermediateField F E

Full source

/-- `adjoin F S` extends a field `F` by adjoining a set `S ⊆ E`. -/
@[stacks 09FZ "first part"]
def adjoin : IntermediateField F E :=
  { Subfield.closure (Set.rangeSet.range (algebraMap F E) ∪ S) with
    algebraMap_mem' := fun x => Subfield.subset_closure (Or.inl (Set.mem_range_self x)) }

Field adjunction $ F(S) $

Informal description

Given a field extension $ E $ of $ F $ and a subset $ S \subseteq E $, the field $ F(S) $ is the smallest intermediate field between $ F $ and $ E $ containing $ S $. It is constructed as the subfield closure of the union of the image of the canonical embedding $ F \hookrightarrow E $ and the set $ S $.

IntermediateField.adjoin_toSubfield theorem

: (adjoin F S).toSubfield = Subfield.closure (Set.range (algebraMap F E) ∪ S)

Full source

@[simp]
theorem adjoin_toSubfield :
    (adjoin F S).toSubfield = Subfield.closure (Set.rangeSet.range (algebraMap F E) ∪ S) := rfl

Subfield Structure of Field Adjoin $F(S)$

Informal description

For a field extension $E$ of $F$ and a subset $S \subseteq E$, the underlying subfield of the intermediate field $F(S)$ is equal to the subfield closure of the union of the range of the canonical embedding $F \hookrightarrow E$ and the set $S$. In symbols: $$(F(S))_{\text{subfield}} = \text{closure}\big(\text{range}(F \to E) \cup S\big)$$

IntermediateField.mem_adjoin_iff_div theorem

{x : E} : x ∈ adjoin F S ↔ ∃ r ∈ Algebra.adjoin F S, ∃ s ∈ Algebra.adjoin F S, x = r / s

Full source

theorem mem_adjoin_iff_div {x : E} : x ∈ adjoin F Sx ∈ adjoin F S ↔
    ∃ r ∈ Algebra.adjoin F S, ∃ s ∈ Algebra.adjoin F S, x = r / s := by
  simp_rw [adjoin, mem_mk, Subring.mem_toSubsemiring, Subfield.mem_toSubring,
    Subfield.mem_closure_iff, ← Algebra.adjoin_eq_ring_closure, Subalgebra.mem_toSubring, eq_comm]

Characterization of Elements in Field Adjoin $F(S)$ via Quotients

Informal description

Let $E$ be a field extension of $F$ and $S \subseteq E$ a subset. An element $x \in E$ belongs to the field adjunction $F(S)$ if and only if there exist elements $r, s$ in the algebra adjunction $F(S)$ such that $x = r/s$.

IntermediateField.adjoin_le_iff theorem

{S : Set E} {T : IntermediateField F E} : adjoin F S ≤ T ↔ S ⊆ T

Full source

@[simp]
theorem adjoin_le_iff {S : Set E} {T : IntermediateField F E} : adjoinadjoin F S ≤ T ↔ S ⊆ T :=
  ⟨fun H => le_trans (le_trans Set.subset_union_right Subfield.subset_closure) H, fun H =>
    (@Subfield.closure_le E _ (Set.range (algebraMap F E) ∪ S) T.toSubfield).mpr
      (Set.union_subset (IntermediateField.set_range_subset T) H)⟩

Field Adjoin Containment Criterion: $F(S) \leq T \leftrightarrow S \subseteq T$

Informal description

Let $F$ be a field, $E$ a field extension of $F$, $S$ a subset of $E$, and $T$ an intermediate field between $F$ and $E$. Then the field adjunction $F(S)$ is contained in $T$ if and only if $S$ is a subset of $T$. In symbols: $$F(S) \leq T \leftrightarrow S \subseteq T$$

IntermediateField.gc theorem

: GaloisConnection (adjoin F : Set E → IntermediateField F E) (fun (x : IntermediateField F E) => (x : Set E))

Full source

theorem gc : GaloisConnection (adjoin F : Set E → IntermediateField F E)
    (fun (x : IntermediateField F E) => (x : Set E)) := fun _ _ =>
  adjoin_le_iff

Galois Connection Between Field Adjoin and Subset Coercion

Informal description

Let $F$ be a field and $E$ a field extension of $F$. The field adjunction operation $\text{adjoin}\,F : \mathcal{P}(E) \to \text{IntermediateField}\,F\,E$ and the coercion from intermediate fields back to subsets of $E$ form a Galois connection. That is, for any subset $S \subseteq E$ and any intermediate field $T$ between $F$ and $E$, we have: $$\text{adjoin}\,F\,S \leq T \leftrightarrow S \subseteq (T : \mathcal{P}(E))$$ where $\leq$ denotes the partial order on intermediate fields induced by inclusion.

IntermediateField.gi definition

: GaloisInsertion (adjoin F : Set E → IntermediateField F E) (fun (x : IntermediateField F E) => (x : Set E))

Full source

/-- Galois insertion between `adjoin` and `coe`. -/
def gi : GaloisInsertion (adjoin F : Set E → IntermediateField F E)
    (fun (x : IntermediateField F E) => (x : Set E)) where
  choice s hs := (adjoin F s).copy s <| le_antisymm (gc.le_u_l s) hs
  gc := IntermediateField.gc
  le_l_u S := (IntermediateField.gc (S : Set E) (adjoin F S)).1 <| le_rfl
  choice_eq _ _ := copy_eq _ _ _

Galois insertion between field adjunction and subset coercion

Informal description

The Galois insertion between the field adjunction operation $\text{adjoin}\,F : \mathcal{P}(E) \to \text{IntermediateField}\,F\,E$ and the coercion from intermediate fields back to subsets of $E$. Specifically, for any subset $S \subseteq E$, $\text{adjoin}\,F\,S$ is the smallest intermediate field containing $S$, and for any intermediate field $T$, the coercion $(T : \mathcal{P}(E))$ is the underlying subset of $E$. The Galois insertion satisfies $\text{adjoin}\,F\,(T : \mathcal{P}(E)) = T$ for any intermediate field $T$.

IntermediateField.instCompleteLattice instance

: CompleteLattice (IntermediateField F E)

Full source

instance : CompleteLattice (IntermediateField F E) where
  __ := GaloisInsertion.liftCompleteLattice IntermediateField.gi
  bot :=
    { toSubalgebra := ⊥
      inv_mem' := by rintro x ⟨r, rfl⟩; exact ⟨r⁻¹, map_inv₀ _ _⟩ }
  bot_le x := (bot_le : ⊥ ≤ x.toSubalgebra)

Complete Lattice Structure on Intermediate Fields

Informal description

The collection of intermediate fields between fields $F$ and $E$ forms a complete lattice, where the order is given by inclusion and the supremum (resp. infimum) of a family of intermediate fields is the smallest (resp. largest) intermediate field containing (resp. contained in) all members of the family.

IntermediateField.sup_def theorem

(S T : IntermediateField F E) : S ⊔ T = adjoin F (S ∪ T : Set E)

Full source

theorem sup_def (S T : IntermediateField F E) : S ⊔ T = adjoin F (S ∪ T : Set E) := rfl

Supremum of Intermediate Fields as Field Adjunction of Union

Informal description

For any two intermediate fields $S$ and $T$ between fields $F$ and $E$, the supremum $S \sqcup T$ in the lattice of intermediate fields is equal to the field adjunction $F(S \cup T)$, where $S \cup T$ denotes the union of $S$ and $T$ as subsets of $E$.

IntermediateField.sSup_def theorem

(S : Set (IntermediateField F E)) : sSup S = adjoin F (⋃₀ (SetLike.coe '' S))

Full source

theorem sSup_def (S : Set (IntermediateField F E)) :
    sSup S = adjoin F (⋃₀ (SetLike.coe '' S)) := rfl

Supremum of Intermediate Fields as Adjoint of Union

Informal description

For any set $S$ of intermediate fields between fields $F$ and $E$, the supremum of $S$ in the lattice of intermediate fields is equal to the field adjunction $F(\bigcup_{K \in S} K)$, where $\bigcup_{K \in S} K$ denotes the union of all intermediate fields in $S$.

IntermediateField.instInhabited instance

: Inhabited (IntermediateField F E)

Full source

instance : Inhabited (IntermediateField F E) :=
  ⟨⊤⟩

Nonempty Intermediate Fields Between Fields

Informal description

For any fields $F$ and $E$ with $F$ a subfield of $E$, the collection of intermediate fields between $F$ and $E$ is nonempty.

IntermediateField.instUnique instance

: Unique (IntermediateField F F)

Full source

instance : Unique (IntermediateField F F) :=
  { inferInstanceAs (Inhabited (IntermediateField F F)) with
    uniq := fun _ ↦ toSubalgebra_injective <| Subsingleton.elim _ _ }

Uniqueness of the Trivial Intermediate Field

Informal description

For any field $F$, there is exactly one intermediate field between $F$ and itself, namely $F$ viewed as a subfield of itself.

IntermediateField.coe_bot theorem

: ↑(⊥ : IntermediateField F E) = Set.range (algebraMap F E)

Full source

theorem coe_bot : ↑(⊥ : IntermediateField F E) = Set.range (algebraMap F E) := rfl

Characterization of the Minimal Intermediate Field as the Image of the Base Field

Informal description

The smallest intermediate field between fields $F$ and $E$, denoted $\bot$, is equal to the range of the canonical embedding $\text{algebraMap} : F \to E$. In other words, $\bot = \{x \in E \mid \exists y \in F, \text{algebraMap}(y) = x\}$.

IntermediateField.mem_bot theorem

{x : E} : x ∈ (⊥ : IntermediateField F E) ↔ x ∈ Set.range (algebraMap F E)

Full source

theorem mem_bot {x : E} : x ∈ (⊥ : IntermediateField F E)x ∈ (⊥ : IntermediateField F E) ↔ x ∈ Set.range (algebraMap F E) :=
  Iff.rfl

Characterization of Elements in the Smallest Intermediate Field

Informal description

For any element $x$ in the field extension $E$ of $F$, $x$ belongs to the smallest intermediate field $\bot$ between $F$ and $E$ if and only if $x$ is in the range of the canonical field homomorphism from $F$ to $E$.

IntermediateField.bot_toSubalgebra theorem

: (⊥ : IntermediateField F E).toSubalgebra = ⊥

Full source

@[simp]
theorem bot_toSubalgebra : (⊥ : IntermediateField F E).toSubalgebra = ⊥ := rfl

Bottom Intermediate Field Maps to Bottom Subalgebra

Informal description

The subalgebra corresponding to the bottom element of the lattice of intermediate fields between $F$ and $E$ is equal to the bottom element of the lattice of subalgebras, i.e., $(\bot : \text{IntermediateField}\,F\,E).\text{toSubalgebra} = \bot$.

IntermediateField.bot_toSubfield theorem

: (⊥ : IntermediateField F E).toSubfield = (algebraMap F E).fieldRange

Full source

theorem bot_toSubfield : (⊥ : IntermediateField F E).toSubfield = (algebraMap F E).fieldRange :=
  rfl

Bottom Intermediate Field as Field Range of Algebra Map

Informal description

The subfield corresponding to the bottom element of the lattice of intermediate fields between $F$ and $E$ is equal to the field range of the algebra map from $F$ to $E$.

IntermediateField.coe_top theorem

: ↑(⊤ : IntermediateField F E) = (Set.univ : Set E)

Full source

@[simp]
theorem coe_top : ↑(⊤ : IntermediateField F E) = (Set.univ : Set E) :=
  rfl

Top Intermediate Field as Universal Set

Informal description

The underlying set of the top intermediate field between fields $F$ and $E$ is equal to the universal set of $E$, i.e., $\top_{\text{IntermediateField}\,F\,E} = \text{univ}_E$.

IntermediateField.mem_top theorem

{x : E} : x ∈ (⊤ : IntermediateField F E)

Full source

@[simp]
theorem mem_top {x : E} : x ∈ (⊤ : IntermediateField F E) :=
  trivial

Every Element Belongs to the Top Intermediate Field

Informal description

For any element $x$ in the field extension $E$ of $F$, $x$ belongs to the largest intermediate field between $F$ and $E$.

IntermediateField.top_toSubalgebra theorem

: (⊤ : IntermediateField F E).toSubalgebra = ⊤

Full source

@[simp]
theorem top_toSubalgebra : (⊤ : IntermediateField F E).toSubalgebra = ⊤ :=
  rfl

Top Intermediate Field Subalgebra Correspondence

Informal description

The subalgebra associated with the top element in the lattice of intermediate fields between $F$ and $E$ is equal to the top element in the lattice of subalgebras of $E$ over $F$. In other words, $(⊤ : \text{IntermediateField } F E).\text{toSubalgebra} = ⊤$.

IntermediateField.top_toSubfield theorem

: (⊤ : IntermediateField F E).toSubfield = ⊤

Full source

@[simp]
theorem top_toSubfield : (⊤ : IntermediateField F E).toSubfield = ⊤ :=
  rfl

Top Intermediate Field's Subfield is Top Subfield

Informal description

The underlying subfield of the top intermediate field between fields $F$ and $E$ is equal to the top subfield of $E$.

IntermediateField.coe_inf theorem

(S T : IntermediateField F E) : (↑(S ⊓ T) : Set E) = (S : Set E) ∩ T

Full source

@[simp, norm_cast]
theorem coe_inf (S T : IntermediateField F E) : (↑(S ⊓ T) : Set E) = (S : Set E) ∩ T :=
  rfl

Infimum of Intermediate Fields as Set Intersection

Informal description

For any intermediate fields $S$ and $T$ between fields $F$ and $E$, the underlying set of their infimum $S \sqcap T$ is equal to the intersection of the underlying sets of $S$ and $T$, i.e., $(S \sqcap T) = S \cap T$ as subsets of $E$.

IntermediateField.mem_inf theorem

{S T : IntermediateField F E} {x : E} : x ∈ S ⊓ T ↔ x ∈ S ∧ x ∈ T

Full source

@[simp]
theorem mem_inf {S T : IntermediateField F E} {x : E} : x ∈ S ⊓ Tx ∈ S ⊓ T ↔ x ∈ S ∧ x ∈ T :=
  Iff.rfl

Membership in Intersection of Intermediate Fields

Informal description

For any intermediate fields $S$ and $T$ between fields $F$ and $E$, and any element $x \in E$, we have $x \in S \cap T$ if and only if $x \in S$ and $x \in T$.

IntermediateField.inf_toSubalgebra theorem

(S T : IntermediateField F E) : (S ⊓ T).toSubalgebra = S.toSubalgebra ⊓ T.toSubalgebra

Full source

@[simp]
theorem inf_toSubalgebra (S T : IntermediateField F E) :
    (S ⊓ T).toSubalgebra = S.toSubalgebra ⊓ T.toSubalgebra :=
  rfl

Infimum of Intermediate Fields Preserves Subalgebra Structure

Informal description

For any intermediate fields $S$ and $T$ between fields $F$ and $E$, the underlying subalgebra of their infimum $S \sqcap T$ is equal to the infimum of their underlying subalgebras, i.e., $(S \sqcap T).\text{toSubalgebra} = S.\text{toSubalgebra} \sqcap T.\text{toSubalgebra}$.

IntermediateField.inf_toSubfield theorem

(S T : IntermediateField F E) : (S ⊓ T).toSubfield = S.toSubfield ⊓ T.toSubfield

Full source

@[simp]
theorem inf_toSubfield (S T : IntermediateField F E) :
    (S ⊓ T).toSubfield = S.toSubfield ⊓ T.toSubfield :=
  rfl

Infimum of Intermediate Fields Preserves Subfield Structure

Informal description

For any intermediate fields $S$ and $T$ between fields $F$ and $E$, the underlying subfield of their infimum $S \sqcap T$ is equal to the infimum of their underlying subfields $S.\text{toSubfield} \sqcap T.\text{toSubfield}$.

IntermediateField.sup_toSubfield theorem

(S T : IntermediateField F E) : (S ⊔ T).toSubfield = S.toSubfield ⊔ T.toSubfield

Full source

@[simp]
theorem sup_toSubfield (S T : IntermediateField F E) :
    (S ⊔ T).toSubfield = S.toSubfield ⊔ T.toSubfield := by
  rw [← S.toSubfield.closure_eq, ← T.toSubfield.closure_eq, ← Subfield.closure_union]
  simp_rw [sup_def, adjoin_toSubfield, coe_toSubfield]
  congr 1
  rw [Set.union_eq_right]
  rintro _ ⟨x, rfl⟩
  exact Set.mem_union_left _ (algebraMap_mem S x)

Supremum of Intermediate Fields Preserves Subfield Structure

Informal description

For any intermediate fields $S$ and $T$ between fields $F$ and $E$, the underlying subfield of the supremum $S \sqcup T$ is equal to the supremum of the underlying subfields of $S$ and $T$. That is, \[ (S \sqcup T).toSubfield = S.toSubfield \sqcup T.toSubfield. \]

IntermediateField.coe_sInf theorem

 (S : Set (IntermediateField F E)) : (↑(sInf S) : Set E) = sInf ((fun (x : IntermediateField F E) => (x : Set E)) '' S)

Full source

@[simp, norm_cast]
theorem coe_sInf (S : Set (IntermediateField F E)) : (↑(sInf S) : Set E) =
    sInf ((fun (x : IntermediateField F E) => (x : Set E)) '' S) :=
  rfl

Infimum of Intermediate Fields as Sets

Informal description

For any set $S$ of intermediate fields between fields $F$ and $E$, the underlying set of the infimum of $S$ is equal to the infimum of the images of the underlying sets of each intermediate field in $S$. That is, \[ \inf S = \inf \{K \mid K \in S\} \] as subsets of $E$.

IntermediateField.sInf_toSubalgebra theorem

(S : Set (IntermediateField F E)) : (sInf S).toSubalgebra = sInf (toSubalgebra '' S)

Full source

@[simp]
theorem sInf_toSubalgebra (S : Set (IntermediateField F E)) :
    (sInf S).toSubalgebra = sInf (toSubalgebratoSubalgebra '' S) :=
  SetLike.coe_injective <| by simp [Set.sUnion_image]

Infimum of Intermediate Fields Preserves Subalgebra Structure

Informal description

For any set $S$ of intermediate fields between fields $F$ and $E$, the underlying subalgebra of the infimum of $S$ is equal to the infimum of the images of the subalgebras associated to each intermediate field in $S$. That is, \[ (\inf S).toSubalgebra = \inf \{K.toSubalgebra \mid K \in S\}. \]

IntermediateField.sInf_toSubfield theorem

(S : Set (IntermediateField F E)) : (sInf S).toSubfield = sInf (toSubfield '' S)

Full source

@[simp]
theorem sInf_toSubfield (S : Set (IntermediateField F E)) :
    (sInf S).toSubfield = sInf (toSubfieldtoSubfield '' S) :=
  SetLike.coe_injective <| by simp [Set.sUnion_image]

Infimum of Intermediate Fields Preserves Subfield Structure

Informal description

For any set $S$ of intermediate fields between fields $F$ and $E$, the underlying subfield of the infimum of $S$ is equal to the infimum of the images of the subfields associated to each intermediate field in $S$. That is, \[ (\inf S).toSubfield = \inf \{K.toSubfield \mid K \in S\}. \]

IntermediateField.sSup_toSubfield theorem

(S : Set (IntermediateField F E)) (hS : S.Nonempty) : (sSup S).toSubfield = sSup (toSubfield '' S)

Full source

@[simp]
theorem sSup_toSubfield (S : Set (IntermediateField F E)) (hS : S.Nonempty) :
    (sSup S).toSubfield = sSup (toSubfieldtoSubfield '' S) := by
  have h : toSubfieldtoSubfield '' S = Subfield.closureSubfield.closure '' (SetLike.coe '' S) := by
    rw [Set.image_image]
    congr! with x
    exact x.toSubfield.closure_eq.symm
  rw [h, sSup_image, ← Subfield.closure_sUnion, sSup_def, adjoin_toSubfield]
  congr 1
  rw [Set.union_eq_right]
  rintro _ ⟨x, rfl⟩
  obtain ⟨y, hy⟩ := hS
  simp only [Set.mem_sUnion, Set.mem_image, exists_exists_and_eq_and, SetLike.mem_coe]
  exact ⟨y, hy, algebraMap_mem y x⟩

Supremum of Intermediate Fields Preserves Subfield Structure

Informal description

For any nonempty set $S$ of intermediate fields between fields $F$ and $E$, the underlying subfield of the supremum of $S$ is equal to the supremum of the images of the subfields associated to each intermediate field in $S$. That is, $$(\sup S)_{\text{subfield}} = \sup \{K_{\text{subfield}} \mid K \in S\}.$$

IntermediateField.coe_iInf theorem

{ι : Sort*} (S : ι → IntermediateField F E) : (↑(iInf S) : Set E) = ⋂ i, S i

Full source

@[simp, norm_cast]
theorem coe_iInf {ι : Sort*} (S : ι → IntermediateField F E) : (↑(iInf S) : Set E) = ⋂ i, S i := by
  simp [iInf]

Infimum of Intermediate Fields as Intersection of Sets

Informal description

For any family of intermediate fields $S_i$ between fields $F$ and $E$ indexed by a type $\iota$, the underlying set of the infimum of the family $\bigsqcap_i S_i$ is equal to the intersection $\bigcap_i S_i$ of the underlying sets of the intermediate fields.

IntermediateField.iInf_toSubalgebra theorem

{ι : Sort*} (S : ι → IntermediateField F E) : (iInf S).toSubalgebra = ⨅ i, (S i).toSubalgebra

Full source

@[simp]
theorem iInf_toSubalgebra {ι : Sort*} (S : ι → IntermediateField F E) :
    (iInf S).toSubalgebra = ⨅ i, (S i).toSubalgebra :=
  SetLike.coe_injective <| by simp [iInf]

Infimum of Intermediate Fields Preserves Subalgebra Structure

Informal description

For any family of intermediate fields $S_i$ between fields $F$ and $E$ indexed by a type $\iota$, the underlying subalgebra of the infimum $\bigsqcap_i S_i$ is equal to the infimum $\bigsqcap_i (S_i).toSubalgebra$ of the underlying subalgebras of the intermediate fields.

IntermediateField.iInf_toSubfield theorem

{ι : Sort*} (S : ι → IntermediateField F E) : (iInf S).toSubfield = ⨅ i, (S i).toSubfield

Full source

@[simp]
theorem iInf_toSubfield {ι : Sort*} (S : ι → IntermediateField F E) :
    (iInf S).toSubfield = ⨅ i, (S i).toSubfield :=
  SetLike.coe_injective <| by simp [iInf]

Infimum of Intermediate Fields Preserves Subfield Structure (Indexed Version)

Informal description

For any family of intermediate fields $S_i$ between fields $F$ and $E$ indexed by a type $\iota$, the underlying subfield of the infimum $\bigsqcap_i S_i$ is equal to the infimum $\bigsqcap_i (S_i).toSubfield$ of the underlying subfields of the intermediate fields in the family.

IntermediateField.iSup_toSubfield theorem

{ι : Sort*} [Nonempty ι] (S : ι → IntermediateField F E) : (iSup S).toSubfield = ⨆ i, (S i).toSubfield

Full source

@[simp]
theorem iSup_toSubfield {ι : Sort*} [Nonempty ι] (S : ι → IntermediateField F E) :
    (iSup S).toSubfield = ⨆ i, (S i).toSubfield := by
  simp only [iSup, Set.range_nonempty, sSup_toSubfield, ← Set.range_comp, Function.comp_def]

Supremum of Intermediate Fields Preserves Subfield Structure (Indexed Version)

Informal description

For any nonempty index type $\iota$ and any family of intermediate fields $S_i$ between fields $F$ and $E$ indexed by $\iota$, the underlying subfield of the supremum $\bigsqcup_i S_i$ is equal to the supremum $\bigsqcup_i (S_i).toSubfield$ of the underlying subfields of the intermediate fields in the family.

IntermediateField.equivOfEq definition

{S T : IntermediateField F E} (h : S = T) : S ≃ₐ[F] T

Full source

/-- Construct an algebra isomorphism from an equality of intermediate fields -/
@[simps! apply]
def equivOfEq {S T : IntermediateField F E} (h : S = T) : S ≃ₐ[F] T :=
  Subalgebra.equivOfEq _ _ (congr_arg toSubalgebra h)

Algebra isomorphism between equal intermediate fields

Informal description

Given two intermediate fields $ S $ and $ T $ of a field extension $ E $ over $ F $, if $ S = T $, then there exists an algebra isomorphism $ S \simeq T $ over $ F $.

IntermediateField.equivOfEq_symm theorem

{S T : IntermediateField F E} (h : S = T) : (equivOfEq h).symm = equivOfEq h.symm

Full source

@[simp]
theorem equivOfEq_symm {S T : IntermediateField F E} (h : S = T) :
    (equivOfEq h).symm = equivOfEq h.symm :=
  rfl

Inverse of Algebra Isomorphism Between Equal Intermediate Fields

Informal description

Given two intermediate fields $ S $ and $ T $ of a field extension $ E $ over $ F $, if $ S = T $, then the inverse of the algebra isomorphism $ \text{equivOfEq} \, h $ is equal to the algebra isomorphism $ \text{equivOfEq} \, h^{\text{symm}} $, where $ h^{\text{symm}} $ is the symmetry of the equality $ h $.

IntermediateField.equivOfEq_rfl theorem

(S : IntermediateField F E) : equivOfEq (rfl : S = S) = AlgEquiv.refl

Full source

@[simp]
theorem equivOfEq_rfl (S : IntermediateField F E) : equivOfEq (rfl : S = S) = AlgEquiv.refl := by
  ext; rfl

Identity Algebra Isomorphism for Reflexive Equality of Intermediate Fields

Informal description

For any intermediate field $S$ of a field extension $E$ over $F$, the algebra isomorphism `equivOfEq` applied to the reflexivity proof `rfl : S = S` yields the identity algebra equivalence $\text{AlgEquiv.refl}$ from $S$ to itself.

IntermediateField.equivOfEq_trans theorem

 {S T U : IntermediateField F E} (hST : S = T) (hTU : T = U) :
  (equivOfEq hST).trans (equivOfEq hTU) = equivOfEq (hST.trans hTU)

Full source

@[simp]
theorem equivOfEq_trans {S T U : IntermediateField F E} (hST : S = T) (hTU : T = U) :
    (equivOfEq hST).trans (equivOfEq hTU) = equivOfEq (hST.trans hTU) :=
  rfl

Transitivity of Algebra Isomorphism Between Equal Intermediate Fields

Informal description

For intermediate fields $S$, $T$, and $U$ in a field extension $E$ over $F$, if $S = T$ and $T = U$, then the composition of the algebra isomorphisms $\text{equivOfEq} \, h_{ST}$ and $\text{equivOfEq} \, h_{TU}$ is equal to the algebra isomorphism $\text{equivOfEq} \, (h_{ST} \circ h_{TU})$.

IntermediateField.botEquiv definition

: (⊥ : IntermediateField F E) ≃ₐ[F] F

Full source

/-- The bottom intermediate_field is isomorphic to the field. -/
noncomputable def botEquiv : (⊥ : IntermediateField F E) ≃ₐ[F] F :=
  (Subalgebra.equivOfEq _ _ bot_toSubalgebra).trans (Algebra.botEquiv F E)

Isomorphism between bottom intermediate field and base field

Informal description

The algebra isomorphism between the bottom intermediate field $\bot$ (which is the smallest intermediate field between $F$ and $E$) and the base field $F$. This isomorphism is constructed by first using the equivalence of subalgebras corresponding to the bottom intermediate field and the bottom subalgebra, and then composing with the canonical algebra isomorphism between the bottom subalgebra and $F$.

IntermediateField.botEquiv_def theorem

(x : F) : botEquiv F E (algebraMap F (⊥ : IntermediateField F E) x) = x

Full source

theorem botEquiv_def (x : F) : botEquiv F E (algebraMap F (⊥ : IntermediateField F E) x) = x := by
  simp

Definition of Bottom Intermediate Field Isomorphism on Algebra Map

Informal description

For any element $x$ in the base field $F$, the algebra isomorphism $\text{botEquiv}$ between the bottom intermediate field $\bot$ and $F$ satisfies $\text{botEquiv}(\text{algebraMap}_F^\bot(x)) = x$, where $\text{algebraMap}_F^\bot$ is the canonical algebra map from $F$ to $\bot$.

IntermediateField.botEquiv_symm theorem

(x : F) : (botEquiv F E).symm x = algebraMap F _ x

Full source

@[simp]
theorem botEquiv_symm (x : F) : (botEquiv F E).symm x = algebraMap F _ x :=
  rfl

Inverse of Bottom Intermediate Field Isomorphism Maps to Canonical Embedding

Informal description

For any element $x$ in the field $F$, the inverse of the algebra isomorphism $\text{botEquiv}$ between the bottom intermediate field $\bot$ and $F$ maps $x$ to the canonical algebra embedding of $x$ into $\bot$, i.e., $(\text{botEquiv}_{F,E})^{-1}(x) = \text{algebraMap}_F^\bot(x)$.

IntermediateField.algebraOverBot instance

: Algebra (⊥ : IntermediateField F E) F

Full source

noncomputable instance algebraOverBot : Algebra (⊥ : IntermediateField F E) F :=
  (IntermediateField.botEquiv F E).toAlgHom.toRingHom.toAlgebra

Algebra Structure on Bottom Intermediate Field over Base Field

Informal description

The bottom intermediate field $\bot$ (the smallest intermediate field between $F$ and $E$) has a canonical algebra structure over $F$.

IntermediateField.coe_algebraMap_over_bot theorem

: (algebraMap (⊥ : IntermediateField F E) F : (⊥ : IntermediateField F E) → F) = IntermediateField.botEquiv F E

Full source

theorem coe_algebraMap_over_bot :
    (algebraMap (⊥ : IntermediateField F E) F : (⊥ : IntermediateField F E) → F) =
      IntermediateField.botEquiv F E :=
  rfl

Equality of Algebra Map and Bottom Isomorphism on $\bot$

Informal description

The canonical algebra map from the bottom intermediate field $\bot$ (the smallest intermediate field between $F$ and $E$) to $F$ coincides with the algebra isomorphism $\text{botEquiv}_{F,E}$ when viewed as functions from $\bot$ to $F$. In other words, the restriction of the algebra map to $\bot$ is equal to $\text{botEquiv}_{F,E}$.

IntermediateField.isScalarTower_over_bot instance

: IsScalarTower (⊥ : IntermediateField F E) F E

Full source

instance isScalarTower_over_bot : IsScalarTower (⊥ : IntermediateField F E) F E :=
  IsScalarTower.of_algebraMap_eq
    (by
      intro x
      obtain ⟨y, rfl⟩ := (botEquiv F E).symm.surjective x
      rw [coe_algebraMap_over_bot, (botEquiv F E).apply_symm_apply, botEquiv_symm,
        IsScalarTower.algebraMap_apply F (⊥ : IntermediateField F E) E])

Scalar Tower Property for Bottom Intermediate Field

Informal description

For fields $F \subseteq E$, the smallest intermediate field $\bot$ between $F$ and $E$ forms a scalar tower with $F$ and $E$. That is, the scalar multiplication operations are compatible in the sense that for any $a \in \bot$, $b \in F$, and $c \in E$, we have $(a \cdot b) \cdot c = a \cdot (b \cdot c)$.

IntermediateField.topEquiv definition

: (⊤ : IntermediateField F E) ≃ₐ[F] E

Full source

/-- The top `IntermediateField` is isomorphic to the field.

This is the intermediate field version of `Subalgebra.topEquiv`. -/
@[simps!]
def topEquiv : (⊤ : IntermediateField F E) ≃ₐ[F] E :=
  Subalgebra.topEquiv

Isomorphism between top intermediate field and extension field

Informal description

The top intermediate field between fields $F$ and $E$ is isomorphic to $E$ as an $F$-algebra. This isomorphism is the intermediate field version of the isomorphism between the top subalgebra and the algebra itself.

IntermediateField.restrictScalars_bot_eq_self theorem

(K : IntermediateField F E) : (⊥ : IntermediateField K E).restrictScalars _ = K

Full source

@[simp]
theorem restrictScalars_bot_eq_self (K : IntermediateField F E) :
    (⊥ : IntermediateField K E).restrictScalars _ = K :=
  SetLike.coe_injective Subtype.range_coe

Restriction of Scalars of Bottom Intermediate Field Equals Itself

Informal description

For any intermediate field $K$ between fields $F$ and $E$, the restriction of scalars of the bottom intermediate field (with respect to $K$ and $E$) is equal to $K$ itself. That is, $(\bot : \text{IntermediateField}\ K\ E).\text{restrictScalars}\ F = K$.

IntermediateField.restrictScalars_top theorem

: (⊤ : IntermediateField F E).restrictScalars K = ⊤

Full source

@[simp]
theorem restrictScalars_top : (⊤ : IntermediateField F E).restrictScalars K = ⊤ :=
  rfl

Restriction of Scalars Preserves Top Intermediate Field

Informal description

Let $F$ and $E$ be fields with $F \subseteq E$, and let $K$ be an intermediate field between $F$ and $E$. Then the restriction of scalars of the top intermediate field (i.e., $E$ itself) to $K$ is equal to the top intermediate field over $K$, i.e., $(\top : \text{IntermediateField}\, F\, E).\text{restrictScalars}\, K = \top$.

IntermediateField.restrictScalars_sup theorem

: L.restrictScalars K ⊔ L'.restrictScalars K = (L ⊔ L').restrictScalars K

Full source

theorem restrictScalars_sup :
    L.restrictScalars K ⊔ L'.restrictScalars K = (L ⊔ L').restrictScalars K :=
  toSubfield_injective (by simp)

Supremum Commutes with Scalar Restriction in Intermediate Fields

Informal description

For any intermediate fields $L$ and $L'$ between fields $F$ and $E$, the supremum of their scalar restrictions to $K$ is equal to the scalar restriction to $K$ of their supremum. That is, $$ L|_K \sqcup L'|_K = (L \sqcup L')|_K $$ where $|_K$ denotes the restriction of scalars to $K$.

IntermediateField.restrictScalars_inf theorem

: L.restrictScalars K ⊓ L'.restrictScalars K = (L ⊓ L').restrictScalars K

Full source

theorem restrictScalars_inf :
    L.restrictScalars K ⊓ L'.restrictScalars K = (L ⊓ L').restrictScalars K := rfl

Infimum Commutes with Scalar Restriction in Intermediate Fields

Informal description

For any intermediate fields $L$ and $L'$ between fields $F$ and $E$, the infimum of their scalar restrictions to $K$ is equal to the scalar restriction to $K$ of their infimum. That is, $$ L|_K \sqcap L'|_K = (L \sqcap L')|_K $$ where $|_K$ denotes the restriction of scalars to $K$.

IntermediateField.map_bot theorem

(f : E →ₐ[F] K) : IntermediateField.map f ⊥ = ⊥

Full source

@[simp]
theorem map_bot (f : E →ₐ[F] K) :
    IntermediateField.map f ⊥ = ⊥ :=
  toSubalgebra_injective <| Algebra.map_bot _

Image of Trivial Intermediate Field under Field Homomorphism is Trivial

Informal description

For any field homomorphism $f \colon E \to K$ that fixes $F$ (i.e., an $F$-algebra homomorphism), the image of the trivial intermediate field $\bot$ (the smallest intermediate field between $F$ and $E$) under $f$ is the trivial intermediate field $\bot$ in $K$.

IntermediateField.map_sup theorem

(s t : IntermediateField F E) (f : E →ₐ[F] K) : (s ⊔ t).map f = s.map f ⊔ t.map f

Full source

theorem map_sup (s t : IntermediateField F E) (f : E →ₐ[F] K) : (s ⊔ t).map f = s.map f ⊔ t.map f :=
  (gc_map_comap f).l_sup

Supremum Preservation Under Field Homomorphism: $f(s \sqcup t) = f(s) \sqcup f(t)$

Informal description

Let $F$ and $E$ be fields with $F \subseteq E$, and let $K$ be another field. For any two intermediate fields $s, t$ between $F$ and $E$, and any field homomorphism $f: E \to K$ that fixes $F$, the image of the supremum $s \sqcup t$ under $f$ equals the supremum of the images of $s$ and $t$ under $f$, i.e., $f(s \sqcup t) = f(s) \sqcup f(t)$.

IntermediateField.map_iSup theorem

{ι : Sort*} (f : E →ₐ[F] K) (s : ι → IntermediateField F E) : (iSup s).map f = ⨆ i, (s i).map f

Full source

theorem map_iSup {ι : Sort*} (f : E →ₐ[F] K) (s : ι → IntermediateField F E) :
    (iSup s).map f = ⨆ i, (s i).map f :=
  (gc_map_comap f).l_iSup

Supremum Preservation Under Field Homomorphism

Informal description

Let $F$ and $E$ be fields with $F \subseteq E$, and let $K$ be another field extension of $F$. Given an $F$-algebra homomorphism $f: E \to K$ and a family of intermediate fields $(s_i)_{i \in \iota}$ between $F$ and $E$, the image under $f$ of the smallest intermediate field containing all $s_i$ equals the smallest intermediate field containing all $f(s_i)$. In symbols: $$ f\left(\bigvee_i s_i\right) = \bigvee_i f(s_i) $$ where $\bigvee$ denotes the supremum in the lattice of intermediate fields.

IntermediateField.map_inf theorem

(s t : IntermediateField F E) (f : E →ₐ[F] K) : (s ⊓ t).map f = s.map f ⊓ t.map f

Full source

theorem map_inf (s t : IntermediateField F E) (f : E →ₐ[F] K) :
    (s ⊓ t).map f = s.map f ⊓ t.map f := SetLike.coe_injective (Set.image_inter f.injective)

Image of Intersection of Intermediate Fields under Algebra Homomorphism

Informal description

Let $F$ be a field, $E$ and $K$ be field extensions of $F$, and $s, t$ be intermediate fields between $F$ and $E$. For any $F$-algebra homomorphism $f: E \to K$, the image of the intersection $s \cap t$ under $f$ equals the intersection of the images of $s$ and $t$ under $f$, i.e., $f(s \cap t) = f(s) \cap f(t)$.

IntermediateField.map_iInf theorem

{ι : Sort*} [Nonempty ι] (f : E →ₐ[F] K) (s : ι → IntermediateField F E) : (iInf s).map f = ⨅ i, (s i).map f

Full source

theorem map_iInf {ι : Sort*} [Nonempty ι] (f : E →ₐ[F] K) (s : ι → IntermediateField F E) :
    (iInf s).map f = ⨅ i, (s i).map f := by
  apply SetLike.coe_injective
  simpa using (Set.injOn_of_injective f.injective).image_iInter_eq (s := SetLike.coeSetLike.coe ∘ s)

Infimum Preservation Under Field Homomorphism

Informal description

Let $F$ be a field, $E$ and $K$ be field extensions of $F$, and $\{s_i\}_{i \in \iota}$ be a nonempty family of intermediate fields between $F$ and $E$. For any $F$-algebra homomorphism $f: E \to K$, the image under $f$ of the largest intermediate field contained in all $s_i$ equals the largest intermediate field contained in all $f(s_i)$. In symbols: $$ f\left(\bigsqcap_i s_i\right) = \bigsqcap_i f(s_i) $$ where $\bigsqcap$ denotes the infimum in the lattice of intermediate fields.

AlgHom.fieldRange_eq_map theorem

(f : E →ₐ[F] K) : f.fieldRange = IntermediateField.map f ⊤

Full source

theorem _root_.AlgHom.fieldRange_eq_map (f : E →ₐ[F] K) :
    f.fieldRange = IntermediateField.map f ⊤ :=
  SetLike.ext' Set.image_univ.symm

Field Range as Image of Top Intermediate Field under Algebra Homomorphism

Informal description

For any field homomorphism $f \colon E \to K$ that is an $F$-algebra homomorphism (where $F$ is a subfield of both $E$ and $K$), the field range of $f$ is equal to the image of the top intermediate field under $f$. That is, $\text{fieldRange}(f) = f(\top)$, where $\top$ represents the largest intermediate field between $F$ and $E$.

AlgHom.map_fieldRange theorem

 {L : Type*} [Field L] [Algebra F L] (f : E →ₐ[F] K) (g : K →ₐ[F] L) : f.fieldRange.map g = (g.comp f).fieldRange

Full source

theorem _root_.AlgHom.map_fieldRange {L : Type*} [Field L] [Algebra F L]
    (f : E →ₐ[F] K) (g : K →ₐ[F] L) : f.fieldRange.map g = (g.comp f).fieldRange :=
  SetLike.ext' (Set.range_comp g f).symm

Field Range Preservation under Composition of Algebra Homomorphisms

Informal description

Let $F$, $E$, $K$, and $L$ be fields with $F$ as a subfield of $E$, $K$, and $L$ via the respective algebra structures. Given an $F$-algebra homomorphism $f: E \to K$ and an $F$-algebra homomorphism $g: K \to L$, the image of the field range of $f$ under $g$ is equal to the field range of the composition $g \circ f$. In other words, $g(f(\mathrm{fieldRange}(f))) = \mathrm{fieldRange}(g \circ f)$.

AlgHom.fieldRange_eq_top theorem

{f : E →ₐ[F] K} : f.fieldRange = ⊤ ↔ Function.Surjective f

Full source

theorem _root_.AlgHom.fieldRange_eq_top {f : E →ₐ[F] K} :
    f.fieldRange = ⊤ ↔ Function.Surjective f :=
  SetLike.ext'_iff.trans Set.range_eq_univ

Field Range Equals Codomain iff Homomorphism is Surjective

Informal description

For an $F$-algebra homomorphism $f \colon E \to K$ between fields, the field range of $f$ is equal to the entire field $K$ if and only if $f$ is surjective. In other words, $f(\text{fieldRange}) = K \leftrightarrow f \text{ is surjective}$.

AlgEquiv.fieldRange_eq_top theorem

(f : E ≃ₐ[F] K) : (f : E →ₐ[F] K).fieldRange = ⊤

Full source

@[simp]
theorem _root_.AlgEquiv.fieldRange_eq_top (f : E ≃ₐ[F] K) :
    (f : E →ₐ[F] K).fieldRange = ⊤ :=
  AlgHom.fieldRange_eq_top.mpr f.surjective

Field Range of Algebra Isomorphism is Entire Codomain

Informal description

For any field isomorphism $f \colon E \to K$ of $F$-algebras, the field range of $f$ (considered as an $F$-algebra homomorphism) is equal to the entire field $K$.

IntermediateField.fieldRange_comp_val theorem

: (f.comp L.val).fieldRange = L.map f

Full source

theorem fieldRange_comp_val : (f.comp L.val).fieldRange = L.map f := toSubalgebra_injective <| by
  rw [toSubalgebra_map, AlgHom.fieldRange_toSubalgebra, AlgHom.range_comp, range_val]

Field Range of Composition Equals Image of Intermediate Field

Informal description

For any field homomorphism $f \colon E \to K$ over $F$ and any intermediate field $L$ between $F$ and $E$, the field range of the composition $f \circ \mathrm{val}_L$ is equal to the image of $L$ under $f$, i.e., $\mathrm{fieldRange}(f \circ \mathrm{val}_L) = f(L)$.

IntermediateField.equivMap definition

: L ≃ₐ[F] L.map f

Full source

/-- An intermediate field is isomorphic to its image under an `AlgHom`
(which is automatically injective) -/
noncomputable def equivMap : L ≃ₐ[F] L.map f :=
  (AlgEquiv.ofInjective _ (f.comp L.val).injective).trans (equivOfEq (fieldRange_comp_val L f))

Algebra isomorphism between an intermediate field and its image under an algebra homomorphism

Informal description

Given an intermediate field $ L $ between $ F $ and $ E $, and an algebra homomorphism $ f \colon E \to K $ over $ F $, the map $ \text{equivMap} $ is an algebra isomorphism between $ L $ and its image $ f(L) $ under $ f $.

IntermediateField.coe_equivMap_apply theorem

(x : L) : ↑(equivMap L f x) = f x

Full source

@[simp]
theorem coe_equivMap_apply (x : L) : ↑(equivMap L f x) = f x := rfl

Image of Element under Algebra Isomorphism Equals its Image under Homomorphism

Informal description

For any element $x$ in the intermediate field $L$, the image of $x$ under the algebra isomorphism $\text{equivMap}\, L\, f$ is equal to $f(x)$, i.e., $\text{equivMap}\, L\, f\, x = f(x)$.

IntermediateField.adjoin_eq_range_algebraMap_adjoin theorem

: (adjoin F S : Set E) = Set.range (algebraMap (adjoin F S) E)

Full source

theorem adjoin_eq_range_algebraMap_adjoin :
    (adjoin F S : Set E) = Set.range (algebraMap (adjoin F S) E) :=
  Subtype.range_coe.symm

Field Adjunction as Range of Algebra Map

Informal description

For a field extension $E$ of $F$ and a subset $S \subseteq E$, the set underlying the field $F(S)$ (the adjunction of $S$ to $F$) is equal to the range of the algebra homomorphism from $F(S)$ to $E$. In other words, $(F(S) : \text{Set } E) = \text{range}(\text{algebraMap}_{F(S) \to E})$.

IntermediateField.adjoin.algebraMap_mem theorem

(x : F) : algebraMap F E x ∈ adjoin F S

Full source

theorem adjoin.algebraMap_mem (x : F) : algebraMapalgebraMap F E x ∈ adjoin F S :=
  IntermediateField.algebraMap_mem (adjoin F S) x

Canonical Algebra Map Preserves Membership in Field Adjunction

Informal description

For any element $x$ in the field $F$, the image of $x$ under the canonical algebra map $F \to E$ is contained in the field adjunction $F(S)$, where $S$ is a subset of $E$.

IntermediateField.adjoin.range_algebraMap_subset theorem

: Set.range (algebraMap F E) ⊆ adjoin F S

Full source

theorem adjoin.range_algebraMap_subset : Set.rangeSet.range (algebraMap F E) ⊆ adjoin F S := by
  intro x hx
  obtain ⟨f, hf⟩ := hx
  rw [← hf]
  exact adjoin.algebraMap_mem F S f

Inclusion of Canonical Map Range in Field Adjunction

Informal description

For a field extension $E$ of $F$ and any subset $S \subseteq E$, the range of the canonical algebra homomorphism $\text{algebraMap}_{F \to E}$ is contained in the field adjunction $F(S)$.

IntermediateField.adjoin.fieldCoe instance

: CoeTC F (adjoin F S)

Full source

instance adjoin.fieldCoe : CoeTC F (adjoin F S) where
  coe x := ⟨algebraMap F E x, adjoin.algebraMap_mem F S x⟩

Canonical Embedding of Base Field into Adjoined Field

Informal description

For any field extension $E$ of $F$ and subset $S \subseteq E$, there is a canonical embedding of $F$ into the intermediate field $F(S)$ obtained by adjoining $S$ to $F$.

IntermediateField.subset_adjoin theorem

: S ⊆ adjoin F S

Full source

theorem subset_adjoin : S ⊆ adjoin F S := fun _ hx => Subfield.subset_closure (Or.inr hx)

Subset Adjoined to Field Contains Original Set

Informal description

For any subset $S$ of a field extension $E$ over $F$, the set $S$ is contained in the intermediate field $F(S)$ obtained by adjoining $S$ to $F$.

IntermediateField.adjoin.setCoe instance

: CoeTC S (adjoin F S)

Full source

instance adjoin.setCoe : CoeTC S (adjoin F S) where coe x := ⟨x, subset_adjoin F S (Subtype.mem x)⟩

Canonical Embedding of a Set into its Adjoined Field

Informal description

For any field extension $E$ of $F$ and subset $S \subseteq E$, there is a canonical embedding of $S$ into the intermediate field $F(S)$ obtained by adjoining $S$ to $F$.

IntermediateField.adjoin.mono theorem

(T : Set E) (h : S ⊆ T) : adjoin F S ≤ adjoin F T

Full source

@[mono]
theorem adjoin.mono (T : Set E) (h : S ⊆ T) : adjoin F S ≤ adjoin F T :=
  GaloisConnection.monotone_l gc h

Monotonicity of Field Adjoin Operation: $S \subseteq T \Rightarrow F(S) \leq F(T)$

Informal description

For any subsets $S$ and $T$ of a field extension $E$ over $F$, if $S \subseteq T$, then the intermediate field obtained by adjoining $S$ to $F$ is contained in the intermediate field obtained by adjoining $T$ to $F$, i.e., $F(S) \leq F(T)$.

IntermediateField.adjoin_contains_field_as_subfield theorem

(F : Subfield E) : (F : Set E) ⊆ adjoin F S

Full source

theorem adjoin_contains_field_as_subfield (F : Subfield E) : (F : Set E) ⊆ adjoin F S := fun x hx =>
  adjoin.algebraMap_mem F S ⟨x, hx⟩

Base Field is Contained in its Adjoin with Any Subset

Informal description

For any subfield $F$ of a field extension $E$, the subset $F$ (viewed as a subset of $E$) is contained in the field adjunction $F(S)$ for any subset $S \subseteq E$.

IntermediateField.subset_adjoin_of_subset_left theorem

{F : Subfield E} {T : Set E} (HT : T ⊆ F) : T ⊆ adjoin F S

Full source

theorem subset_adjoin_of_subset_left {F : Subfield E} {T : Set E} (HT : T ⊆ F) : T ⊆ adjoin F S :=
  fun x hx => (adjoin F S).algebraMap_mem ⟨x, HT hx⟩

Inclusion of Subset in Field Adjoin when Contained in Base Field

Informal description

For any subset $T$ of a field extension $E$ over $F$, if $T$ is contained in the subfield $F$ (viewed as a subset of $E$), then $T$ is also contained in the field adjunction $F(S)$ for any subset $S \subseteq E$.

IntermediateField.subset_adjoin_of_subset_right theorem

{T : Set E} (H : T ⊆ S) : T ⊆ adjoin F S

Full source

theorem subset_adjoin_of_subset_right {T : Set E} (H : T ⊆ S) : T ⊆ adjoin F S := fun _ hx =>
  subset_adjoin F S (H hx)

Inclusion of Subset in Field Adjoin when Contained in Larger Subset

Informal description

For any subset $T$ of a field extension $E$ over $F$, if $T$ is contained in a subset $S \subseteq E$, then $T$ is also contained in the field adjunction $F(S)$.

IntermediateField.adjoin_empty theorem

(F E : Type*) [Field F] [Field E] [Algebra F E] : adjoin F (∅ : Set E) = ⊥

Full source

@[simp]
theorem adjoin_empty (F E : Type*) [Field F] [Field E] [Algebra F E] : adjoin F (∅ : Set E) = ⊥ :=
  eq_bot_iff.mpr (adjoin_le_iff.mpr (Set.empty_subset _))

Adjoining Empty Set Yields Base Field: $F(\emptyset) = F$

Informal description

Let $F$ and $E$ be fields with $F$ a subfield of $E$ via an algebra structure. Then the field obtained by adjoining the empty set to $F$ is equal to the bottom intermediate field (i.e., $F$ itself). In symbols: $$F(\emptyset) = F$$

IntermediateField.adjoin_univ theorem

(F E : Type*) [Field F] [Field E] [Algebra F E] : adjoin F (Set.univ : Set E) = ⊤

Full source

@[simp]
theorem adjoin_univ (F E : Type*) [Field F] [Field E] [Algebra F E] :
    adjoin F (Set.univ : Set E) = ⊤ :=
  eq_top_iff.mpr <| subset_adjoin _ _

Adjoining Universal Set Yields Entire Field Extension

Informal description

For any field extension $E$ of $F$, the adjunction of the universal set $\text{univ} \subseteq E$ to $F$ equals the top intermediate field $\top$ (which is $E$ itself).

IntermediateField.adjoin_le_subfield theorem

{K : Subfield E} (HF : Set.range (algebraMap F E) ⊆ K) (HS : S ⊆ K) : (adjoin F S).toSubfield ≤ K

Full source

/-- If `K` is a field with `F ⊆ K` and `S ⊆ K` then `adjoin F S ≤ K`. -/
theorem adjoin_le_subfield {K : Subfield E} (HF : Set.rangeSet.range (algebraMap F E) ⊆ K) (HS : S ⊆ K) :
    (adjoin F S).toSubfield ≤ K := by
  apply Subfield.closure_le.mpr
  rw [Set.union_subset_iff]
  exact ⟨HF, HS⟩

Inclusion of Adjoined Field in Containing Subfield

Informal description

Let $F \subseteq E$ be a field extension, and let $K$ be a subfield of $E$ containing both the image of the canonical embedding $F \hookrightarrow E$ and a subset $S \subseteq E$. Then the field $F(S)$ obtained by adjoining $S$ to $F$ is contained in $K$ as a subfield.

IntermediateField.adjoin_subset_adjoin_iff theorem

 {F' : Type*} [Field F'] [Algebra F' E] {S S' : Set E} :
  (adjoin F S : Set E) ⊆ adjoin F' S' ↔ Set.range (algebraMap F E) ⊆ adjoin F' S' ∧ S ⊆ adjoin F' S'

Full source

theorem adjoin_subset_adjoin_iff {F' : Type*} [Field F'] [Algebra F' E] {S S' : Set E} :
    (adjoin F S : Set E) ⊆ adjoin F' S'(adjoin F S : Set E) ⊆ adjoin F' S' ↔
      Set.range (algebraMap F E) ⊆ adjoin F' S' ∧ S ⊆ adjoin F' S' :=
  ⟨fun h => ⟨(adjoin.range_algebraMap_subset _ _).trans h,
    (subset_adjoin _ _).trans h⟩, fun ⟨hF, hS⟩ =>
      (Subfield.closure_le (t := (adjoin F' S').toSubfield)).mpr (Set.union_subset hF hS)⟩

Criterion for Field Adjunction Inclusion: $F(S) \subseteq F'(S')$

Informal description

Let $F$ and $F'$ be fields with $E$ as a common extension field, and let $S, S' \subseteq E$ be subsets. Then the adjunction $F(S)$ is contained in $F'(S')$ if and only if both: 1. The range of the canonical algebra homomorphism $F \to E$ is contained in $F'(S')$, and 2. The set $S$ is contained in $F'(S')$.

IntermediateField.adjoin_adjoin_left theorem

(T : Set E) : (adjoin (adjoin F S) T).restrictScalars _ = adjoin F (S ∪ T)

Full source

/-- Adjoining S and then T is the same as adjoining `S ∪ T`. -/
theorem adjoin_adjoin_left (T : Set E) :
    (adjoin (adjoin F S) T).restrictScalars _ = adjoin F (S ∪ T) := by
  rw [SetLike.ext'_iff]
  change (adjoin (adjoin F S) T : Set E) = _
  apply subset_antisymm <;> rw [adjoin_subset_adjoin_iff] <;> constructor
  · rintro _ ⟨⟨x, hx⟩, rfl⟩; exact adjoin.mono _ _ _ Set.subset_union_left hx
  · exact subset_adjoin_of_subset_right _ _ Set.subset_union_right
  · exact Set.range_subset_iff.mpr fun f ↦ Subfield.subset_closure (.inl ⟨f, rfl⟩)
  · exact Set.union_subset
      (fun x hx ↦ Subfield.subset_closure <| .inl ⟨⟨x, Subfield.subset_closure (.inr hx)⟩, rfl⟩)
      (fun x hx ↦ Subfield.subset_closure <| .inr hx)

Adjoin Union Property: $F(S)(T) = F(S \cup T)$

Informal description

Let $F \subseteq E$ be a field extension and $S, T \subseteq E$ be subsets. Then the field obtained by first adjoining $S$ to $F$ and then adjoining $T$ to the resulting field $F(S)$ is equal to the field obtained by adjoining the union $S \cup T$ directly to $F$. In symbols: $F(S)(T) = F(S \cup T)$.

IntermediateField.adjoin_insert_adjoin theorem

(x : E) : adjoin F (insert x (adjoin F S : Set E)) = adjoin F (insert x S)

Full source

@[simp]
theorem adjoin_insert_adjoin (x : E) :
    adjoin F (insert x (adjoin F S : Set E)) = adjoin F (insert x S) :=
  le_antisymm
    (adjoin_le_iff.mpr
      (Set.insert_subset_iff.mpr
        ⟨subset_adjoin _ _ (Set.mem_insert _ _),
          adjoin_le_iff.mpr (subset_adjoin_of_subset_right _ _ (Set.subset_insert _ _))⟩))
    (adjoin.mono _ _ _ (Set.insert_subset_insert (subset_adjoin _ _)))

Adjoin Insertion Property: $F(x, F(S)) = F(x, S)$

Informal description

Let $F$ be a field, $E$ a field extension of $F$, and $S \subseteq E$ a subset. For any element $x \in E$, the intermediate field obtained by adjoining $x$ to $F(S)$ equals the intermediate field obtained by adjoining $x$ and $S$ to $F$ simultaneously. In symbols: $$F(x, F(S)) = F(x, S)$$

IntermediateField.adjoin_adjoin_comm theorem

(T : Set E) : (adjoin (adjoin F S) T).restrictScalars F = (adjoin (adjoin F T) S).restrictScalars F

Full source

/-- `F[S][T] = F[T][S]` -/
theorem adjoin_adjoin_comm (T : Set E) :
    (adjoin (adjoin F S) T).restrictScalars F = (adjoin (adjoin F T) S).restrictScalars F := by
  rw [adjoin_adjoin_left, adjoin_adjoin_left, Set.union_comm]

Commutativity of Field Adjoin Operations: $F(S)(T) = F(T)(S)$

Informal description

Let $F \subseteq E$ be a field extension and $S, T \subseteq E$ be subsets. Then the field obtained by first adjoining $S$ to $F$ and then adjoining $T$ to the resulting field $F(S)$ is equal to the field obtained by first adjoining $T$ to $F$ and then adjoining $S$ to the resulting field $F(T)$. In symbols: $F(S)(T) = F(T)(S)$.

IntermediateField.adjoin_map theorem

{E' : Type*} [Field E'] [Algebra F E'] (f : E →ₐ[F] E') : (adjoin F S).map f = adjoin F (f '' S)

Full source

theorem adjoin_map {E' : Type*} [Field E'] [Algebra F E'] (f : E →ₐ[F] E') :
    (adjoin F S).map f = adjoin F (f '' S) :=
  le_antisymm
    (map_le_iff_le_comap.mpr <| adjoin_le_iff.mpr fun x hx ↦ subset_adjoin _ _ ⟨x, hx, rfl⟩)
    (adjoin_le_iff.mpr <| Set.monotone_image <| subset_adjoin _ _)

Image of Field Adjoin under Algebra Homomorphism Equals Adjoin of Image

Informal description

Let $F$ be a field, $E$ and $E'$ field extensions of $F$, and $S \subseteq E$ a subset. For any $F$-algebra homomorphism $f : E \to E'$, the image of the adjunction $F(S)$ under $f$ equals the adjunction $F(f(S))$, where $f(S)$ denotes the image of $S$ under $f$. In symbols: $$f(F(S)) = F(f(S))$$

IntermediateField.lift_adjoin theorem

(K : IntermediateField F E) (S : Set K) : lift (adjoin F S) = adjoin F (Subtype.val '' S)

Full source

@[simp]
theorem lift_adjoin (K : IntermediateField F E) (S : Set K) :
    lift (adjoin F S) = adjoin F (Subtype.valSubtype.val '' S) :=
  adjoin_map _ _ _

Lift of Field Adjoin Equals Adjoin of Image Under Inclusion

Informal description

Let $F \subseteq K \subseteq E$ be a tower of field extensions, and let $S$ be a subset of $K$. Then the lift of the adjunction $F(S)$ (formed within $K$) to $E$ is equal to the adjunction $F(\iota(S))$ in $E$, where $\iota: K \hookrightarrow E$ is the inclusion map. In symbols: $$\text{lift}(F(S)) = F(\iota(S))$$

IntermediateField.lift_adjoin_simple theorem

(K : IntermediateField F E) (α : K) : lift (adjoin F { α }) = adjoin F { α.1 }

Full source

theorem lift_adjoin_simple (K : IntermediateField F E) (α : K) :
    lift (adjoin F {α}) = adjoin F {α.1} := by
  simp only [lift_adjoin, Set.image_singleton]

Lift of Simple Field Adjoin Equals Adjoin of Image Element

Informal description

Let $F \subseteq K \subseteq E$ be a tower of field extensions, and let $\alpha \in K$. Then the lift of the adjunction $F(\alpha)$ (formed within $K$) to $E$ is equal to the adjunction $F(\iota(\alpha))$ in $E$, where $\iota: K \hookrightarrow E$ is the inclusion map. In symbols: $$\text{lift}(F(\alpha)) = F(\iota(\alpha))$$

IntermediateField.lift_bot theorem

(K : IntermediateField F E) : lift (F := K) ⊥ = ⊥

Full source

@[simp]
theorem lift_bot (K : IntermediateField F E) :
    lift (F := K) ⊥ = ⊥ := map_bot _

Lift of Trivial Intermediate Field is Trivial

Informal description

For any intermediate field $K$ between fields $F$ and $E$, the lift of the trivial intermediate field $\bot$ (with respect to $K$) is equal to the trivial intermediate field $\bot$ in $K$.

IntermediateField.lift_top theorem

(K : IntermediateField F E) : lift (F := K) ⊤ = K

Full source

@[simp]
theorem lift_top (K : IntermediateField F E) :
    lift (F := K) ⊤ = K := by rw [lift, ← AlgHom.fieldRange_eq_map, fieldRange_val]

Lift of Top Intermediate Field Equals Itself

Informal description

For any intermediate field $K$ between fields $F$ and $E$, the lift of the top intermediate field (i.e., $E$) under the inclusion map from $K$ to $E$ is equal to $K$ itself. In other words, $K$ is the image of $E$ under the canonical inclusion map from $K$ to $E$.

IntermediateField.adjoin_self theorem

(K : IntermediateField F E) : adjoin F K = K

Full source

@[simp]
theorem adjoin_self (K : IntermediateField F E) :
    adjoin F K = K := le_antisymm (adjoin_le_iff.2 fun _ ↦ id) (subset_adjoin F _)

Self-Adjunction of Intermediate Fields: $F(K) = K$

Informal description

For any intermediate field $K$ between fields $F$ and $E$, the adjunction of $K$ to $F$ is equal to $K$ itself, i.e., $F(K) = K$.

IntermediateField.restrictScalars_adjoin theorem

(K : IntermediateField F E) (S : Set E) : restrictScalars F (adjoin K S) = adjoin F (K ∪ S)

Full source

theorem restrictScalars_adjoin (K : IntermediateField F E) (S : Set E) :
    restrictScalars F (adjoin K S) = adjoin F (K ∪ S) := by
  rw [← adjoin_self _ K, adjoin_adjoin_left, adjoin_self _ K]

Restriction of Scalars for Field Adjoin: $F \cdot K(S) = F(K \cup S)$

Informal description

Let $F \subseteq E$ be a field extension, $K$ an intermediate field between $F$ and $E$, and $S \subseteq E$ a subset. Then the restriction of scalars of the field $K(S)$ to $F$ is equal to the field $F(K \cup S)$. In symbols: $F \cdot K(S) = F(K \cup S)$, where $F \cdot K(S)$ denotes the restriction of $K(S)$ to $F$.

IntermediateField.extendScalars_adjoin theorem

{K : IntermediateField F E} {S : Set E} (h : K ≤ adjoin F S) : extendScalars h = adjoin K S

Full source

theorem extendScalars_adjoin {K : IntermediateField F E} {S : Set E} (h : K ≤ adjoin F S) :
    extendScalars h = adjoin K S := restrictScalars_injective F <| by
  rw [extendScalars_restrictScalars, restrictScalars_adjoin]
  exact le_antisymm (adjoin.mono F S _ Set.subset_union_right) <| adjoin_le_iff.2 <|
    Set.union_subset h (subset_adjoin F S)

Extension of Scalars for Field Adjoin: $\text{extendScalars}(h) = K(S)$ when $K \leq F(S)$

Informal description

Let $F \subseteq E$ be a field extension, $K$ an intermediate field between $F$ and $E$, and $S \subseteq E$ a subset. If $K$ is contained in the field adjunction $F(S)$, then the extension of scalars of $K$ with respect to this containment is equal to the field adjunction $K(S)$. In symbols: If $K \leq F(S)$, then $\text{extendScalars}(h) = K(S)$.

IntermediateField.adjoin_union theorem

{S T : Set E} : adjoin F (S ∪ T) = adjoin F S ⊔ adjoin F T

Full source

theorem adjoin_union {S T : Set E} : adjoin F (S ∪ T) = adjoinadjoin F S ⊔ adjoin F T :=
  gc.l_sup

Field Adjoin of Union Equals Supremum of Adjoins

Informal description

Let $F$ be a field and $E$ a field extension of $F$. For any subsets $S, T \subseteq E$, the field adjunction $F(S \cup T)$ is equal to the supremum of the field adjunctions $F(S)$ and $F(T)$, i.e., $$ F(S \cup T) = F(S) \sqcup F(T). $$

IntermediateField.restrictScalars_adjoin_eq_sup theorem

(K : IntermediateField F E) (S : Set E) : restrictScalars F (adjoin K S) = K ⊔ adjoin F S

Full source

theorem restrictScalars_adjoin_eq_sup (K : IntermediateField F E) (S : Set E) :
    restrictScalars F (adjoin K S) = K ⊔ adjoin F S := by
  rw [restrictScalars_adjoin, adjoin_union, adjoin_self]

Restriction of Scalars for Field Adjoin Equals Supremum: $F \cdot K(S) = K \sqcup F(S)$

Informal description

Let $F \subseteq E$ be a field extension, $K$ an intermediate field between $F$ and $E$, and $S \subseteq E$ a subset. Then the restriction of scalars of the field $K(S)$ to $F$ is equal to the supremum of $K$ and $F(S)$ in the lattice of intermediate fields between $F$ and $E$. In symbols: $F \cdot K(S) = K \sqcup F(S)$, where $F \cdot K(S)$ denotes the restriction of $K(S)$ to $F$.

IntermediateField.adjoin_iUnion theorem

{ι} (f : ι → Set E) : adjoin F (⋃ i, f i) = ⨆ i, adjoin F (f i)

Full source

theorem adjoin_iUnion {ι} (f : ι → Set E) : adjoin F (⋃ i, f i) = ⨆ i, adjoin F (f i) :=
  gc.l_iSup

Adjoin Union Equals Supremum of Adjoins

Informal description

Let $F$ be a field and $E$ a field extension of $F$. For any family of subsets $(f_i)_{i \in \iota}$ of $E$, the field obtained by adjoining the union $\bigcup_{i} f_i$ to $F$ is equal to the supremum (in the lattice of intermediate fields between $F$ and $E$) of the fields obtained by adjoining each $f_i$ to $F$. In symbols: $$ F\left(\bigcup_{i} f_i\right) = \bigsqcup_{i} F(f_i) $$

IntermediateField.restrictScalars_adjoin_of_algEquiv theorem

 {L L' : Type*} [Field L] [Field L'] [Algebra F L] [Algebra L E] [Algebra F L'] [Algebra L' E] [IsScalarTower F L E]
  [IsScalarTower F L' E] (i : L ≃ₐ[F] L') (hi : algebraMap L E = (algebraMap L' E) ∘ i) (S : Set E) :
  (adjoin L S).restrictScalars F = (adjoin L' S).restrictScalars F

Full source

/-- If `E / L / F` and `E / L' / F` are two field extension towers, `L ≃ₐ[F] L'` is an isomorphism
compatible with `E / L` and `E / L'`, then for any subset `S` of `E`, `L(S)` and `L'(S)` are
equal as intermediate fields of `E / F`. -/
theorem restrictScalars_adjoin_of_algEquiv
    {L L' : Type*} [Field L] [Field L']
    [Algebra F L] [Algebra L E] [Algebra F L'] [Algebra L' E]
    [IsScalarTower F L E] [IsScalarTower F L' E] (i : L ≃ₐ[F] L')
    (hi : algebraMap L E = (algebraMap L' E) ∘ i) (S : Set E) :
    (adjoin L S).restrictScalars F = (adjoin L' S).restrictScalars F := by
  apply_fun toSubfield using (fun K K' h ↦ by
    ext x; change x ∈ K.toSubfield ↔ x ∈ K'.toSubfield; rw [h])
  change Subfield.closure _ = Subfield.closure _
  congr
  ext x
  exact ⟨fun ⟨y, h⟩ ↦ ⟨i y, by rw [← h, hi]; rfl⟩,
    fun ⟨y, h⟩ ↦ ⟨i.symm y, by rw [← h, hi, Function.comp_apply, AlgEquiv.apply_symm_apply]⟩⟩

Equality of Adjoined Fields under Isomorphic Intermediate Extensions

Informal description

Let $E$ be a field extension of $F$, and let $L$ and $L'$ be intermediate fields between $F$ and $E$ with corresponding field extensions $E / L / F$ and $E / L' / F$. Suppose there exists an $F$-algebra isomorphism $i: L \simeq L'$ such that the algebra maps satisfy $\text{algebraMap}_{L \to E} = \text{algebraMap}_{L' \to E} \circ i$. Then for any subset $S \subseteq E$, the intermediate fields $L(S)$ and $L'(S)$, when restricted to $F$, are equal as subfields of $E$.

IntermediateField.adjoin_induction theorem

 {s : Set E} {p : ∀ x ∈ adjoin F s, Prop} (mem : ∀ x hx, p x (subset_adjoin _ _ hx))
  (algebraMap : ∀ x, p (algebraMap F E x) (algebraMap_mem _ _))
  (add : ∀ x y hx hy, p x hx → p y hy → p (x + y) (add_mem hx hy)) (inv : ∀ x hx, p x hx → p x⁻¹ (inv_mem hx))
  (mul : ∀ x y hx hy, p x hx → p y hy → p (x * y) (mul_mem hx hy)) {x} (h : x ∈ adjoin F s) : p x h

Full source

@[elab_as_elim]
theorem adjoin_induction {s : Set E} {p : ∀ x ∈ adjoin F s, Prop}
    (mem : ∀ x hx, p x (subset_adjoin _ _ hx))
    (algebraMap : ∀ x, p (algebraMap F E x) (algebraMap_mem _ _))
    (add : ∀ x y hx hy, p x hx → p y hy → p (x + y) (add_mem hx hy))
    (inv : ∀ x hx, p x hx → p x⁻¹ (inv_mem hx))
    (mul : ∀ x y hx hy, p x hx → p y hy → p (x * y) (mul_mem hx hy))
    {x} (h : x ∈ adjoin F s) : p x h :=
  Subfield.closure_induction
    (fun x hx ↦ Or.casesOn hx (fun ⟨x, hx⟩ ↦ hx ▸ algebraMap x) (mem x))
    (by simp_rw [← (_root_.algebraMap F E).map_one]; exact algebraMap 1) add
    (fun x _ h ↦ by
      simp_rw [← neg_one_smul F x, Algebra.smul_def]; exact mul _ _ _ _ (algebraMap _) h) inv mul h

Induction Principle for Adjoined Field Elements

Informal description

Let $E$ be a field extension of $F$, and let $s \subseteq E$ be a subset. For any predicate $p$ defined on elements of the intermediate field $F(s)$, if: 1. $p$ holds for all elements $x \in s$, 2. $p$ holds for the image of any $x \in F$ under the algebra map $F \to E$, 3. $p$ is preserved under addition (i.e., if $p(x)$ and $p(y)$ hold, then $p(x+y)$ holds), 4. $p$ is preserved under inversion (i.e., if $p(x)$ holds, then $p(x^{-1})$ holds), 5. $p$ is preserved under multiplication (i.e., if $p(x)$ and $p(y)$ hold, then $p(xy)$ holds), then $p(x)$ holds for every $x \in F(s)$.

IntermediateField.adjoin_algHom_ext theorem

 {s : Set E} ⦃φ₁ φ₂ : adjoin F s →ₐ[F] K⦄ (h : ∀ x hx, φ₁ ⟨x, subset_adjoin _ _ hx⟩ = φ₂ ⟨x, subset_adjoin _ _ hx⟩) :
  φ₁ = φ₂

Full source

theorem adjoin_algHom_ext {s : Set E} ⦃φ₁ φ₂ : adjoinadjoin F s →ₐ[F] K⦄
    (h : ∀ x hx, φ₁ ⟨x, subset_adjoin _ _ hx⟩ = φ₂ ⟨x, subset_adjoin _ _ hx⟩) :
    φ₁ = φ₂ :=
  AlgHom.ext fun ⟨x, hx⟩ ↦ adjoin_induction _ h (fun _ ↦ φ₂.commutes _ ▸ φ₁.commutes _)
    (fun _ _ _ _ h₁ h₂ ↦ by convert congr_arg₂ (· + ·) h₁ h₂ <;> rw [← map_add] <;> rfl)
    (fun _ _ ↦ eq_on_inv₀ _ _)
    (fun _ _ _ _ h₁ h₂ ↦ by convert congr_arg₂ (· * ·) h₁ h₂ <;> rw [← map_mul] <;> rfl)
    hx

Uniqueness of Algebra Homomorphisms from Adjoined Field Extensions

Informal description

Let $E$ be a field extension of $F$, and let $s \subseteq E$ be a subset. For any two $F$-algebra homomorphisms $\varphi_1, \varphi_2 \colon F(s) \to K$ from the intermediate field $F(s)$ to another field $K$, if $\varphi_1(x) = \varphi_2(x)$ for all $x \in s$, then $\varphi_1 = \varphi_2$ on the entire field $F(s)$.

IntermediateField.algHom_ext_of_eq_adjoin theorem

 {S : IntermediateField F E} {s : Set E} (hS : S = adjoin F s) ⦃φ₁ φ₂ : S →ₐ[F] K⦄
  (h : ∀ x hx, φ₁ ⟨x, hS.ge (subset_adjoin _ _ hx)⟩ = φ₂ ⟨x, hS.ge (subset_adjoin _ _ hx)⟩) : φ₁ = φ₂

Full source

theorem algHom_ext_of_eq_adjoin {S : IntermediateField F E} {s : Set E} (hS : S = adjoin F s)
    ⦃φ₁ φ₂ : S →ₐ[F] K⦄
    (h : ∀ x hx, φ₁ ⟨x, hS.ge (subset_adjoin _ _ hx)⟩ = φ₂ ⟨x, hS.ge (subset_adjoin _ _ hx)⟩) :
    φ₁ = φ₂ := by
  subst hS; exact adjoin_algHom_ext F h

Uniqueness of Algebra Homomorphisms on Adjoined Field Extensions

Informal description

Let $S$ be an intermediate field between fields $F$ and $E$, and let $s \subseteq E$ be a subset such that $S = F(s)$. For any two $F$-algebra homomorphisms $\varphi_1, \varphi_2 \colon S \to K$, if $\varphi_1(x) = \varphi_2(x)$ for all $x \in s$, then $\varphi_1 = \varphi_2$ on the entire field $S$.

IntermediateField.term_⟮_,,⟯ definition

: Lean.TrailingParserDescr✝

Full source

macromacro:max K:term "⟮" xs:term,* "⟯" : term => do ``(adjoin $K $(← mkInsertTerm xs.getElems))

Field adjunction notation

Informal description

The notation `F⟮x₁, x₂, ..., xₙ⟯` represents the intermediate field generated by adjoining elements `x₁, x₂, ..., xₙ` to the field `F`, where these elements belong to some field extension `E` of `F`. This is the smallest intermediate field between `F` and `E` containing all the specified elements.

IntermediateField.delabAdjoinNotation definition

: Delab

Full source

@[app_delab IntermediateField.adjoin]
partial def delabAdjoinNotation : Delab := whenPPOption getPPNotation do
  let e ← getExpr
  guardguard <| e.isAppOfArity ``adjoin 6
  let F ← withNaryArg 0 delab
  let xs ← withNaryArg 5 delabInsertArray
  `($F⟮$(xs.toArray),*⟯)
where
  delabInsertArray : DelabM (List Term) := do
    let e ← getExpr
    if e.isAppOfArity ``EmptyCollection.emptyCollection 2 then
      return []
    else if e.isAppOfArity ``singleton 4 then
      let x ← withNaryArg 3 delab
      return [x]
    else if e.isAppOfArity ``insert 5 then
      let x ← withNaryArg 3 delab
      let xs ← withNaryArg 4 delabInsertArray
      return x :: xs
    else failure

Field adjunction notation

Informal description

The notation `F⟮x₁, x₂, ..., xₙ⟯` represents the intermediate field generated by adjoining elements `x₁, x₂, \dots, xₙ$ to the field $F$, where these elements belong to some field extension $E$ of $F$. This is the smallest intermediate field between $F$ and $E$ containing all the specified elements.

IntermediateField.mem_adjoin_simple_self theorem

: α ∈ F⟮α⟯

Full source

theorem mem_adjoin_simple_self : α ∈ F⟮α⟯ :=
  subset_adjoin F {α} (Set.mem_singleton α)

Element Belongs to Its Own Adjoined Field: $\alpha \in F(\alpha)$

Informal description

For any field extension $E$ of $F$ and any element $\alpha \in E$, the element $\alpha$ belongs to the intermediate field $F(\alpha)$ obtained by adjoining $\alpha$ to $F$.

IntermediateField.AdjoinSimple.gen definition

: F⟮α⟯

Full source

/-- generator of `F⟮α⟯` -/
def AdjoinSimple.gen : F⟮α⟯ :=
  ⟨α, mem_adjoin_simple_self F α⟩

Generator of the Adjoined Field $ F(\alpha) $

Informal description

The generator of the intermediate field $ F(\alpha) $, which is the element $\alpha$ adjoined to the field $ F $. This element is represented as a term of type $ F(\alpha) $ and satisfies the property that its image under the canonical embedding into $ E $ is $\alpha$ itself.

IntermediateField.AdjoinSimple.coe_gen theorem

: (AdjoinSimple.gen F α : E) = α

Full source

@[simp]
theorem AdjoinSimple.coe_gen : (AdjoinSimple.gen F α : E) = α :=
  rfl

Generator Inclusion in Adjoined Field: $\alpha \in F(\alpha) \hookrightarrow E$ maps to $\alpha$

Informal description

The generator $\alpha$ of the field extension $F(\alpha)$, when viewed as an element of $E$, is equal to $\alpha$ itself. That is, the inclusion map $F(\alpha) \hookrightarrow E$ sends the generator $\alpha$ to $\alpha \in E$.

IntermediateField.AdjoinSimple.algebraMap_gen theorem

: algebraMap F⟮α⟯ E (AdjoinSimple.gen F α) = α

Full source

theorem AdjoinSimple.algebraMap_gen : algebraMap F⟮α⟯ E (AdjoinSimple.gen F α) = α :=
  rfl

Algebra Map Evaluates Generator to Itself in Field Extension

Informal description

The algebra map from the field extension $F(\alpha)$ to $E$ evaluated at the generator $\alpha$ of $F(\alpha)$ equals $\alpha$, i.e., $\text{algebraMap}_{F(\alpha) \to E}(\alpha) = \alpha$.

IntermediateField.adjoin_simple_adjoin_simple theorem

(β : E) : F⟮α⟯⟮β⟯.restrictScalars F = F⟮α, β⟯

Full source

theorem adjoin_simple_adjoin_simple (β : E) : F⟮α⟯F⟮α⟯⟮β⟯.restrictScalars F = F⟮α, β⟯ :=
  adjoin_adjoin_left _ _ _

Iterated Adjoin Equals Simultaneous Adjoin: $F(\alpha)(\beta) = F(\alpha, \beta)$

Informal description

Let $F \subseteq E$ be a field extension and $\alpha, \beta \in E$. Then the field obtained by first adjoining $\alpha$ to $F$ and then adjoining $\beta$ to the resulting field $F(\alpha)$ is equal to the field obtained by adjoining both $\alpha$ and $\beta$ simultaneously to $F$. In symbols: $F(\alpha)(\beta) = F(\alpha, \beta)$.

IntermediateField.adjoin_simple_comm theorem

(β : E) : F⟮α⟯⟮β⟯.restrictScalars F = F⟮β⟯⟮α⟯.restrictScalars F

Full source

theorem adjoin_simple_comm (β : E) : F⟮α⟯F⟮α⟯⟮β⟯.restrictScalars F = F⟮β⟯F⟮β⟯⟮α⟯.restrictScalars F :=
  adjoin_adjoin_comm _ _ _

Commutativity of Simple Field Adjoin Operations: $F(\alpha)(\beta) = F(\beta)(\alpha)$

Informal description

Let $F \subseteq E$ be a field extension and $\alpha, \beta \in E$. Then the field obtained by first adjoining $\alpha$ to $F$ and then adjoining $\beta$ to $F(\alpha)$ is equal to the field obtained by first adjoining $\beta$ to $F$ and then adjoining $\alpha$ to $F(\beta)$. In symbols: $F(\alpha)(\beta) = F(\beta)(\alpha)$.

IntermediateField.adjoin_simple_le_iff theorem

{K : IntermediateField F E} : F⟮α⟯ ≤ K ↔ α ∈ K

Full source

theorem adjoin_simple_le_iff {K : IntermediateField F E} : F⟮α⟯F⟮α⟯ ≤ K ↔ α ∈ K := by simp

Characterization of Field Adjoin Inclusion: $F(\alpha) \subseteq K \iff \alpha \in K$

Informal description

For any intermediate field $K$ between $F$ and $E$, the field $F(\alpha)$ is contained in $K$ if and only if $\alpha$ belongs to $K$.

IntermediateField.biSup_adjoin_simple theorem

: ⨆ x ∈ S, F⟮x⟯ = adjoin F S

Full source

theorem biSup_adjoin_simple : ⨆ x ∈ S, F⟮x⟯ = adjoin F S := by
  rw [← iSup_subtype'', ← gc.l_iSup, iSup_subtype'']; congr; exact S.biUnion_of_singleton

Supremum of Adjoined Simple Fields Equals Adjoined Set

Informal description

For any subset $S$ of a field extension $E$ over $F$, the supremum of the family of fields $F(x)$ adjoined by each element $x \in S$ is equal to the field $F(S)$ obtained by adjoining the entire set $S$ to $F$. In other words: \[ \bigsqcup_{x \in S} F(x) = F(S). \]

IntermediateField.adjoin_eq_bot_iff theorem

: adjoin F S = ⊥ ↔ S ⊆ (⊥ : IntermediateField F E)

Full source

@[simp]
theorem adjoin_eq_bot_iff : adjoinadjoin F S = ⊥ ↔ S ⊆ (⊥ : IntermediateField F E) := by
  rw [eq_bot_iff, adjoin_le_iff]

Characterization of Trivial Field Adjunction: $F(S) = F \leftrightarrow S \subseteq F$

Informal description

Let $F$ be a field and $E$ a field extension of $F$. For any subset $S \subseteq E$, the adjunction field $F(S)$ equals the bottom intermediate field $\bot$ (which is $F$ itself) if and only if $S$ is contained in $\bot$. In other words: $$F(S) = F \leftrightarrow S \subseteq F$$

IntermediateField.adjoin_simple_eq_bot_iff theorem

: F⟮α⟯ = ⊥ ↔ α ∈ (⊥ : IntermediateField F E)

Full source

theorem adjoin_simple_eq_bot_iff : F⟮α⟯F⟮α⟯ = ⊥ ↔ α ∈ (⊥ : IntermediateField F E) := by
  simp

Triviality Criterion for Simple Field Adjoint: $F(\alpha) = \bot \leftrightarrow \alpha \in \bot$

Informal description

Let $F$ be a field and $E$ a field extension of $F$. For any element $\alpha \in E$, the adjunction field $F(\alpha)$ equals the trivial intermediate field $\bot$ if and only if $\alpha$ belongs to $\bot$.

IntermediateField.adjoin_zero theorem

: F⟮(0 : E)⟯ = ⊥

Full source

@[simp]
theorem adjoin_zero : F⟮(0 : E)⟯ = ⊥ :=
  adjoin_simple_eq_bot_iff.mpr (zero_mem ⊥)

Triviality of Zero Adjoint: $F(0) = F$

Informal description

Let $F$ be a field and $E$ a field extension of $F$. The adjunction field $F(0)$ generated by the zero element $0 \in E$ is equal to the trivial intermediate field $\bot$ (which is $F$ itself).

IntermediateField.adjoin_one theorem

: F⟮(1 : E)⟯ = ⊥

Full source

@[simp]
theorem adjoin_one : F⟮(1 : E)⟯ = ⊥ :=
  adjoin_simple_eq_bot_iff.mpr (one_mem ⊥)

Triviality of Adjoining Multiplicative Identity to Field Extension

Informal description

Let $F$ be a field and $E$ a field extension of $F$. The adjunction field $F(1)$, where $1$ is the multiplicative identity in $E$, is equal to the trivial intermediate field $\bot$.

IntermediateField.adjoin_intCast theorem

(n : ℤ) : F⟮(n : E)⟯ = ⊥

Full source

@[simp]
theorem adjoin_intCast (n : ℤ) : F⟮(n : E)⟯ = ⊥ := by
  exact adjoin_simple_eq_bot_iff.mpr (intCast_mem ⊥ n)

Triviality of Integer Adjoint: $F(n) = F$ for $n \in \mathbb{Z}$

Informal description

For any integer $n \in \mathbb{Z}$ and any field extension $E$ of $F$, the adjunction field $F(n)$ generated by the image of $n$ in $E$ is equal to the trivial intermediate field $\bot$ (which is $F$ itself).

IntermediateField.adjoin_natCast theorem

(n : ℕ) : F⟮(n : E)⟯ = ⊥

Full source

@[simp]
theorem adjoin_natCast (n : ℕ) : F⟮(n : E)⟯ = ⊥ :=
  adjoin_simple_eq_bot_iff.mpr (natCast_mem ⊥ n)

Triviality of Adjoining Natural Numbers to Field Extension

Informal description

For any natural number $n$ and field extension $E$ of $F$, the adjunction field $F(n)$ (where $n$ is viewed as an element of $E$ via the canonical embedding) is equal to the trivial intermediate field $\bot$.

IntermediateField.FG definition

(S : IntermediateField F E) : Prop

Full source

/-- An intermediate field `S` is finitely generated if there exists `t : Finset E` such that
`IntermediateField.adjoin F t = S`. -/
@[stacks 09FZ "second part"]
def FG (S : IntermediateField F E) : Prop :=
  ∃ t : Finset E, adjoin F ↑t = S

Finitely generated intermediate field

Informal description

An intermediate field $ S $ between $ F $ and $ E $ is finitely generated if there exists a finite subset $ t \subseteq E $ such that the adjunction $ F(t) $ equals $ S $.

IntermediateField.fg_adjoin_finset theorem

(t : Finset E) : (adjoin F (↑t : Set E)).FG

Full source

theorem fg_adjoin_finset (t : Finset E) : (adjoin F (↑t : Set E)).FG :=
  ⟨t, rfl⟩

Finite Adjoining Yields Finitely Generated Intermediate Field

Informal description

For any finite subset $t$ of a field extension $E$ over $F$, the intermediate field $F(t)$ obtained by adjoining $t$ to $F$ is finitely generated.

IntermediateField.fg_def theorem

{S : IntermediateField F E} : S.FG ↔ ∃ t : Set E, Set.Finite t ∧ adjoin F t = S

Full source

theorem fg_def {S : IntermediateField F E} : S.FG ↔ ∃ t : Set E, Set.Finite t ∧ adjoin F t = S :=
  Iff.symm Set.exists_finite_iff_finset

Characterization of Finitely Generated Intermediate Fields

Informal description

An intermediate field $S$ between $F$ and $E$ is finitely generated if and only if there exists a finite subset $t \subseteq E$ such that the adjunction $F(t)$ equals $S$.

IntermediateField.fg_adjoin_of_finite theorem

{t : Set E} (h : Set.Finite t) : (adjoin F t).FG

Full source

theorem fg_adjoin_of_finite {t : Set E} (h : Set.Finite t) : (adjoin F t).FG :=
  fg_def.mpr ⟨t, h, rfl⟩

Finite Adjoining Yields Finitely Generated Intermediate Field

Informal description

For any finite subset $t$ of a field extension $E$ over $F$, the intermediate field $F(t)$ obtained by adjoining $t$ to $F$ is finitely generated.

IntermediateField.fg_bot theorem

: (⊥ : IntermediateField F E).FG

Full source

theorem fg_bot : (⊥ : IntermediateField F E).FG :=
  ⟨∅, by simp only [Finset.coe_empty, adjoin_empty]⟩

Base Field is Finitely Generated in Field Extension

Informal description

The bottom intermediate field $\bot$ (which is $F$ itself) in a field extension $E$ of $F$ is finitely generated.

IntermediateField.fg_sup theorem

{S T : IntermediateField F E} (hS : S.FG) (hT : T.FG) : (S ⊔ T).FG

Full source

theorem fg_sup {S T : IntermediateField F E} (hS : S.FG) (hT : T.FG) : (S ⊔ T).FG := by
  obtain ⟨s, rfl⟩ := hS; obtain ⟨t, rfl⟩ := hT
  classical rw [← adjoin_union, ← Finset.coe_union]
  exact fg_adjoin_finset _

Supremum of Finitely Generated Intermediate Fields is Finitely Generated

Informal description

Let $F \subseteq E$ be a field extension and let $S, T$ be intermediate fields between $F$ and $E$. If both $S$ and $T$ are finitely generated over $F$, then their supremum $S \sqcup T$ (the smallest intermediate field containing both $S$ and $T$) is also finitely generated over $F$.

IntermediateField.fg_iSup theorem

{ι : Sort*} [Finite ι] {S : ι → IntermediateField F E} (h : ∀ i, (S i).FG) : (⨆ i, S i).FG

Full source

theorem fg_iSup {ι : Sort*} [Finite ι] {S : ι → IntermediateField F E} (h : ∀ i, (S i).FG) :
    (⨆ i, S i).FG := by
  choose s hs using h
  simp_rw [← hs, ← adjoin_iUnion]
  exact fg_adjoin_of_finite (Set.finite_iUnion fun _ ↦ Finset.finite_toSet _)

Finite Supremum of Finitely Generated Intermediate Fields is Finitely Generated

Informal description

Let $F \subseteq E$ be a field extension and $\{S_i\}_{i \in \iota}$ be a family of intermediate fields between $F$ and $E$, where the index set $\iota$ is finite. If each intermediate field $S_i$ is finitely generated over $F$, then their supremum $\bigsqcup_{i \in \iota} S_i$ (the smallest intermediate field containing all $S_i$) is also finitely generated over $F$.

IntermediateField.induction_on_adjoin_finset theorem

 (S : Finset E) (P : IntermediateField F E → Prop) (base : P ⊥)
  (ih : ∀ (K : IntermediateField F E), ∀ x ∈ S, P K → P (K⟮x⟯.restrictScalars F)) : P (adjoin F S)

Full source

theorem induction_on_adjoin_finset (S : Finset E) (P : IntermediateField F E → Prop) (base : P ⊥)
    (ih : ∀ (K : IntermediateField F E), ∀ x ∈ S, P K → P (K⟮x⟯.restrictScalars F)) :
    P (adjoin F S) := by
  classical
  refine Finset.induction_on' S ?_ (fun _ _ ha _ _ h => ?_)
  · simp [base]
  · rw [Finset.coe_insert, Set.insert_eq, Set.union_comm, ← adjoin_adjoin_left]
    exact ih (adjoin F _) _ ha h

Induction Principle for Field Adjoining Finite Sets: $P(F(S))$ via $P(F)$ and $P(K) \Rightarrow P(K(x))$ for $x \in S$

Informal description

Let $F \subseteq E$ be a field extension and $S$ be a finite subset of $E$. For any property $P$ of intermediate fields between $F$ and $E$, if: 1. $P$ holds for the base field $F$ (i.e., $P(\bot)$), and 2. For any intermediate field $K$ and any $x \in S$, if $P(K)$ holds then $P(K(x))$ holds (where $K(x)$ denotes adjoining $x$ to $K$), then $P$ holds for the field $F(S)$ obtained by adjoining all elements of $S$ to $F$.

IntermediateField.induction_on_adjoin_fg theorem

 (P : IntermediateField F E → Prop) (base : P ⊥)
  (ih : ∀ (K : IntermediateField F E) (x : E), P K → P (K⟮x⟯.restrictScalars F)) (K : IntermediateField F E)
  (hK : K.FG) : P K

Full source

theorem induction_on_adjoin_fg (P : IntermediateField F E → Prop) (base : P ⊥)
    (ih : ∀ (K : IntermediateField F E) (x : E), P K → P (K⟮x⟯.restrictScalars F))
    (K : IntermediateField F E) (hK : K.FG) : P K := by
  obtain ⟨S, rfl⟩ := hK
  exact induction_on_adjoin_finset S P base fun K x _ hK => ih K x hK

Induction Principle for Finitely Generated Intermediate Fields: $P(K)$ via $P(F)$ and $P(L) \Rightarrow P(L(x))$

Informal description

Let $F \subseteq E$ be a field extension and $K$ be a finitely generated intermediate field between $F$ and $E$. For any property $P$ of intermediate fields, if: 1. $P$ holds for the base field $F$ (i.e., $P(F)$), and 2. For any intermediate field $L$ and any $x \in E$, if $P(L)$ holds then $P(L(x))$ holds (where $L(x)$ denotes adjoining $x$ to $L$), then $P$ holds for $K$.

IntermediateField.map_comap_eq theorem

(f : L →ₐ[K] L') (S : IntermediateField K L') : (S.comap f).map f = S ⊓ f.fieldRange

Full source

theorem map_comap_eq (f : L →ₐ[K] L') (S : IntermediateField K L') :
    (S.comap f).map f = S ⊓ f.fieldRange :=
  SetLike.coe_injective Set.image_preimage_eq_inter_range

Image-Preimage Equality for Field Homomorphisms: $f(f^{-1}(S)) = S \cap \mathrm{range}(f)$

Informal description

Let $K$ be a field, $L$ and $L'$ be field extensions of $K$, and $f \colon L \to L'$ be a $K$-algebra homomorphism. For any intermediate field $S$ between $K$ and $L'$, we have \[ f(f^{-1}(S)) = S \cap \mathrm{range}(f), \] where $f^{-1}(S)$ denotes the preimage of $S$ under $f$, and $\mathrm{range}(f)$ is the range of $f$.

IntermediateField.map_comap_eq_self theorem

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

Full source

theorem map_comap_eq_self {f : L →ₐ[K] L'} {S : IntermediateField K L'} (h : S ≤ f.fieldRange) :
    (S.comap f).map f = S := by
  simpa only [inf_of_le_left h] using map_comap_eq f S

Image-Preimage Equality for Intermediate Fields within Range: $f(f^{-1}(S)) = S$ when $S \subseteq \mathrm{range}(f)$

Informal description

Let $K$ be a field, $L$ and $L'$ be field extensions of $K$, and $f \colon L \to L'$ be a $K$-algebra homomorphism. For any intermediate field $S$ between $K$ and $L'$ such that $S$ is contained in the range of $f$, we have \[ f(f^{-1}(S)) = S. \]

IntermediateField.map_comap_eq_self_of_surjective theorem

{f : L →ₐ[K] L'} (hf : Function.Surjective f) (S : IntermediateField K L') : (S.comap f).map f = S

Full source

theorem map_comap_eq_self_of_surjective {f : L →ₐ[K] L'} (hf : Function.Surjective f)
    (S : IntermediateField K L') : (S.comap f).map f = S :=
  SetLike.coe_injective (Set.image_preimage_eq _ hf)

Image-Preimage Equality for Surjective Field Homomorphisms: $f(f^{-1}(S)) = S$

Informal description

Let $K$ be a field, $L$ and $L'$ be field extensions of $K$, and $f \colon L \to L'$ be a surjective $K$-algebra homomorphism. For any intermediate field $S$ between $K$ and $L'$, the image under $f$ of the preimage of $S$ under $f$ equals $S$ itself, i.e., \[ f(f^{-1}(S)) = S. \]

IntermediateField.comap_map theorem

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

Full source

theorem comap_map (f : L →ₐ[K] L') (S : IntermediateField K L) : (S.map f).comap f = S :=
  SetLike.coe_injective (Set.preimage_image_eq _ f.injective)

Preimage of Image Equals Original Intermediate Field

Informal description

Let $K$ be a field, $L$ and $L'$ be field extensions of $K$, and $f \colon L \to L'$ be a $K$-algebra homomorphism. For any intermediate field $S$ between $K$ and $L$, the preimage under $f$ of the image of $S$ under $f$ equals $S$ itself, i.e., $f^{-1}(f(S)) = S$.

Subfield.extendScalars_self theorem

: extendScalars (le_refl F) = ⊥

Full source

@[simp]
theorem extendScalars_self : extendScalars (le_refl F) = ⊥ := by
  ext x
  rw [mem_extendScalars, IntermediateField.mem_bot]
  refine ⟨fun h ↦ ⟨⟨x, h⟩, rfl⟩, ?_⟩
  rintro ⟨y, rfl⟩
  exact y.2

Scalar Extension Along Reflexive Inclusion Yields Bottom Field

Informal description

For any field $F$, the extension of scalars along the reflexive inclusion $F \leq F$ is equal to the smallest intermediate field $\bot$ between $F$ and itself.

Subfield.extendScalars_top theorem

: extendScalars (le_top : F ≤ ⊤) = ⊤

Full source

@[simp]
theorem extendScalars_top : extendScalars (le_top : F ≤ ⊤) = ⊤ :=
  IntermediateField.toSubfield_injective (by simp)

Extension of Scalars Along Top Inclusion Yields Top Field

Informal description

For any field $F$, the extension of scalars along the inclusion $F \leq \top$ (where $\top$ is the top element in the lattice of field extensions) is equal to $\top$ itself, i.e., $\text{extendScalars}(F \leq \top) = \top$.

Subfield.extendScalars_sup theorem

: extendScalars h ⊔ extendScalars h' = extendScalars (le_sup_of_le_left h : F ≤ E ⊔ E')

Full source

theorem extendScalars_sup :
    extendScalarsextendScalars h ⊔ extendScalars h' = extendScalars (le_sup_of_le_left h : F ≤ E ⊔ E') :=
  ((extendScalars.orderIso F).map_sup ⟨_, h⟩ ⟨_, h'⟩).symm

Supremum of Scalar Extensions Equals Scalar Extension of Supremum

Informal description

Let $F$, $E$, and $E'$ be fields with $F \leq E$ and $F \leq E'$. For any intermediate fields $K$ and $K'$ between $F$ and $E$ (resp. $F$ and $E'$), the supremum of the scalar extensions of $K$ and $K'$ is equal to the scalar extension of the supremum of $E$ and $E'$ under the condition that $F \leq E \sqcup E'$.

Subfield.extendScalars_inf theorem

: extendScalars h ⊓ extendScalars h' = extendScalars (le_inf h h')

Full source

theorem extendScalars_inf : extendScalarsextendScalars h ⊓ extendScalars h' = extendScalars (le_inf h h') :=
  ((extendScalars.orderIso F).map_inf ⟨_, h⟩ ⟨_, h'⟩).symm

Infimum of Scalar Extensions Equals Scalar Extension of Infimum

Informal description

Let $F$, $E$, and $E'$ be fields with $F \leq E$ and $F \leq E'$. Then the infimum of the scalar extensions of $E$ and $E'$ over $F$ is equal to the scalar extension of the infimum of $E$ and $E'$ over $F$, i.e., \[ \text{extendScalars}(h) \sqcap \text{extendScalars}(h') = \text{extendScalars}(\inf h h') \] where $h$ and $h'$ are the inclusion proofs $F \leq E$ and $F \leq E'$ respectively.

IntermediateField.extendScalars_self theorem

: extendScalars (le_refl F) = ⊥

Full source

@[simp]
theorem extendScalars_self : extendScalars (le_refl F) = ⊥ :=
  restrictScalars_injective K (by simp)

Scalar Extension of Reflexive Inclusion is Bottom Intermediate Field

Informal description

For any field $F$, the extension of scalars of the reflexive inclusion $F \leq F$ is equal to the bottom intermediate field $\bot$ in the lattice of intermediate fields between $F$ and itself.

IntermediateField.extendScalars_top theorem

: extendScalars (le_top : F ≤ ⊤) = ⊤

Full source

@[simp]
theorem extendScalars_top : extendScalars (le_top : F ≤ ⊤) = ⊤ :=
  restrictScalars_injective K (by simp)

Extension of Scalars to Top Intermediate Field is Top

Informal description

Let $F$ be a field and $\top$ be the largest intermediate field between $F$ and some extension field $E$. Then the extension of scalars of $F$ to $\top$ is equal to $\top$ itself, i.e., $F \leq \top$ implies $\text{extendScalars}(F \leq \top) = \top$.

IntermediateField.extendScalars_sup theorem

: extendScalars h ⊔ extendScalars h' = extendScalars (le_sup_of_le_left h : F ≤ E ⊔ E')

Full source

theorem extendScalars_sup :
    extendScalarsextendScalars h ⊔ extendScalars h' = extendScalars (le_sup_of_le_left h : F ≤ E ⊔ E') :=
  ((extendScalars.orderIso F).map_sup ⟨_, h⟩ ⟨_, h'⟩).symm

Supremum of Scalar Extensions Equals Scalar Extension of Supremum

Informal description

Let $F$, $E$, and $E'$ be fields with $F \leq E$ and $F \leq E'$. For any intermediate field extensions $h : F \leq E$ and $h' : F \leq E'$, the supremum of the scalar extensions $\text{extendScalars}(h)$ and $\text{extendScalars}(h')$ in the lattice of intermediate fields is equal to the scalar extension of the supremum inclusion $F \leq E \sqcup E'$, i.e., \[ \text{extendScalars}(h) \sqcup \text{extendScalars}(h') = \text{extendScalars}(F \leq E \sqcup E'). \]

IntermediateField.extendScalars_inf theorem

: extendScalars h ⊓ extendScalars h' = extendScalars (le_inf h h')

Full source

theorem extendScalars_inf : extendScalarsextendScalars h ⊓ extendScalars h' = extendScalars (le_inf h h') :=
  ((extendScalars.orderIso F).map_inf ⟨_, h⟩ ⟨_, h'⟩).symm

Infimum of Scalar Extensions Equals Scalar Extension of Infimum

Informal description

Let $F$, $E$, and $E'$ be fields with $F \leq E$ and $F \leq E'$. For any intermediate fields $K$ and $K'$ of $E$ and $E'$ respectively, the infimum of the scalar extensions of $K$ and $K'$ is equal to the scalar extension of the infimum of $K$ and $K'$. In other words, $\text{extendScalars}(h) \sqcap \text{extendScalars}(h') = \text{extendScalars}(\text{le\_inf}\ h\ h')$.