NYLL
Module

PrimaryRootsFiniteness.lean

Nyll.GaloisCohomology.Kummer.Concrete.PrimaryRootsFiniteness
2 declarations indexed from sourceView source ↗

Module documentation

Transport of finite primary roots along field embeddings

Primary roots embed through the actual map on units. A finite extension embedded in a chosen overfield is identified with its actual intermediate field range.

Imports3
  • Mathlib.FieldTheory.IntermediateField.Basic
  • Mathlib.LinearAlgebra.FiniteDimensional.Basic
  • Mathlib.GroupTheory.Torsion
Imported by3

Declarations

theorem

finite_primaryComponent_of_fieldEmbedding

L23 ↗
KummerTheory.finite_primaryComponent_of_fieldEmbedding
Documentation

Primary roots of a subfield inject into those of the ambient field.

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace KummerTheory
universe u v w
Lean source · statement
theorem finite_primaryComponent_of_fieldEmbedding
    {E : Type u} {F : Type v} [Field E] [Field F] (f : E →+* F)
    (p : ℕ) [Finite (CommGroup.primaryComponent Fˣ p)] :
    Finite (CommGroup.primaryComponent Eˣ p)
theorem

finite_primaryComponent_of_finiteExtension_embedding

L41 ↗
KummerTheory.finite_primaryComponent_of_finiteExtension_embedding
Documentation

Root finiteness on finite intermediate fields applies to any embedded finite extension.

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace KummerTheory
universe u v w
Lean source · statement
theorem finite_primaryComponent_of_finiteExtension_embedding
    {K : Type u} {E : Type v} {Ω : Type w}
    [Field K] [Field E] [Field Ω] [Algebra K E] [Algebra K Ω]
    [FiniteDimensional K E] (f : E →ₐ[K] Ω) (p : ℕ)
    (hRoots : ∀ L : IntermediateField K Ω, FiniteDimensional K L →
      Finite (CommGroup.primaryComponent Lˣ p)) :
    Finite (CommGroup.primaryComponent Eˣ p)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.