Mathlib.FieldTheory.Fixed

FixedBy.subfield definition

: Subfield F

Full source

/-- The subfield of F fixed by the field endomorphism `m`. -/
def FixedBy.subfield : Subfield F where
  carrier := fixedBy F m
  zero_mem' := smul_zero m
  add_mem' hx hy := (smul_add m _ _).trans <| congr_arg₂ _ hx hy
  neg_mem' hx := (smul_neg m _).trans <| congr_arg _ hx
  one_mem' := smul_one m
  mul_mem' hx hy := (smul_mul' m _ _).trans <| congr_arg₂ _ hx hy
  inv_mem' x hx := (smul_inv'' m x).trans <| congr_arg _ hx

Fixed subfield under a field endomorphism

Informal description

The subfield of $ F $ consisting of all elements fixed by the field endomorphism $ m $, i.e., elements $ x \in F $ such that $ m \cdot x = x $. This subfield is closed under addition, negation, multiplication, and inversion, and contains the additive and multiplicative identities.

IsInvariantSubfield structure

(S : Subfield F)

Full source

/-- A typeclass for subrings invariant under a `MulSemiringAction`. -/
class IsInvariantSubfield (S : Subfield F) : Prop where
  smul_mem : ∀ (m : M) {x : F}, x ∈ S → m • x ∈ S

Invariant Subfield under Multiplicative Semiring Action

Informal description

A subfield $ S $ of a field $ F $ is called *invariant under a multiplicative semiring action* if it is preserved by the action of a monoid $ M $ on $ F $. This means that for every element $ m \in M $ and every $ s \in S $, the result of the action $ m \cdot s $ remains in $ S $.

IsInvariantSubfield.toMulSemiringAction instance

[IsInvariantSubfield M S] : MulSemiringAction M S

Full source

instance IsInvariantSubfield.toMulSemiringAction [IsInvariantSubfield M S] :
    MulSemiringAction M S where
  smul m x := ⟨m • x.1, IsInvariantSubfield.smul_mem m x.2⟩
  one_smul s := Subtype.eq <| one_smul M s.1
  mul_smul m₁ m₂ s := Subtype.eq <| mul_smul m₁ m₂ s.1
  smul_add m s₁ s₂ := Subtype.eq <| smul_add m s₁.1 s₂.1
  smul_zero m := Subtype.eq <| smul_zero m
  smul_one m := Subtype.eq <| smul_one m
  smul_mul m s₁ s₂ := Subtype.eq <| smul_mul' m s₁.1 s₂.1

Multiplicative Semiring Action on Invariant Subfields

Informal description

For any monoid $M$ acting on a field $F$ and a subfield $S$ of $F$ that is invariant under the action of $M$, there is a canonical multiplicative semiring action of $M$ on $S$.

instIsInvariantSubringOfIsInvariantSubfield instance

[IsInvariantSubfield M S] : IsInvariantSubring M S.toSubring

Full source

instance [IsInvariantSubfield M S] : IsInvariantSubring M S.toSubring where
  smul_mem := IsInvariantSubfield.smul_mem

Invariant Subfields Yield Invariant Subrings

Informal description

For any monoid $M$ acting on a field $F$ and any subfield $S$ of $F$ that is invariant under the action of $M$, the underlying subring of $S$ is also invariant under the action of $M$.

FixedPoints.subfield definition

: Subfield F

Full source

/-- The subfield of fixed points by a monoid action. -/
def subfield : Subfield F :=
  Subfield.copy (⨅ m : M, FixedBy.subfield F m) (fixedPoints M F)
    (by ext z; simp [fixedPoints, FixedBy.subfield, iInf, Subfield.mem_sInf]; rfl)

Fixed subfield under a monoid action

Informal description

The subfield of $F$ consisting of all elements fixed by every element of the monoid $M$ under its action on $F$, i.e., elements $x \in F$ such that $m \cdot x = x$ for all $m \in M$.

FixedPoints.instIsInvariantSubfieldSubfield instance

: IsInvariantSubfield M (FixedPoints.subfield M F)

Full source

instance : IsInvariantSubfield M (FixedPoints.subfield M F) where
  smul_mem g x hx g' := by rw [hx, hx]

Invariance of the Fixed Subfield under Monoid Action

Informal description

For any monoid $M$ acting on a field $F$, the fixed subfield $\text{FixedPoints.subfield}\ M\ F$ is invariant under the action of $M$. That is, for every $m \in M$ and $x \in \text{FixedPoints.subfield}\ M\ F$, we have $m \cdot x \in \text{FixedPoints.subfield}\ M\ F$.

FixedPoints.instSMulCommClassSubtypeMemSubfieldSubfield instance

: SMulCommClass M (FixedPoints.subfield M F) F

Full source

instance : SMulCommClass M (FixedPoints.subfield M F) F where
  smul_comm m f f' := show m • (↑f * f') = f * m • f' by rw [smul_mul', f.prop m]

Commutativity of Monoid Action with Fixed Subfield Scalar Multiplication

Informal description

For a monoid $M$ acting on a field $F$, the action of $M$ commutes with the scalar multiplication by elements of the fixed subfield $\text{FixedPoints.subfield}\, M\, F$. That is, for any $m \in M$, $s \in \text{FixedPoints.subfield}\, M\, F$, and $x \in F$, we have $m \cdot (s \cdot x) = s \cdot (m \cdot x)$.

