Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra

IntermediateField.algebra_adjoin_le_adjoin theorem

: Algebra.adjoin F S ≤ (adjoin F S).toSubalgebra

Full source

theorem algebra_adjoin_le_adjoin : Algebra.adjoin F S ≤ (adjoin F S).toSubalgebra :=
  Algebra.adjoin_le (subset_adjoin _ _)

Inclusion of Algebra Adjoin in Intermediate Field Adjoin

Informal description

For any field extension $E$ of $F$ and any subset $S \subseteq E$, the algebra generated by $S$ over $F$ is contained in the subalgebra corresponding to the intermediate field generated by $S$ over $F$. In other words, $\text{Algebra.adjoin}_F(S) \leq (\text{adjoin}_F(S)).\text{toSubalgebra}$.

IntermediateField.algebraAdjoinAdjoin.instAlgebraSubtypeMemSubalgebraAdjoinAdjoin instance

: Algebra (Algebra.adjoin F S) (adjoin F S)

Full source

/-- `IntermediateField.adjoin` as an algebra over `Algebra.adjoin`. -/
scoped instance : Algebra (Algebra.adjoin F S) (adjoin F S) :=
  (Subalgebra.inclusion <| algebra_adjoin_le_adjoin F S).toAlgebra

Algebra Structure on Intermediate Field Adjoin over Algebra Adjoin

Informal description

For any field extension $E$ of $F$ and any subset $S \subseteq E$, the intermediate field generated by $S$ over $F$ is naturally an algebra over the algebra generated by $S$ over $F$. In other words, $\text{adjoin}_F(S)$ is an $\text{Algebra.adjoin}_F(S)$-algebra.

IntermediateField.algebraAdjoinAdjoin.instIsScalarTowerSubtypeMemSubalgebraAdjoinAdjoin instance

(X) [SMul X F] [SMul X E] [IsScalarTower X F E] : IsScalarTower X (Algebra.adjoin F S) (adjoin F S)

Full source

scoped instance (X) [SMul X F] [SMul X E] [IsScalarTower X F E] :
    IsScalarTower X (Algebra.adjoin F S) (adjoin F S) :=
  Subalgebra.inclusion.isScalarTower_left (algebra_adjoin_le_adjoin F S) _

Scalar Tower Property for Adjoined Algebras and Intermediate Fields

Informal description

For any field extension $E$ of $F$, any subset $S \subseteq E$, and any type $X$ with scalar multiplication actions on $F$ and $E$ such that $X$ forms a scalar tower with $F$ and $E$, the scalar multiplication actions of $X$ on $\text{Algebra.adjoin}_F(S)$ and $\text{adjoin}_F(S)$ also form a scalar tower. That is, for any $x \in X$, $a \in \text{Algebra.adjoin}_F(S)$, and $b \in \text{adjoin}_F(S)$, we have $x \cdot (a \cdot b) = (x \cdot a) \cdot b$.

IntermediateField.algebraAdjoinAdjoin.instIsScalarTowerSubtypeMemSubalgebraAdjoinAdjoin_1 instance

(X) [MulAction E X] : IsScalarTower (Algebra.adjoin F S) (adjoin F S) X

Full source

scoped instance (X) [MulAction E X] : IsScalarTower (Algebra.adjoin F S) (adjoin F S) X :=
  Subalgebra.inclusion.isScalarTower_right (algebra_adjoin_le_adjoin F S) _

Scalar Tower Property for Adjoined Algebras Acting on Modules

Informal description

For any field extension $E$ of $F$, any subset $S \subseteq E$, and any type $X$ with a multiplicative action of $E$, the scalar multiplication actions of $\text{Algebra.adjoin}_F(S)$ and $\text{adjoin}_F(S)$ on $X$ form a scalar tower. That is, for any $a \in \text{Algebra.adjoin}_F(S)$, $b \in \text{adjoin}_F(S)$, and $x \in X$, we have $a \cdot (b \cdot x) = (a \cdot b) \cdot x$.

