NYLL
Module

FixedSubgroupCharacterDescent.lean

Nyll.GaloisCohomology.Kummer.Concrete.FixedSubgroupCharacterDescent
3 declarations indexed from sourceView source ↗

Module documentation

Descent of invariant absolute Galois characters

Transport an absolute character of a finite normal intermediate field to its actual fixing subgroup. The established comparison of conjugation actions preserves invariance. Transfer divided by the extension degree then extends the character whenever that degree is coprime to its coefficient modulus.

Imports11
Imported by3

Declarations

def

fixingSubgroupAbsoluteCharacter

L39 ↗
KummerTheory.fixingSubgroupAbsoluteCharacter
Documentation

Pull back an absolute character along the actual comparison from the fixing subgroup to the absolute Galois group of the intermediate field.

Source context 4 commands

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

namespace KummerTheory
open ProCGroups.Abelian
variable {K Ω : Type*} [Field K] [Field Ω] [Algebra K Ω] [IsAlgClosure K Ω]
  (L : IntermediateField K Ω) [FiniteDimensional K L]
attribute [local instance] closureOverIntermediate
Lean source · statement
def fixingSubgroupAbsoluteCharacter
    {A : Type*} [CommGroup A] [TopologicalSpace A]
    (f : Gal(AlgebraicClosure L/L) →ₜ* A) : L.fixingSubgroup →ₜ* A
theorem

fixingSubgroupAbsoluteCharacter_conjNormal

L52 ↗
KummerTheory.fixingSubgroupAbsoluteCharacter_conjNormal
Documentation

Invariance under all relative field automorphisms gives invariance under actual ambient conjugation on the fixing subgroup.

Source context 6 commands

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

namespace KummerTheory
open ProCGroups.Abelian
variable {K Ω : Type*} [Field K] [Field Ω] [Algebra K Ω] [IsAlgClosure K Ω]
  (L : IntermediateField K Ω) [FiniteDimensional K L]
attribute [local instance] closureOverIntermediate
variable [Normal K L]
attribute [local instance] fixingSubgroup_normal
Lean source · statement
theorem fixingSubgroupAbsoluteCharacter_conjNormal
    {A : Type*} [CommGroup A] [TopologicalSpace A] [T1Space A]
    (f : Gal(AlgebraicClosure L/L) →ₜ* A)
    (hinv : ∀ (δ : Gal(L/K)) (σ : Gal(AlgebraicClosure L/L)),
      f (absoluteGaloisConjugate δ.toRingEquiv σ) = f σ)
    (g : Gal(Ω/K)) (σ : L.fixingSubgroup) :
    fixingSubgroupAbsoluteCharacter L f (MulAut.conjNormal g σ) =
      fixingSubgroupAbsoluteCharacter L f σ
theorem

exists_character_extension_of_coprime_finrank

L78 ↗
KummerTheory.exists_character_extension_of_coprime_finrank
Documentation

An invariant absolute character extends to the actual ambient Galois group when its modulus is coprime to the finite separable extension degree.

Source context 6 commands

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

namespace KummerTheory
open ProCGroups.Abelian
variable {K Ω : Type*} [Field K] [Field Ω] [Algebra K Ω] [IsAlgClosure K Ω]
  (L : IntermediateField K Ω) [FiniteDimensional K L]
attribute [local instance] closureOverIntermediate
variable [Normal K L]
attribute [local instance] fixingSubgroup_normal
Lean source · statement
theorem exists_character_extension_of_coprime_finrank [Algebra.IsSeparable K L]
    (n : ℕ) (hdegree : (Module.finrank K L).Coprime n)
    (f : Gal(AlgebraicClosure L/L) →ₜ* Multiplicative (ZMod n))
    (hinv : ∀ (δ : Gal(L/K)) (σ : Gal(AlgebraicClosure L/L)),
      f (absoluteGaloisConjugate δ.toRingEquiv σ) = f σ) :
    ∃ ψ : Gal(Ω/K) →ₜ* Multiplicative (ZMod n),
      ∀ σ : L.fixingSubgroup, ψ (σ : Gal(Ω/K)) =
        f (absoluteGaloisClosureEquiv L Ω (fixingSubgroupContinuousEquiv L σ))

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