FixedPoints.smulCommClass' instance

: SMulCommClass (FixedPoints.subfield M F) M F

Full source

instance smulCommClass' : SMulCommClass (FixedPoints.subfield M F) M F :=
  SMulCommClass.symm _ _ _

Commutativity of Fixed Subfield Scalar Multiplication with Monoid Action

Informal description

For a monoid $M$ acting on a field $F$, the scalar multiplication by elements of the fixed subfield $\text{FixedPoints.subfield}\, M\, F$ commutes with the action of $M$ on $F$. That is, for any $s \in \text{FixedPoints.subfield}\, M\, F$, $m \in M$, and $x \in F$, we have $s \cdot (m \cdot x) = m \cdot (s \cdot x)$.

FixedPoints.smul theorem

(m : M) (x : FixedPoints.subfield M F) : m • x = x

Full source

@[simp]
theorem smul (m : M) (x : FixedPoints.subfield M F) : m • x = x :=
  Subtype.eq <| x.2 m

Invariance of Fixed Subfield Elements under Monoid Action

Informal description

For any element $m$ of a monoid $M$ acting on a field $F$ and any element $x$ in the fixed subfield $\text{FixedPoints.subfield}\, M\, F$, the action of $m$ on $x$ leaves $x$ unchanged, i.e., $m \cdot x = x$.

FixedPoints.smul_polynomial theorem

(m : M) (p : Polynomial (FixedPoints.subfield M F)) : m • p = p

Full source

@[simp]
theorem smul_polynomial (m : M) (p : Polynomial (FixedPoints.subfield M F)) : m • p = p :=
  Polynomial.induction_on p (fun x => by rw [Polynomial.smul_C, smul])
    (fun p q ihp ihq => by rw [smul_add, ihp, ihq]) fun n x _ => by
    rw [smul_mul', Polynomial.smul_C, smul, smul_pow', Polynomial.smul_X]

Invariance of Polynomials over Fixed Subfield under Monoid Action

Informal description

For any element $m$ of a monoid $M$ acting on a field $F$ and any polynomial $p$ with coefficients in the fixed subfield $\text{FixedPoints.subfield}\, M\, F$, the action of $m$ on $p$ leaves $p$ unchanged, i.e., $m \cdot p = p$.

FixedPoints.instAlgebraSubtypeMemSubfieldSubfield instance

: Algebra (FixedPoints.subfield M F) F

Full source

instance : Algebra (FixedPoints.subfield M F) F := by infer_instance

Algebra Structure on the Fixed Subfield

Informal description

For any monoid $M$ acting on a field $F$, the fixed subfield $\text{FixedPoints.subfield}\ M\ F$ is equipped with a canonical algebra structure over $F$. This means there is a natural ring homomorphism from the fixed subfield to $F$ that preserves the field operations.

FixedPoints.coe_algebraMap theorem

: algebraMap (FixedPoints.subfield M F) F = Subfield.subtype (FixedPoints.subfield M F)

Full source

theorem coe_algebraMap :
    algebraMap (FixedPoints.subfield M F) F = Subfield.subtype (FixedPoints.subfield M F) :=
  rfl

Algebra Map Equals Subfield Inclusion for Fixed Points

Informal description

The algebra map from the fixed subfield $\text{FixedPoints.subfield}\ M\ F$ to $F$ is equal to the canonical inclusion map of the subfield into $F$.

FixedPoints.linearIndependent_smul_of_linearIndependent theorem

{s : Finset F} : (LinearIndepOn (FixedPoints.subfield G F) id (s : Set F)) → LinearIndepOn F (MulAction.toFun G F) s

Full source