IntermediateField.algebraAdjoinAdjoin.instFaithfulSMulSubtypeMemSubalgebraAdjoinAdjoin instance

: FaithfulSMul (Algebra.adjoin F S) (adjoin F S)

Full source

scoped instance : FaithfulSMul (Algebra.adjoin F S) (adjoin F S) :=
  Subalgebra.inclusion.faithfulSMul (algebra_adjoin_le_adjoin F S)

Faithful Scalar Multiplication on Adjoined Intermediate Field

Informal description

For any field extension $E$ of $F$ and any subset $S \subseteq E$, the scalar multiplication action of the algebra generated by $S$ over $F$ on the intermediate field generated by $S$ over $F$ is faithful. That is, distinct elements of $\text{Algebra.adjoin}_F(S)$ act differently on $\text{adjoin}_F(S)$.

IntermediateField.algebraAdjoinAdjoin.instIsFractionRingSubtypeMemSubalgebraAdjoinAdjoin instance

: IsFractionRing (Algebra.adjoin F S) (adjoin F S)

Full source

scoped instance : IsFractionRing (Algebra.adjoin F S) (adjoin F S) :=
  .of_field _ _ fun ⟨_, h⟩ ↦ have ⟨x, hx, y, hy, eq⟩ := mem_adjoin_iff_div.mp h
    ⟨⟨x, hx⟩, ⟨y, hy⟩, Subtype.ext eq⟩

Intermediate Field Adjoin as Fraction Ring of Algebra Adjoin

Informal description

For any field extension $E$ of $F$ and subset $S \subseteq E$, the intermediate field $\text{adjoin}_F(S)$ is the fraction ring of the algebra $\text{Algebra.adjoin}_F(S)$. That is, $\text{adjoin}_F(S)$ is obtained by localizing $\text{Algebra.adjoin}_F(S)$ at its non-zero divisors.

IntermediateField.algebraAdjoinAdjoin.instIsAlgebraicSubtypeMemSubalgebraAdjoinAdjoin instance

: Algebra.IsAlgebraic (Algebra.adjoin F S) (adjoin F S)

Full source

scoped instance : Algebra.IsAlgebraic (Algebra.adjoin F S) (adjoin F S) :=
  IsLocalization.isAlgebraic _ (nonZeroDivisors (Algebra.adjoin F S))

Algebraicity of Intermediate Field Adjoin over Algebra Adjoin

Informal description

For any field extension $E$ of $F$ and subset $S \subseteq E$, the intermediate field $\text{adjoin}_F(S)$ is algebraic over the algebra $\text{Algebra.adjoin}_F(S)$. That is, every element of $\text{adjoin}_F(S)$ is algebraic over $\text{Algebra.adjoin}_F(S)$.

IntermediateField.adjoin_eq_algebra_adjoin theorem

 (inv_mem : ∀ x ∈ Algebra.adjoin F S, x⁻¹ ∈ Algebra.adjoin F S) : (adjoin F S).toSubalgebra = Algebra.adjoin F S

Full source

