Module

InfiniteInverse.lean

Nyll.GaloisCohomology.Kummer.Concrete.InfiniteInverse

9 declarations indexed from sourceView source ↗

Module documentation

infinite inverse inclusion

Any radical appearing in K(√[n]{Δ}) uses only finitely many of the adjoined roots. The corresponding admissible finite-support subgroup Δ₀ ≤ Δ gives a finite Galois Kummer stage. Applying the finite inverse theorem at that stage shows that the original radical already belongs to Δ₀, hence to Δ.

Imports2

Imported by3

def

finiteSupportField

L35 ↗

KummerTheory.finiteSupportField

Documentation

The finite field generated by the selected radical roots.

Source context 5 commands

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

noncomputable section
namespace KummerTheory
variable {K Omega : Type*} [Field K] [Field Omega] [Algebra K Omega]
section FiniteSupportField
variable (n : ℕ+) (Delta : KummerSubgroup K n) (T : Finset Omega)
  (hT : (T : Set Omega) ⊆
    kummerRootSet (K := K) (Omega := Omega) n Delta.1)

Lean source · statement

def finiteSupportField : IntermediateField K Omega

theorem

admissibleFiniteSupportSubgroup_le_finiteKummerRadicalSubgroup

L40 ↗

KummerTheory.admissibleFiniteSupportSubgroup_le_finiteKummerRadicalSubgroup

Documentation

The admissible finite-support subgroup has all of its prescribed roots in the field generated by T.

Source context 5 commands

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

noncomputable section
namespace KummerTheory
variable {K Omega : Type*} [Field K] [Field Omega] [Algebra K Omega]
section FiniteSupportField
variable (n : ℕ+) (Delta : KummerSubgroup K n) (T : Finset Omega)
  (hT : (T : Set Omega) ⊆
    kummerRootSet (K := K) (Omega := Omega) n Delta.1)

Lean source · statement

theorem admissibleFiniteSupportSubgroup_le_finiteKummerRadicalSubgroup :
    (admissibleFiniteSupportSubgroup
      (K := K) (Omega := Omega) n Delta T hT).1 ≤
      finiteKummerRadicalSubgroup
        (K := K) (L := finiteSupportField (K := K) T) n

theorem

finiteSupportField_finiteDimensional

L71 ↗

KummerTheory.finiteSupportField_finiteDimensional

Documentation

A finite set of integral radical roots generates a finite-dimensional extension.

Source context 5 commands

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

noncomputable section
namespace KummerTheory
variable {K Omega : Type*} [Field K] [Field Omega] [Algebra K Omega]
section FiniteSupportField
variable (n : ℕ+) (Delta : KummerSubgroup K n) (T : Finset Omega)
  (hT : (T : Set Omega) ⊆
    kummerRootSet (K := K) (Omega := Omega) n Delta.1)

Lean source · statement

theorem finiteSupportField_finiteDimensional :
    ((T : Set Omega) ⊆
      kummerRootSet (K := K) (Omega := Omega) n Delta.1) →
      FiniteDimensional K (finiteSupportField (K := K) T)

theorem

kummerRootSet_admissibleFiniteSupport_subset

L86 ↗

KummerTheory.kummerRootSet_admissibleFiniteSupport_subset

Documentation

Every global root belonging to the finite-support subgroup already lies in the field generated by T. The ratio with a root in that field is an n-th root of unity and hence lies in K.

Source context 5 commands

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

noncomputable section
namespace KummerTheory
variable {K Omega : Type*} [Field K] [Field Omega] [Algebra K Omega]
section FiniteSupportField
variable (n : ℕ+) (Delta : KummerSubgroup K n) (T : Finset Omega)
  (hT : (T : Set Omega) ⊆
    kummerRootSet (K := K) (Omega := Omega) n Delta.1)

Lean source · statement

theorem kummerRootSet_admissibleFiniteSupport_subset
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) :
    kummerRootSet (K := K) (Omega := Omega) n
        (admissibleFiniteSupportSubgroup
          (K := K) (Omega := Omega) n Delta T hT).1 ≤
      finiteSupportField (K := K) T

theorem

kummerRadicalExtension_admissibleFiniteSupport_eq

L130 ↗

KummerTheory.kummerRadicalExtension_admissibleFiniteSupport_eq

Documentation

The full radical extension attached to the finite-support subgroup is exactly the field generated by the selected roots.

Source context 5 commands

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