theorem linearIndependent_smul_of_linearIndependent {s : Finset F} :
    (LinearIndepOn (FixedPoints.subfield G F) id (s : Set F)) →
      LinearIndepOn F (MulAction.toFun G F) s := by
  classical
  have : IsEmpty ((∅ : Finset F) : Set F) := by simp
  refine Finset.induction_on s (fun _ => linearIndependent_empty_type) fun a s has ih hs => ?_
  rw [coe_insert] at hs ⊢
  rw [linearIndepOn_insert (mt mem_coe.1 has)] at hs
  rw [linearIndepOn_insert (mt mem_coe.1 has)]; refine ⟨ih hs.1, fun ha => ?_⟩
  rw [Finsupp.mem_span_image_iff_linearCombination] at ha; rcases ha with ⟨l, hl, hla⟩
  rw [Finsupp.linearCombination_apply_of_mem_supported F hl] at hla
  suffices ∀ i ∈ s, l i ∈ FixedPoints.subfield G F by
    replace hla := (sum_apply _ _ fun i => l i • toFun G F i).symm.trans (congr_fun hla 1)
    simp_rw [Pi.smul_apply, toFun_apply, one_smul] at hla
    refine hs.2 (hla ▸ Submodule.sum_mem _ fun c hcs => ?_)
    change (⟨l c, this c hcs⟩ : FixedPoints.subfield G F) • c ∈ _
    exact Submodule.smul_mem _ _ <| Submodule.subset_span <| by simpa

  intro i his g
  refine
    eq_of_sub_eq_zero
      (linearIndependent_iff'.1 (ih hs.1) s.attach (fun i => g • l i - l i) ?_ ⟨i, his⟩
          (mem_attach _ _) :
        _)
  refine (sum_attach s fun i ↦ (g • l i - l i) • MulAction.toFun G F i).trans ?_
  ext g'; dsimp only
  conv_lhs =>
    rw [sum_apply]
    congr
    · skip
    · ext
      rw [Pi.smul_apply, sub_smul, smul_eq_mul]
  rw [sum_sub_distrib, Pi.zero_apply, sub_eq_zero]
  conv_lhs =>
    congr
    · skip
    · ext x
      rw [toFun_apply, ← mul_inv_cancel_left g g', mul_smul, ← smul_mul', ← toFun_apply _ x]
  show
    (∑ x ∈ s, g • (fun y => l y • MulAction.toFun G F y) x (g⁻¹ * g')) =
      ∑ x ∈ s, (fun y => l y • MulAction.toFun G F y) x g'
  rw [← smul_sum, ← sum_apply _ _ fun y => l y • toFun G F y, ←
    sum_apply _ _ fun y => l y • toFun G F y]
  rw [hla, toFun_apply, toFun_apply, smul_smul, mul_inv_cancel_left]

Linear Independence Preservation under Group Action on Field Elements

Informal description

Let $G$ be a group acting on a field $F$, and let $s$ be a finite subset of $F$. If the set $s$ is linearly independent over the fixed subfield $\text{FixedPoints.subfield } G F$, then the set $\{g \cdot x \mid g \in G, x \in s\}$ is linearly independent over $F$.

FixedPoints.minpoly definition

: Polynomial (FixedPoints.subfield G F)

Full source

/-- `minpoly G F x` is the minimal polynomial of `(x : F)` over `FixedPoints.subfield G F`. -/
def minpoly : Polynomial (FixedPoints.subfield G F) :=
  (prodXSubSMul G F x).toSubring (FixedPoints.subfield G F).toSubring fun _ hc g =>
    let ⟨n, _, hn⟩ := Polynomial.mem_coeffs_iff.1 hc
    hn.symm ▸ prodXSubSMul.coeff G F x g n

Minimal polynomial over the fixed subfield under group action

Informal description

The minimal polynomial of an element $ x \in F $ over the fixed subfield $ \text{FixedPoints.subfield } G F $, where $ G $ is a group acting on the field $ F $. This polynomial is monic and has $ x $ as a root when evaluated in $ F $.

FixedPoints.minpoly.monic theorem

: (minpoly G F x).Monic

Full source

theorem monic : (minpoly G F x).Monic := by
  simp only [minpoly]
  rw [Polynomial.monic_toSubring]
  exact prodXSubSMul.monic G F x

Monicity of the Minimal Polynomial over the Fixed Subfield

Informal description

The minimal polynomial of an element $x$ in a field $F$ over the fixed subfield $\text{FixedPoints.subfield } G F$ is monic. Here, $G$ is a group acting on $F$, and $\text{FixedPoints.subfield } G F$ denotes the subfield of elements fixed by every element of $G$.

FixedPoints.minpoly.eval₂ theorem

: Polynomial.eval₂ (Subring.subtype <| (FixedPoints.subfield G F).toSubring) x (minpoly G F x) = 0

Full source

theorem eval₂ :
    Polynomial.eval₂ (Subring.subtype <| (FixedPoints.subfield G F).toSubring) x (minpoly G F x) =
      0 := by
  rw [← prodXSubSMul.eval G F x, Polynomial.eval₂_eq_eval_map]
  simp only [minpoly, Polynomial.map_toSubring]

Evaluation of Minimal Polynomial over Fixed Subfield Vanishes at $x$

Informal description

Let $G$ be a group acting on a field $F$, and let $x \in F$. The minimal polynomial of $x$ over the fixed subfield $\text{FixedPoints.subfield } G F$ evaluates to zero at $x$ when mapped through the subring inclusion of the fixed subfield into $F$. That is, $\text{eval}_2 (\text{Subring.subtype } (\text{FixedPoints.subfield } G F).\text{toSubring}) x (\text{minpoly } G F x) = 0$.

FixedPoints.minpoly.eval₂' theorem

: Polynomial.eval₂ (Subfield.subtype <| FixedPoints.subfield G F) x (minpoly G F x) = 0

Full source

theorem eval₂' :
    Polynomial.eval₂ (Subfield.subtype <| FixedPoints.subfield G F) x (minpoly G F x) = 0 :=
  eval₂ G F x

Minimal Polynomial Vanishes at $x$ over Fixed Subfield

Informal description

Let $G$ be a group acting on a field $F$, and let $x \in F$. The minimal polynomial of $x$ over the fixed subfield $\text{FixedPoints.subfield } G F$ evaluates to zero at $x$ when mapped through the subfield inclusion of the fixed subfield into $F$. That is, \[ \text{eval}_2 \left( \text{Subfield.subtype } (\text{FixedPoints.subfield } G F) \right) x \left( \text{minpoly } G F x \right) = 0. \]

FixedPoints.minpoly.ne_one theorem

: minpoly G F x ≠ (1 : Polynomial (FixedPoints.subfield G F))

Full source

theorem ne_one : minpolyminpoly G F x ≠ (1 : Polynomial (FixedPoints.subfield G F)) := fun H =>
  have := eval₂ G F x
  (one_ne_zero : (1 : F) ≠ 0) <| by rwa [H, Polynomial.eval₂_one] at this

Non-triviality of Minimal Polynomial over Fixed Subfield: $\text{minpoly}_G(F, x) \neq 1$

Informal description

For any element $x$ in a field $F$ with a group $G$ acting on it, the minimal polynomial of $x$ over the fixed subfield $\text{FixedPoints.subfield } G F$ is not equal to the constant polynomial $1$.

FixedPoints.minpoly.of_eval₂ theorem

 (f : Polynomial (FixedPoints.subfield G F))
  (hf : Polynomial.eval₂ (Subfield.subtype <| FixedPoints.subfield G F) x f = 0) : minpoly G F x ∣ f

Full source

theorem of_eval₂ (f : Polynomial (FixedPoints.subfield G F))
    (hf : Polynomial.eval₂ (Subfield.subtype <| FixedPoints.subfield G F) x f = 0) :
    minpolyminpoly G F x ∣ f := by
  classical
  rw [← Polynomial.map_dvd_map' (Subfield.subtype <| FixedPoints.subfield G F), minpoly,
    ← Subfield.toSubring_subtype_eq_subtype, Polynomial.map_toSubring _ _, prodXSubSMul]
  refine
    Fintype.prod_dvd_of_coprime
      (Polynomial.pairwise_coprime_X_sub_C <| MulAction.injective_ofQuotientStabilizer G x) fun y =>
      QuotientGroup.induction_on y fun g => ?_
  rw [Polynomial.dvd_iff_isRoot, Polynomial.IsRoot.def, MulAction.ofQuotientStabilizer_mk,
    Polynomial.eval_smul',
    ← IsInvariantSubring.coe_subtypeHom' G (FixedPoints.subfield G F).toSubring,
    ← MulSemiringActionHom.coe_polynomial, ← MulSemiringActionHom.map_smul, smul_polynomial,
    MulSemiringActionHom.coe_polynomial, IsInvariantSubring.coe_subtypeHom',
    Polynomial.eval_map, Subfield.toSubring_subtype_eq_subtype, hf, smul_zero]

Minimal Polynomial Divides Any Vanishing Polynomial over Fixed Subfield

Informal description

Let $G$ be a group acting on a field $F$, and let $x \in F$. For any polynomial $f$ with coefficients in the fixed subfield $\text{FixedPoints.subfield } G F$, if $f$ evaluates to zero at $x$ under the inclusion map of the fixed subfield into $F$, then the minimal polynomial of $x$ over the fixed subfield divides $f$.

FixedPoints.minpoly.irreducible_aux theorem

 (f g : Polynomial (FixedPoints.subfield G F)) (hf : f.Monic) (hg : g.Monic) (hfg : f * g = minpoly G F x) :
  f = 1 ∨ g = 1

Full source

theorem irreducible_aux (f g : Polynomial (FixedPoints.subfield G F)) (hf : f.Monic) (hg : g.Monic)
    (hfg : f * g = minpoly G F x) : f = 1 ∨ g = 1 := by
  have hf2 : f ∣ minpoly G F x := by rw [← hfg]; exact dvd_mul_right _ _
  have hg2 : g ∣ minpoly G F x := by rw [← hfg]; exact dvd_mul_left _ _
  have := eval₂ G F x
  rw [← hfg, Polynomial.eval₂_mul, mul_eq_zero] at this
  rcases this with this | this
  · right
    have hf3 : f = minpoly G F x :=
      Polynomial.eq_of_monic_of_associated hf (monic G F x)
        (associated_of_dvd_dvd hf2 <| @of_eval₂ G _ F _ _ _ x f this)
    rwa [← mul_one (minpoly G F x), hf3, mul_right_inj' (monic G F x).ne_zero] at hfg
  · left
    have hg3 : g = minpoly G F x :=
      Polynomial.eq_of_monic_of_associated hg (monic G F x)
        (associated_of_dvd_dvd hg2 <| @of_eval₂ G _ F _ _ _ x g this)
    rwa [← one_mul (minpoly G F x), hg3, mul_left_inj' (monic G F x).ne_zero] at hfg

Irreducibility Criterion for Minimal Polynomial over Fixed Subfield

Informal description

Let $G$ be a group acting on a field $F$, and let $x \in F$. For any monic polynomials $f$ and $g$ with coefficients in the fixed subfield $\text{FixedPoints.subfield } G F$, if their product $f \cdot g$ equals the minimal polynomial of $x$ over the fixed subfield, then either $f = 1$ or $g = 1$.

FixedPoints.minpoly.irreducible theorem

: Irreducible (minpoly G F x)

Full source

theorem irreducible : Irreducible (minpoly G F x) :=
  (Polynomial.irreducible_of_monic (monic G F x) (ne_one G F x)).2 (irreducible_aux G F x)

Irreducibility of Minimal Polynomial over Fixed Subfield under Group Action

Informal description

Let $G$ be a group acting on a field $F$. For any element $x \in F$, the minimal polynomial of $x$ over the fixed subfield $\text{FixedPoints.subfield } G F$ is irreducible in the polynomial ring over this fixed subfield.

FixedPoints.isIntegral theorem

[Finite G] (x : F) : IsIntegral (FixedPoints.subfield G F) x

Full source

theorem isIntegral [Finite G] (x : F) : IsIntegral (FixedPoints.subfield G F) x := by
  cases nonempty_fintype G; exact ⟨minpoly G F x, minpoly.monic G F x, minpoly.eval₂ G F x⟩

Integrality of Field Elements over Fixed Subfield under Finite Group Action

Informal description

Let $G$ be a finite group acting on a field $F$. For any element $x \in F$, $x$ is integral over the fixed subfield $\text{FixedPoints.subfield } G F$, i.e., there exists a monic polynomial with coefficients in $\text{FixedPoints.subfield } G F$ that has $x$ as a root.

FixedPoints.minpoly_eq_minpoly theorem

: minpoly G F x = _root_.minpoly (FixedPoints.subfield G F) x

Full source

theorem minpoly_eq_minpoly : minpoly G F x = _root_.minpoly (FixedPoints.subfield G F) x :=
  minpoly.eq_of_irreducible_of_monic (minpoly.irreducible G F x) (minpoly.eval₂ G F x)
    (minpoly.monic G F x)

Equality of Minimal Polynomials over Fixed Subfield under Group Action

Informal description

Let $G$ be a group acting on a field $F$. For any element $x \in F$, the minimal polynomial of $x$ over the fixed subfield $\text{FixedPoints.subfield } G F$ is equal to the minimal polynomial of $x$ over this fixed subfield in the usual sense (denoted by $\_root\_.\text{minpoly}$).

FixedPoints.rank_le_card theorem

: Module.rank (FixedPoints.subfield G F) F ≤ Fintype.card G

Full source

theorem rank_le_card : Module.rank (FixedPoints.subfield G F) F ≤ Fintype.card G :=
  rank_le fun s hs => by
    simpa only [rank_fun', Cardinal.mk_coe_finset, Finset.coe_sort_coe, Cardinal.lift_natCast,
      Nat.cast_le] using
      (linearIndependent_smul_of_linearIndependent G F hs).cardinal_lift_le_rank

Rank Bound for Field over Fixed Subfield: $\text{rank}_{F^G} F \leq |G|$

Informal description

Let $G$ be a finite group acting on a field $F$. Then the rank of $F$ as a module over the fixed subfield $\text{FixedPoints.subfield } G F$ is bounded by the cardinality of $G$, i.e., \[ \text{rank}_{\text{FixedPoints.subfield } G F} F \leq |G|. \]

FixedPoints.normal instance

: Normal (FixedPoints.subfield G F) F

Full source

instance normal : Normal (FixedPoints.subfield G F) F where
  isAlgebraic x := (isIntegral G F x).isAlgebraic
  splits' x :=
    (Polynomial.splits_id_iff_splits _).1 <| by
      cases nonempty_fintype G
      rw [← minpoly_eq_minpoly, minpoly, coe_algebraMap, ← Subfield.toSubring_subtype_eq_subtype,
        Polynomial.map_toSubring _ (subfield G F).toSubring, prodXSubSMul]
      exact Polynomial.splits_prod _ fun _ _ => Polynomial.splits_X_sub_C _

Normality of Field Extension over Fixed Subfield under Group Action

Informal description

For any group $G$ acting on a field $F$, the field extension $F$ over the fixed subfield $\text{FixedPoints.subfield } G F$ is normal. This means that every element of $F$ is algebraic over the fixed subfield and its minimal polynomial splits completely in $F$.

FixedPoints.isSeparable instance

: Algebra.IsSeparable (FixedPoints.subfield G F) F

Full source

instance isSeparable : Algebra.IsSeparable (FixedPoints.subfield G F) F := by
  classical
  exact ⟨fun x => by
    cases nonempty_fintype G
    rw [IsSeparable, ← minpoly_eq_minpoly,
      ← Polynomial.separable_map (FixedPoints.subfield G F).subtype, minpoly,
      ← Subfield.toSubring_subtype_eq_subtype, Polynomial.map_toSubring _ (subfield G F).toSubring]
    exact Polynomial.separable_prod_X_sub_C_iff.2 (injective_ofQuotientStabilizer G x)⟩

Separability of Field Extension over Fixed Subfield under Group Action

Informal description

For any group $G$ acting on a field $F$, the field extension $F$ over the fixed subfield $\text{FixedPoints.subfield } G F$ is separable.

FixedPoints.instFiniteDimensionalSubtypeMemSubfieldSubfield instance

: FiniteDimensional (subfield G F) F

Full source

instance : FiniteDimensional (subfield G F) F := by
  cases nonempty_fintype G
  exact IsNoetherian.iff_fg.1
      (IsNoetherian.iff_rank_lt_aleph0.2 <| (rank_le_card G F).trans_lt <| Cardinal.nat_lt_aleph0 _)

Finite-Dimensionality of Field Extension over Fixed Subfield under Group Action

Informal description

For any group $G$ acting on a field $F$, the field extension $F$ over the fixed subfield $\text{FixedPoints.subfield } G F$ is finite-dimensional.

FixedPoints.finrank_le_card theorem

[Fintype G] : finrank (subfield G F) F ≤ Fintype.card G

Full source

theorem finrank_le_card [Fintype G] : finrank (subfield G F) F ≤ Fintype.card G := by
  rw [← @Nat.cast_le Cardinal, finrank_eq_rank]
  apply rank_le_card

Finite dimension bound for field extension over fixed subfield: $\text{finrank}_{F^G} F \leq |G|$

Informal description

Let $G$ be a finite group acting on a field $F$. Then the finite dimension of $F$ as a vector space over the fixed subfield $\text{FixedPoints.subfield } G F$ is bounded by the cardinality of $G$, i.e., \[ \text{finrank}_{\text{FixedPoints.subfield } G F} F \leq |G|. \]

linearIndependent_toLinearMap theorem

 (R : Type u) (A : Type v) (B : Type w) [CommSemiring R] [Semiring A] [Algebra R A] [CommRing B] [IsDomain B]
  [Algebra R B] : LinearIndependent B (AlgHom.toLinearMap : (A →ₐ[R] B) → A →ₗ[R] B)

Full source

theorem linearIndependent_toLinearMap (R : Type u) (A : Type v) (B : Type w) [CommSemiring R]
    [Semiring A] [Algebra R A] [CommRing B] [IsDomain B] [Algebra R B] :
    LinearIndependent B (AlgHom.toLinearMap : (A →ₐ[R] B) → A →ₗ[R] B) :=
  have : LinearIndependent B (LinearMap.ltoFunLinearMap.ltoFun R A B ∘ AlgHom.toLinearMap) :=
    ((linearIndependent_monoidHom A B).comp ((↑) : (A →ₐ[R] B) → A →* B) fun _ _ hfg =>
        AlgHom.ext fun _ => DFunLike.ext_iff.1 hfg _ :
      _)
  this.of_comp _

Linear Independence of Algebra Homomorphisms as Linear Maps

Informal description

Let $R$ be a commutative semiring, $A$ a semiring with an $R$-algebra structure, and $B$ a commutative domain with an $R$-algebra structure. Then the set of algebra homomorphisms from $A$ to $B$, when viewed as linear maps via the canonical embedding $\text{AlgHom.toLinearMap}$, is linearly independent over $B$.

cardinalMk_algHom theorem

 (K : Type u) (V : Type v) (W : Type w) [Field K] [Ring V] [Algebra K V] [FiniteDimensional K V] [Field W]
  [Algebra K W] : Cardinal.mk (V →ₐ[K] W) ≤ finrank W (V →ₗ[K] W)

Full source

theorem cardinalMk_algHom (K : Type u) (V : Type v) (W : Type w) [Field K] [Ring V] [Algebra K V]
    [FiniteDimensional K V] [Field W] [Algebra K W] :
    Cardinal.mk (V →ₐ[K] W) ≤ finrank W (V →ₗ[K] W) :=
  (linearIndependent_toLinearMap K V W).cardinalMk_le_finrank

Cardinality Bound for Algebra Homomorphisms in Finite Extensions

Informal description

Let $K$ be a field, $V$ a finite-dimensional $K$-algebra, and $W$ a field extension of $K$. Then the cardinality of the set of $K$-algebra homomorphisms from $V$ to $W$ is bounded by the dimension of the $W$-vector space of $K$-linear maps from $V$ to $W$, i.e., \[ \#(V \to_{K\text{-alg}} W) \leq \dim_W (V \to_{K\text{-lin}} W). \]

AlgEquiv.fintype instance

(K : Type u) (V : Type v) [Field K] [Field V] [Algebra K V] [FiniteDimensional K V] : Fintype (V ≃ₐ[K] V)

Full source

noncomputable instance AlgEquiv.fintype (K : Type u) (V : Type v) [Field K] [Field V] [Algebra K V]
    [FiniteDimensional K V] : Fintype (V ≃ₐ[K] V) :=
  Fintype.ofEquiv (V →ₐ[K] V) (algEquivEquivAlgHom K V).symm

Finiteness of Algebra Automorphisms in Finite Field Extensions

Informal description

For any field extension $V$ of $K$ that is finite-dimensional as a $K$-vector space, the set of $K$-algebra automorphisms of $V$ (i.e., $K$-algebra isomorphisms from $V$ to itself) is finite.

finrank_algHom theorem

 (K : Type u) (V : Type v) [Field K] [Field V] [Algebra K V] [FiniteDimensional K V] :
  Fintype.card (V →ₐ[K] V) ≤ finrank V (V →ₗ[K] V)

Full source

theorem finrank_algHom (K : Type u) (V : Type v) [Field K] [Field V] [Algebra K V]
    [FiniteDimensional K V] : Fintype.card (V →ₐ[K] V) ≤ finrank V (V →ₗ[K] V) :=
  (linearIndependent_toLinearMap K V V).fintype_card_le_finrank

Cardinality Bound for Algebra Endomorphisms in Finite Field Extensions

Informal description

Let $K$ be a field and $V$ a finite-dimensional field extension of $K$. Then the number of $K$-algebra homomorphisms from $V$ to itself is bounded by the dimension of $V$ as a vector space over $K$ of the space of $K$-linear maps from $V$ to itself, i.e., $$ |V \to_{\text{Alg}[K]} V| \leq \dim_V (V \to_{\text{Lin}[K]} V). $$

AlgHom.card_le theorem

 {F K : Type*} [Field F] [Field K] [Algebra F K] [FiniteDimensional F K] : Fintype.card (K →ₐ[F] K) ≤ Module.finrank F K

Full source

theorem AlgHom.card_le {F K : Type*} [Field F] [Field K] [Algebra F K] [FiniteDimensional F K] :
    Fintype.card (K →ₐ[F] K) ≤ Module.finrank F K :=
  Module.finrank_linearMap_self F K K ▸ finrank_algHom F K

Cardinality Bound for Algebra Homomorphisms in Finite Field Extensions: $|\text{Hom}_F(K, K)| \leq \dim_F K$

Informal description

Let $F$ be a field and $K$ a finite-dimensional field extension of $F$. Then the number of $F$-algebra homomorphisms from $K$ to itself is bounded by the dimension of $K$ as a vector space over $F$, i.e., $$|\text{Hom}_F(K, K)| \leq \dim_F K.$$

AlgEquiv.card_le theorem

 {F K : Type*} [Field F] [Field K] [Algebra F K] [FiniteDimensional F K] : Fintype.card (K ≃ₐ[F] K) ≤ Module.finrank F K

Full source

theorem AlgEquiv.card_le {F K : Type*} [Field F] [Field K] [Algebra F K] [FiniteDimensional F K] :
    Fintype.card (K ≃ₐ[F] K) ≤ Module.finrank F K :=
  Fintype.ofEquiv_card (algEquivEquivAlgHom F K).toEquiv.symm ▸ AlgHom.card_le

Cardinality Bound for Algebra Automorphisms in Finite Field Extensions: $|\text{Aut}_F(K)| \leq \dim_F K$

Informal description

Let $F$ be a field and $K$ a finite-dimensional field extension of $F$. Then the number of $F$-algebra automorphisms of $K$ is bounded by the dimension of $K$ as a vector space over $F$, i.e., \[ |\text{Aut}_F(K)| \leq \dim_F K. \]

FixedPoints.finrank_eq_card theorem

[Fintype G] [FaithfulSMul G F] : finrank (FixedPoints.subfield G F) F = Fintype.card G

Full source

/-- Let $F$ be a field. Let $G$ be a finite group acting faithfully on $F$.
Then $[F : F^G] = |G|$. -/
@[stacks 09I3 "second part"]
theorem finrank_eq_card [Fintype G] [FaithfulSMul G F] :
    finrank (FixedPoints.subfield G F) F = Fintype.card G :=
  le_antisymm (FixedPoints.finrank_le_card G F) <|
    calc
      Fintype.card G ≤ Fintype.card (F →ₐ[FixedPoints.subfield G F] F) :=
        Fintype.card_le_of_injective _ (MulSemiringAction.toAlgHom_injective _ F)
      _ ≤ finrank F (F →ₗ[FixedPoints.subfield G F] F) := finrank_algHom (subfield G F) F
      _ = finrank (FixedPoints.subfield G F) F := finrank_linearMap_self _ _ _

Fundamental Theorem of Galois Theory: Dimension Formula for Fixed Field Extension

Informal description

Let $F$ be a field with a faithful action by a finite group $G$. Then the dimension of $F$ as a vector space over its fixed subfield $F^G$ is equal to the order of $G$, i.e., \[ [F : F^G] = |G|. \]

FixedPoints.toAlgHom_bijective theorem

[Finite G] [FaithfulSMul G F] : Function.Bijective (MulSemiringAction.toAlgHom _ _ : G → F →ₐ[subfield G F] F)

Full source

/-- `MulSemiringAction.toAlgHom` is bijective. -/
theorem toAlgHom_bijective [Finite G] [FaithfulSMul G F] :
    Function.Bijective (MulSemiringAction.toAlgHom _ _ : G → F →ₐ[subfield G F] F) := by
  cases nonempty_fintype G
  rw [Fintype.bijective_iff_injective_and_card]
  constructor
  · exact MulSemiringAction.toAlgHom_injective _ F
  · apply le_antisymm
    · exact Fintype.card_le_of_injective _ (MulSemiringAction.toAlgHom_injective _ F)
    · rw [← finrank_eq_card G F]
      exact LE.le.trans_eq (finrank_algHom _ F) (finrank_linearMap_self _ _ _)

Bijectivity of Group Action to Algebra Homomorphisms in Galois Theory

Informal description

Let $G$ be a finite group acting faithfully on a field $F$. Then the map \[ G \to \mathrm{Hom}_{\text{Alg}}(F, F) \] sending each group element $g \in G$ to its corresponding algebra homomorphism is bijective. Here $\mathrm{Hom}_{\text{Alg}}(F, F)$ denotes the set of algebra homomorphisms from $F$ to itself over the fixed subfield $F^G$.

FixedPoints.toAlgHomEquiv definition

[Finite G] [FaithfulSMul G F] : G ≃ (F →ₐ[FixedPoints.subfield G F] F)

Full source

/-- Bijection between `G` and algebra endomorphisms of `F` that fix the fixed points. -/
def toAlgHomEquiv [Finite G] [FaithfulSMul G F] : G ≃ (F →ₐ[FixedPoints.subfield G F] F) :=
  Equiv.ofBijective _ (toAlgHom_bijective G F)

Bijection between group elements and fixed-point-preserving algebra homomorphisms

Informal description

Given a finite group $ G $ acting faithfully on a field $ F $, there is a bijective correspondence between the elements of $ G $ and the algebra homomorphisms from $ F $ to itself that fix the subfield $ F^G $ of elements fixed by $ G $. This correspondence is given by the map that sends each group element $ g \in G $ to its induced algebra homomorphism $ F \to F $ over the fixed subfield $ F^G $.

FixedPoints.toAlgAut_bijective theorem

[Finite G] [FaithfulSMul G F] : Function.Bijective (MulSemiringAction.toAlgAut G (FixedPoints.subfield G F) F)

Full source

/-- `MulSemiringAction.toAlgAut` is bijective. -/
theorem toAlgAut_bijective [Finite G] [FaithfulSMul G F] :
    Function.Bijective (MulSemiringAction.toAlgAut G (FixedPoints.subfield G F) F) := by
  refine ⟨fun _ _ h ↦ (FixedPoints.toAlgHom_bijective G F).injective ?_,
    fun f ↦ ((FixedPoints.toAlgHom_bijective G F).surjective f).imp (fun _ h ↦ ?_)⟩ <;>
      rwa [DFunLike.ext_iff] at h ⊢

Bijectivity of Group Action to Algebra Automorphisms in Galois Theory

Informal description

Let $G$ be a finite group acting faithfully on a field $F$. Then the map \[ G \to \mathrm{Aut}_{F^G}(F) \] that sends each group element $g \in G$ to its corresponding $F^G$-algebra automorphism of $F$ is bijective. Here $F^G$ denotes the fixed subfield of $F$ under the action of $G$, and $\mathrm{Aut}_{F^G}(F)$ denotes the group of $F^G$-algebra automorphisms of $F$.

FixedPoints.toAlgAutMulEquiv definition

[Finite G] [FaithfulSMul G F] : G ≃* (F ≃ₐ[FixedPoints.subfield G F] F)

Full source

/-- Bijection between `G` and algebra automorphisms of `F` that fix the fixed points. -/
def toAlgAutMulEquiv [Finite G] [FaithfulSMul G F] : G ≃* (F ≃ₐ[FixedPoints.subfield G F] F) :=
  MulEquiv.ofBijective _ (toAlgAut_bijective G F)

Group isomorphism between $ G $ and $ F^G $-algebra automorphisms of $ F $

Informal description

Given a finite group $ G $ acting faithfully on a field $ F $, there is a multiplicative equivalence (isomorphism) between $ G $ and the group of $ F^G $-algebra automorphisms of $ F $, where $ F^G $ denotes the subfield of $ F $ fixed by every element of $ G $. This equivalence maps each group element $ g \in G $ to its corresponding automorphism of $ F $ that fixes $ F^G $, and it is bijective (as established by `toAlgAut_bijective`).

FixedPoints.toAlgAut_surjective theorem

[Finite G] : Function.Surjective (MulSemiringAction.toAlgAut G (FixedPoints.subfield G F) F)

Full source

/-- `MulSemiringAction.toAlgAut` is surjective. -/
theorem toAlgAut_surjective [Finite G] :
    Function.Surjective (MulSemiringAction.toAlgAut G (FixedPoints.subfield G F) F) := by
  let f : G →* F ≃ₐ[FixedPoints.subfield G F] F :=
    MulSemiringAction.toAlgAut G (FixedPoints.subfield G F) F
  let Q := G ⧸ f.ker
  let _ : MulSemiringAction Q F := MulSemiringAction.compHom _ (QuotientGroup.kerLift f)
  have : FaithfulSMul Q F := ⟨by
    intro q₁ q₂
    refine Quotient.inductionOn₂' q₁ q₂ (fun g₁ g₂ h ↦ QuotientGroup.eq.mpr ?_)
    rwa [MonoidHom.mem_ker, map_mul, map_inv, inv_mul_eq_one, AlgEquiv.ext_iff]⟩
  intro f
  obtain ⟨q, hq⟩ := (toAlgAut_bijective Q F).surjective
    (AlgEquiv.ofRingEquiv (f := f) (fun ⟨x, hx⟩ ↦ f.commutes' ⟨x, fun g ↦ hx g⟩))
  revert hq
  refine QuotientGroup.induction_on q (fun g hg ↦ ⟨g, ?_⟩)
  rwa [AlgEquiv.ext_iff] at hg ⊢

Surjectivity of Group Action to Algebra Automorphisms in Galois Theory

Informal description

Let $G$ be a finite group acting on a field $F$. Then the homomorphism \[ G \to \mathrm{Aut}_{F^G}(F), \] which sends each group element $g \in G$ to its corresponding $F^G$-algebra automorphism of $F$, is surjective. Here $F^G$ denotes the fixed subfield of $F$ under the action of $G$, and $\mathrm{Aut}_{F^G}(F)$ denotes the group of $F^G$-algebra automorphisms of $F$.

Main Definitions