theorem adjoin_eq_algebra_adjoin (inv_mem : ∀ x ∈ Algebra.adjoin F S, x⁻¹ ∈ Algebra.adjoin F S) :
    (adjoin F S).toSubalgebra = Algebra.adjoin F S :=
  le_antisymm
    (show adjoin F S ≤
        { Algebra.adjoin F S with
          inv_mem' := inv_mem }
      from adjoin_le_iff.mpr Algebra.subset_adjoin)
    (algebra_adjoin_le_adjoin _ _)

Equality of Intermediate Field Adjoin and Algebra Adjoin under Inversion Closure

Informal description

Let $F$ be a field and $E$ a field extension of $F$. For any subset $S \subseteq E$, if every element $x$ in the algebra generated by $S$ over $F$ has its inverse $x^{-1}$ also in $\text{Algebra.adjoin}_F(S)$, then the subalgebra corresponding to the intermediate field generated by $S$ over $F$ is equal to $\text{Algebra.adjoin}_F(S)$. In other words, $(\text{adjoin}_F(S)).\text{toSubalgebra} = \text{Algebra.adjoin}_F(S)$.

IntermediateField.adjoin_eq_top_of_algebra theorem

(hS : Algebra.adjoin F S = ⊤) : adjoin F S = ⊤

Full source

theorem adjoin_eq_top_of_algebra (hS : Algebra.adjoin F S = ⊤) : adjoin F S = ⊤ :=
  top_le_iff.mp (hS.symm.trans_le <| algebra_adjoin_le_adjoin F S)

Maximality of Intermediate Field Adjoin from Maximal Algebra Adjoin

Informal description

Let $F$ be a field and $E$ be a field extension of $F$. For any subset $S \subseteq E$, if the algebra generated by $S$ over $F$ is the entire extension (i.e., $\text{Algebra.adjoin}_F(S) = \top$), then the intermediate field generated by $S$ over $F$ is also the entire extension (i.e., $\text{adjoin}_F(S) = \top$).

IntermediateField.AdjoinSimple.isIntegral_gen theorem

: IsIntegral F (AdjoinSimple.gen F α) ↔ IsIntegral F α

Full source

@[simp]
theorem AdjoinSimple.isIntegral_gen : IsIntegralIsIntegral F (AdjoinSimple.gen F α) ↔ IsIntegral F α := by
  conv_rhs => rw [← AdjoinSimple.algebraMap_gen F α]
  rw [isIntegral_algebraMap_iff (algebraMap F⟮α⟯ E).injective]

Integrality of Generator in Simple Field Extension

Informal description

Let $F$ be a field and $E$ be a field extension of $F$. For any element $\alpha \in E$, the generator of the simple extension field $F(\alpha)$ (denoted as $\text{AdjoinSimple.gen}\, F\,\alpha$) is integral over $F$ if and only if $\alpha$ itself is integral over $F$.

IntermediateField.adjoin_algebraic_toSubalgebra theorem

{S : Set E} (hS : ∀ x ∈ S, IsAlgebraic F x) : (IntermediateField.adjoin F S).toSubalgebra = Algebra.adjoin F S

Full source

theorem adjoin_algebraic_toSubalgebra {S : Set E} (hS : ∀ x ∈ S, IsAlgebraic F x) :
    (IntermediateField.adjoin F S).toSubalgebra = Algebra.adjoin F S :=
  adjoin_eq_algebra_adjoin _ _ fun _ ↦
    (Algebra.IsIntegral.adjoin fun x hx ↦ (hS x hx).isIntegral).inv_mem

Equality of Intermediate Field Adjoin and Algebra Adjoin for Algebraic Elements

Informal description

Let $F$ be a field and $E$ a field extension of $F$. For any subset $S \subseteq E$ where every element $x \in S$ is algebraic over $F$, the subalgebra corresponding to the intermediate field generated by $S$ over $F$ equals the algebra generated by $S$ over $F$, i.e., $(\text{adjoin}_F(S)).\text{toSubalgebra} = \text{Algebra.adjoin}_F(S)$.

IntermediateField.adjoin_simple_toSubalgebra_of_integral theorem

(hα : IsIntegral F α) : F⟮α⟯.toSubalgebra = Algebra.adjoin F { α }

Full source

theorem adjoin_simple_toSubalgebra_of_integral (hα : IsIntegral F α) :
    F⟮α⟯.toSubalgebra = Algebra.adjoin F {α} := by
  apply adjoin_algebraic_toSubalgebra
  rintro x (rfl : x = α)
  rwa [isAlgebraic_iff_isIntegral]

Equality of Simple Field Extension Subalgebra and Algebra Adjoin for Integral Elements

Informal description

Let $F$ be a field and $E$ a field extension of $F$. For any element $\alpha \in E$ that is integral over $F$, the subalgebra corresponding to the simple extension field $F(\alpha)$ equals the algebra generated by $\alpha$ over $F$, i.e., $F(\alpha).\text{toSubalgebra} = \text{Algebra.adjoin}_F \{\alpha\}$.

IntermediateField.le_sup_toSubalgebra theorem

: E1.toSubalgebra ⊔ E2.toSubalgebra ≤ (E1 ⊔ E2).toSubalgebra

Full source

theorem le_sup_toSubalgebra : E1.toSubalgebra ⊔ E2.toSubalgebra ≤ (E1 ⊔ E2).toSubalgebra :=
  sup_le (show E1 ≤ E1 ⊔ E2 from le_sup_left) (show E2 ≤ E1 ⊔ E2 from le_sup_right)

Subalgebra Supremum is Contained in Intermediate Field Supremum's Subalgebra

Informal description

For any intermediate fields $E_1$ and $E_2$ of a field extension $K \subseteq L$, the supremum of their underlying subalgebras is contained in the subalgebra underlying their supremum as intermediate fields, i.e., $E_1.\text{toSubalgebra} \sqcup E_2.\text{toSubalgebra} \leq (E_1 \sqcup E_2).\text{toSubalgebra}$.

IntermediateField.sup_toSubalgebra_of_isAlgebraic_right theorem

[Algebra.IsAlgebraic K E2] : (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra

Full source

theorem sup_toSubalgebra_of_isAlgebraic_right [Algebra.IsAlgebraic K E2] :
    (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra := by
  have : (adjoin E1 (E2 : Set L)).toSubalgebra = _ := adjoin_algebraic_toSubalgebra fun x h ↦
    IsAlgebraic.tower_top E1 (isAlgebraic_iff.1
      (Algebra.IsAlgebraic.isAlgebraic (⟨x, h⟩ : E2)))
  apply_fun Subalgebra.restrictScalars K at this
  rw [← restrictScalars_toSubalgebra, restrictScalars_adjoin] at this
  -- TODO: rather than using `← coe_type_toSubalgera` here, perhaps we should restate another
  -- version of `Algebra.restrictScalars_adjoin` for intermediate fields?
  simp only [← coe_type_toSubalgebra] at this
  rw [Algebra.restrictScalars_adjoin] at this
  exact this

Subalgebra Join Equality for Algebraic Intermediate Field Extensions (Right Case)

Informal description

Let $K$ be a field and $E_1, E_2$ be intermediate field extensions of $K$. If $E_2$ is algebraic over $K$, then the subalgebra corresponding to the join $E_1 \sqcup E_2$ equals the join of their corresponding subalgebras, i.e., \[ (E_1 \sqcup E_2).\text{toSubalgebra} = E_1.\text{toSubalgebra} \sqcup E_2.\text{toSubalgebra}. \]

IntermediateField.sup_toSubalgebra_of_isAlgebraic_left theorem

[Algebra.IsAlgebraic K E1] : (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra

Full source

theorem sup_toSubalgebra_of_isAlgebraic_left [Algebra.IsAlgebraic K E1] :
    (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra := by
  have := sup_toSubalgebra_of_isAlgebraic_right E2 E1
  rwa [sup_comm (a := E1), sup_comm (a := E1.toSubalgebra)]

Subalgebra Join Equality for Algebraic Intermediate Field Extensions (Left Case)

Informal description

Let $K$ be a field and $E_1, E_2$ be intermediate field extensions of $K$. If $E_1$ is algebraic over $K$, then the subalgebra corresponding to the join $E_1 \sqcup E_2$ equals the join of their corresponding subalgebras, i.e., \[ (E_1 \sqcup E_2).\text{toSubalgebra} = E_1.\text{toSubalgebra} \sqcup E_2.\text{toSubalgebra}. \]

IntermediateField.sup_toSubalgebra_of_isAlgebraic theorem

 (halg : Algebra.IsAlgebraic K E1 ∨ Algebra.IsAlgebraic K E2) :
  (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra

Full source

/-- The compositum of two intermediate fields is equal to the compositum of them
as subalgebras, if one of them is algebraic over the base field. -/
theorem sup_toSubalgebra_of_isAlgebraic
    (halg : Algebra.IsAlgebraicAlgebra.IsAlgebraic K E1 ∨ Algebra.IsAlgebraic K E2) :
    (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra :=
  halg.elim (fun _ ↦ sup_toSubalgebra_of_isAlgebraic_left E1 E2)
    (fun _ ↦ sup_toSubalgebra_of_isAlgebraic_right E1 E2)

Subalgebra Join Equality for Algebraic Intermediate Field Extensions

Informal description

Let $K$ be a field and $E_1, E_2$ be intermediate field extensions of $K$. If either $E_1$ or $E_2$ is algebraic over $K$, then the subalgebra corresponding to the join $E_1 \sqcup E_2$ equals the join of their corresponding subalgebras, i.e., \[ (E_1 \sqcup E_2).\text{toSubalgebra} = E_1.\text{toSubalgebra} \sqcup E_2.\text{toSubalgebra}. \]

IntermediateField.sup_toSubalgebra_of_left theorem

[FiniteDimensional K E1] : (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra

Full source

theorem sup_toSubalgebra_of_left [FiniteDimensional K E1] :
    (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra :=
  sup_toSubalgebra_of_isAlgebraic_left E1 E2

Subalgebra Join Equality for Finite-Dimensional Intermediate Field Extensions (Left Case)

Informal description

Let $K$ be a field and $E_1, E_2$ be intermediate field extensions of $K$. If $E_1$ is finite-dimensional as a vector space over $K$, then the subalgebra corresponding to the join $E_1 \sqcup E_2$ equals the join of their corresponding subalgebras, i.e., \[ (E_1 \sqcup E_2).\text{toSubalgebra} = E_1.\text{toSubalgebra} \sqcup E_2.\text{toSubalgebra}. \]

IntermediateField.sup_toSubalgebra_of_right theorem

[FiniteDimensional K E2] : (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra

Full source

theorem sup_toSubalgebra_of_right [FiniteDimensional K E2] :
    (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra :=
  sup_toSubalgebra_of_isAlgebraic_right E1 E2

Subalgebra Join Equality for Finite-Dimensional Intermediate Field Extensions (Right Case)

Informal description

Let $K$ be a field and $E_1, E_2$ be intermediate field extensions of $K$. If $E_2$ is finite-dimensional as a vector space over $K$, then the subalgebra corresponding to the join $E_1 \sqcup E_2$ equals the join of their corresponding subalgebras, i.e., \[ (E_1 \sqcup E_2).\text{toSubalgebra} = E_1.\text{toSubalgebra} \sqcup E_2.\text{toSubalgebra}. \]

IntermediateField.adjoin_toSubalgebra_of_isAlgebraic theorem

 (L : IntermediateField F K) (halg : Algebra.IsAlgebraic F E ∨ Algebra.IsAlgebraic F L) :
  (adjoin E (L : Set K)).toSubalgebra = Algebra.adjoin E (L : Set K)

Full source

/-- If `K / E / F` is a field extension tower, `L` is an intermediate field of `K / F`, such that
either `E / F` or `L / F` is algebraic, then `E(L) = E[L]`. -/
theorem adjoin_toSubalgebra_of_isAlgebraic (L : IntermediateField F K)
    (halg : Algebra.IsAlgebraicAlgebra.IsAlgebraic F E ∨ Algebra.IsAlgebraic F L) :
    (adjoin E (L : Set K)).toSubalgebra = Algebra.adjoin E (L : Set K) := by
  let i := IsScalarTower.toAlgHom F E K
  let E' := i.fieldRange
  let i' : E ≃ₐ[F] E' := AlgEquiv.ofInjectiveField i
  have hi : algebraMap E K = (algebraMap E' K) ∘ i' := by ext x; rfl
  apply_fun _ using Subalgebra.restrictScalars_injective F
  rw [← restrictScalars_toSubalgebra, restrictScalars_adjoin_of_algEquiv i' hi,
    Algebra.restrictScalars_adjoin_of_algEquiv i' hi, restrictScalars_adjoin]
  dsimp only [← E'.coe_type_toSubalgebra]
  rw [Algebra.restrictScalars_adjoin F E'.toSubalgebra]
  exact E'.sup_toSubalgebra_of_isAlgebraic L (halg.imp
    (fun (_ : Algebra.IsAlgebraic F E) ↦ i'.isAlgebraic) id)

Equality of Subalgebra and Field Adjoin for Algebraic Extensions

Informal description

Let $F \subseteq E \subseteq K$ be a tower of field extensions, and let $L$ be an intermediate field of $K/F$. If either $E/F$ or $L/F$ is algebraic, then the subalgebra generated by $L$ over $E$ is equal to the field adjunction of $L$ over $E$. In symbols: \[ \text{adjoin}_E(L).\text{toSubalgebra} = \text{Algebra.adjoin}_E(L). \]

IntermediateField.adjoin_toSubalgebra_of_isAlgebraic_left theorem

 (L : IntermediateField F K) [halg : Algebra.IsAlgebraic F E] :
  (adjoin E (L : Set K)).toSubalgebra = Algebra.adjoin E (L : Set K)

Full source

theorem adjoin_toSubalgebra_of_isAlgebraic_left (L : IntermediateField F K)
    [halg : Algebra.IsAlgebraic F E] :
    (adjoin E (L : Set K)).toSubalgebra = Algebra.adjoin E (L : Set K) :=
  adjoin_toSubalgebra_of_isAlgebraic E L (Or.inl halg)

Equality of Subalgebra and Field Adjoin for Left Algebraic Extensions

Informal description

Let $F \subseteq E \subseteq K$ be a tower of field extensions, and let $L$ be an intermediate field of $K/F$. If $E/F$ is algebraic, then the subalgebra generated by $L$ over $E$ is equal to the field adjunction of $L$ over $E$. In symbols: \[ \text{adjoin}_E(L).\text{toSubalgebra} = \text{Algebra.adjoin}_E(L). \]

IntermediateField.adjoin_toSubalgebra_of_isAlgebraic_right theorem

 (L : IntermediateField F K) [halg : Algebra.IsAlgebraic F L] :
  (adjoin E (L : Set K)).toSubalgebra = Algebra.adjoin E (L : Set K)

Full source

theorem adjoin_toSubalgebra_of_isAlgebraic_right (L : IntermediateField F K)
    [halg : Algebra.IsAlgebraic F L] :
    (adjoin E (L : Set K)).toSubalgebra = Algebra.adjoin E (L : Set K) :=
  adjoin_toSubalgebra_of_isAlgebraic E L (Or.inr halg)

Equality of Subalgebra and Field Adjoin for Right Algebraic Extensions

Informal description

Let $F \subseteq E \subseteq K$ be a tower of field extensions, and let $L$ be an intermediate field of $K/F$. If $L/F$ is algebraic, then the subalgebra generated by $L$ over $E$ is equal to the field adjunction of $L$ over $E$. In symbols: \[ \text{adjoin}_E(L).\text{toSubalgebra} = \text{Algebra.adjoin}_E(L). \]

IntermediateField.fg_of_fg_toSubalgebra theorem

(S : IntermediateField F E) (h : S.toSubalgebra.FG) : S.FG

Full source

theorem fg_of_fg_toSubalgebra (S : IntermediateField F E) (h : S.toSubalgebra.FG) : S.FG := by
  obtain ⟨t, ht⟩ := h
  exact ⟨t, (eq_adjoin_of_eq_algebra_adjoin _ _ _ ht.symm).symm⟩

Finitely generated intermediate field from finitely generated subalgebra

Informal description

Let $S$ be an intermediate field between fields $F$ and $E$. If the underlying subalgebra of $S$ is finitely generated as an $F$-algebra, then $S$ itself is finitely generated as an intermediate field over $F$.

IntermediateField.fg_of_noetherian theorem

(S : IntermediateField F E) [IsNoetherian F E] : S.FG

Full source

theorem fg_of_noetherian (S : IntermediateField F E) [IsNoetherian F E] : S.FG :=
  S.fg_of_fg_toSubalgebra S.toSubalgebra.fg_of_noetherian

Noetherianity implies finite generation of intermediate fields

Informal description

Let $F$ and $E$ be fields with $F \subseteq E$, and suppose $E$ is Noetherian as an $F$-module. Then every intermediate field $S$ between $F$ and $E$ is finitely generated as an intermediate field over $F$.

IntermediateField.induction_on_adjoin theorem

 [FiniteDimensional F E] (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) : P K

Full source

theorem induction_on_adjoin [FiniteDimensional F E] (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) : P K :=
  letI : IsNoetherian F E := IsNoetherian.iff_fg.2 inferInstance
  induction_on_adjoin_fg P base ih K K.fg_of_noetherian

Induction Principle for Intermediate Fields via Adjoining Elements

Informal description

Let $F \subseteq E$ be a finite-dimensional field extension. For any property $P$ of intermediate fields between $F$ and $E$, if: 1. $P$ holds for the trivial intermediate field $\bot$ (i.e., $F$ itself), and 2. For any intermediate field $K$ and any element $x \in E$, if $P$ holds for $K$, then $P$ holds for $K⟮x⟯$ (the field obtained by adjoining $x$ to $K$), then $P$ holds for all intermediate fields $K$ between $F$ and $E$.

IsFractionRing.algHom_fieldRange_eq_of_comp_eq theorem

(h : RingHom.comp f (algebraMap A K) = (g : A →+* L)) : f.fieldRange = IntermediateField.adjoin F g.range

Full source

/-- If `F` is a field, `A` is an `F`-algebra with fraction field `K`, `L` is a field,
`g : A →ₐ[F] L` lifts to `f : K →ₐ[F] L`,
then the image of `f` is the field generated by the image of `g`.
Note: this does not require `IsScalarTower F A K`. -/
theorem algHom_fieldRange_eq_of_comp_eq (h : RingHom.comp f (algebraMap A K) = (g : A →+* L)) :
    f.fieldRange = IntermediateField.adjoin F g.range := by
  apply IntermediateField.toSubfield_injective
  simp_rw [AlgHom.fieldRange_toSubfield, IntermediateField.adjoin_toSubfield]
  convert ringHom_fieldRange_eq_of_comp_eq h using 2
  exact Set.union_eq_self_of_subset_left fun _ ⟨x, hx⟩ ↦ ⟨algebraMap F A x, by simp [← hx]⟩

Image of Fraction Field Homomorphism Equals Adjoin of Base Algebra Homomorphism Image

Informal description

Let $F$ be a field, $A$ an $F$-algebra with fraction field $K$, and $L$ a field. Given an $F$-algebra homomorphism $g : A \to L$ and an $F$-algebra homomorphism $f : K \to L$ such that $f \circ \text{algebraMap}\ A\ K = g$, the image of $f$ is equal to the intermediate field generated over $F$ by the image of $g$, i.e., \[ f(K) = F(g(A)). \]

IsFractionRing.algHom_fieldRange_eq_of_comp_eq_of_range_eq theorem

 (h : RingHom.comp f (algebraMap A K) = (g : A →+* L)) {s : Set L} (hs : g.range = Algebra.adjoin F s) :
  f.fieldRange = IntermediateField.adjoin F s

Full source

/-- If `F` is a field, `A` is an `F`-algebra with fraction field `K`, `L` is a field,
`g : A →ₐ[F] L` lifts to `f : K →ₐ[F] L`,
`s` is a set such that the image of `g` is the subalgebra generated by `s`,
then the image of `f` is the intermediate field generated by `s`.
Note: this does not require `IsScalarTower F A K`. -/
theorem algHom_fieldRange_eq_of_comp_eq_of_range_eq
    (h : RingHom.comp f (algebraMap A K) = (g : A →+* L))
    {s : Set L} (hs : g.range = Algebra.adjoin F s) :
    f.fieldRange = IntermediateField.adjoin F s := by
  apply IntermediateField.toSubfield_injective
  simp_rw [AlgHom.fieldRange_toSubfield, IntermediateField.adjoin_toSubfield]
  refine ringHom_fieldRange_eq_of_comp_eq_of_range_eq h ?_
  rw [← Algebra.adjoin_eq_ring_closure, ← hs]; rfl

Image of Fraction Field Homomorphism Equals Intermediate Field Generated by Prescribed Set

Informal description

Let $F$ be a field, $A$ an $F$-algebra with fraction field $K$, and $L$ a field. Given an $F$-algebra homomorphism $g \colon A \to L$ and an $F$-algebra homomorphism $f \colon K \to L$ such that $f \circ \text{algebraMap}_A^K = g$, and a subset $s \subseteq L$ such that the image of $g$ equals the $F$-subalgebra generated by $s$, then the image of $f$ equals the intermediate field generated over $F$ by $s$, i.e., \[ f(K) = F(s). \]

IsFractionRing.liftAlgHom_fieldRange theorem

(hg : Function.Injective g) : (liftAlgHom hg : K →ₐ[F] L).fieldRange = IntermediateField.adjoin F g.range

Full source

/-- The image of `IsFractionRing.liftAlgHom` is the intermediate field generated by the image
of the algebra hom. -/
theorem liftAlgHom_fieldRange (hg : Function.Injective g) :
    (liftAlgHom hg : K →ₐ[F] L).fieldRange = IntermediateField.adjoin F g.range :=
  algHom_fieldRange_eq_of_comp_eq (by ext; simp)

Image of Fraction Field Algebra Homomorphism Equals Adjoin of Base Homomorphism Image

Informal description

Let $F$ be a field, $A$ an $F$-algebra with fraction field $K$, and $L$ a field extension of $F$. Given an injective $F$-algebra homomorphism $g : A \to L$, the image of the lifted algebra homomorphism $\operatorname{liftAlgHom}\ hg : K \to L$ is equal to the intermediate field generated over $F$ by the image of $g$, i.e., \[ (\operatorname{liftAlgHom}\ hg)(K) = F(g(A)). \]

IsFractionRing.liftAlgHom_fieldRange_eq_of_range_eq theorem

 (hg : Function.Injective g) {s : Set L} (hs : g.range = Algebra.adjoin F s) :
  (liftAlgHom hg : K →ₐ[F] L).fieldRange = IntermediateField.adjoin F s

Full source

/-- The image of `IsFractionRing.liftAlgHom` is the intermediate field generated by `s`,
if the image of the algebra hom is the subalgebra generated by `s`. -/
theorem liftAlgHom_fieldRange_eq_of_range_eq (hg : Function.Injective g)
    {s : Set L} (hs : g.range = Algebra.adjoin F s) :
    (liftAlgHom hg : K →ₐ[F] L).fieldRange = IntermediateField.adjoin F s :=
  algHom_fieldRange_eq_of_comp_eq_of_range_eq (by ext; simp) hs

Image of Lifted Algebra Homomorphism Equals Intermediate Field Generated by Prescribed Set

Informal description

Let $F$ be a field, $A$ an $F$-algebra with fraction field $K$, and $L$ a field extension of $F$. Given an injective $F$-algebra homomorphism $g \colon A \to L$ and a subset $s \subseteq L$ such that the image of $g$ equals the $F$-subalgebra generated by $s$, then the image of the lifted algebra homomorphism $\operatorname{liftAlgHom}\ hg \colon K \to L$ is equal to the intermediate field generated over $F$ by $s$, i.e., \[ (\operatorname{liftAlgHom}\ hg)(K) = F(s). \]