noncomputable section
namespace KummerTheory
variable {K Omega : Type*} [Field K] [Field Omega] [Algebra K Omega]
section FiniteSupportField
variable (n : ℕ+) (Delta : KummerSubgroup K n) (T : Finset Omega)
  (hT : (T : Set Omega) ⊆
    kummerRootSet (K := K) (Omega := Omega) n Delta.1)

Lean source · statement

theorem kummerRadicalExtension_admissibleFiniteSupport_eq
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) :
    kummerRadicalExtension (K := K) (Omega := Omega) n
        (admissibleFiniteSupportSubgroup
          (K := K) (Omega := Omega) n Delta T hT).1 =
      finiteSupportField (K := K) T

theorem

finiteSupportField_isGalois

L145 ↗

KummerTheory.finiteSupportField_isGalois

Documentation

Over a separable closure, the finite-support field is Galois.

Source context 5 commands

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

noncomputable section
namespace KummerTheory
variable {K Omega : Type*} [Field K] [Field Omega] [Algebra K Omega]
section FiniteSupportField
variable (n : ℕ+) (Delta : KummerSubgroup K n) (T : Finset Omega)
  (hT : (T : Set Omega) ⊆
    kummerRootSet (K := K) (Omega := Omega) n Delta.1)

Lean source · statement

theorem finiteSupportField_isGalois
    [IsSepClosure K Omega]
    (hT' : (T : Set Omega) ⊆
      kummerRootSet (K := K) (Omega := Omega) n Delta.1)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) :
    IsGalois K (finiteSupportField (K := K) T)

theorem

finiteSupportField_internalRoots_adjoin_eq_top

L158 ↗

KummerTheory.finiteSupportField_internalRoots_adjoin_eq_top

Documentation

The internal Kummer root set of the finite-support subgroup generates the finite-support field.

Source context 5 commands

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

noncomputable section
namespace KummerTheory
variable {K Omega : Type*} [Field K] [Field Omega] [Algebra K Omega]
section FiniteSupportField
variable (n : ℕ+) (Delta : KummerSubgroup K n) (T : Finset Omega)
  (hT : (T : Set Omega) ⊆
    kummerRootSet (K := K) (Omega := Omega) n Delta.1)

Lean source · statement

theorem finiteSupportField_internalRoots_adjoin_eq_top :
    IntermediateField.adjoin K
      (kummerRootSet
        (K := K) (Omega := finiteSupportField (K := K) T) n
        (admissibleFiniteSupportSubgroup
          (K := K) (Omega := Omega) n Delta T hT).1) = ⊤

theorem

finiteKummerRadicalSubgroup_kummerRadicalExtension_le

L198 ↗

KummerTheory.finiteKummerRadicalSubgroup_kummerRadicalExtension_le

Documentation

the Kummer correspondence, inverse inclusion for an arbitrary admissible subgroup. Any base-field radical in K(√[n]{Delta}) is already in Delta. The root is first descended to a finite-support Kummer stage, where the finite inverse theorem applies.

Source context 5 commands

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

noncomputable section
namespace KummerTheory
variable {K Omega : Type*} [Field K] [Field Omega] [Algebra K Omega]
section InfiniteInverse
variable [IsSepClosure K Omega]

Lean source · statement

theorem finiteKummerRadicalSubgroup_kummerRadicalExtension_le
    (n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (Delta : KummerSubgroup K n) :
    finiteKummerRadicalSubgroup
        (K := K)
        (L := kummerRadicalExtension
          (K := K) (Omega := Omega) n Delta.1) n ≤
      Delta.1

theorem

finiteKummerRadicalSubgroup_kummerRadicalExtension_eq

L251 ↗

KummerTheory.finiteKummerRadicalSubgroup_kummerRadicalExtension_eq

Documentation

the Kummer correspondence, subgroup round trip. Under the standard characteristic and roots-of-unity hypotheses, adjoining all prescribed radicals and then taking the actual radical subgroup recovers Delta.

Source context 5 commands

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

noncomputable section
namespace KummerTheory
variable {K Omega : Type*} [Field K] [Field Omega] [Algebra K Omega]
section InfiniteInverse
variable [IsSepClosure K Omega]

Lean source · statement

theorem finiteKummerRadicalSubgroup_kummerRadicalExtension_eq
    (n : ℕ+) (hn : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (Delta : KummerSubgroup K n) :
    finiteKummerRadicalSubgroup
        (K := K)
        (L := kummerRadicalExtension
          (K := K) (Omega := Omega) n Delta.1) n =
      Delta.1

Module documentation

infinite inverse inclusion

Declarations