Module

GaloisClosureConjugation.lean

Nyll.GaloisCohomology.Kummer.Concrete.GaloisClosureConjugation

4 declarations indexed from sourceView source ↗

Module documentation

Comparing conjugation with the canonical absolute Galois action

Changing the algebraic closure intertwines concrete semilinear conjugation with the canonical action on topological abelianization. Both the closure equivalence and the comparison are constructed from the given field data.

Imports8

Imported by9

theorem

galoisClosureTransport_abelianization_conjugation_mk

L32 ↗

KummerTheory.galoisClosureTransport_abelianization_conjugation_mk

Documentation

On quotient representatives, transport of any actual lift agrees with the canonical action defined using the selected algebraic closure.

Source context 3 commands

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

namespace KummerTheory
open ProCGroups.Abelian
variable {K Ω : Type*} [Field K] [Field Ω] [Algebra K Ω]

Lean source · statement

theorem galoisClosureTransport_abelianization_conjugation_mk
    (e : Ω ≃ₐ[K] AlgebraicClosure K) (τ : K ≃+* K) (a : Ω ≃+* Ω)
    (ha : ∀ k : K, a (algebraMap K Ω k) = algebraMap K Ω (τ k))
    (σ : Gal(Ω/K)) :
    TopologicalAbelianization.congr (galoisClosureTransport e)
        (TopologicalAbelianization.mk Gal(Ω/K) (semilinearGaloisConjugate τ a ha σ)) =
      absoluteGaloisAbelianizationAction τ
        (TopologicalAbelianization.congr (galoisClosureTransport e)
          (TopologicalAbelianization.mk Gal(Ω/K) σ))

def

absoluteGaloisClosureEquiv

L59 ↗

KummerTheory.absoluteGaloisClosureEquiv

Documentation

The relative Galois group of any algebraic closure is continuously isomorphic to the absolute Galois group defined using AlgebraicClosure.

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 Ω]
variable (K Ω) [IsAlgClosure K Ω]

Lean source · statement

def absoluteGaloisClosureEquiv :
    Gal(Ω/K) ≃ₜ* Gal(AlgebraicClosure K/K)

def

absoluteGaloisClosureAbelianizationEquiv

L64 ↗

KummerTheory.absoluteGaloisClosureAbelianizationEquiv

Documentation

The corresponding continuous comparison on topological abelianization.

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 Ω]
variable (K Ω) [IsAlgClosure K Ω]

Lean source · statement

def absoluteGaloisClosureAbelianizationEquiv :
    _root_.TopologicalAbelianization Gal(Ω/K) ≃ₜ*
      _root_.TopologicalAbelianization Gal(AlgebraicClosure K/K)

theorem

absoluteGaloisClosureAbelianizationEquiv_conjugation

L71 ↗

KummerTheory.absoluteGaloisClosureAbelianizationEquiv_conjugation

Documentation

The closure comparison intertwines the actual semilinear action with the canonical action on the abelianized absolute Galois group.

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 Ω]
variable (K Ω) [IsAlgClosure K Ω]

Lean source · statement

theorem absoluteGaloisClosureAbelianizationEquiv_conjugation
    (τ : K ≃+* K) (a : Ω ≃+* Ω)
    (ha : ∀ k : K, a (algebraMap K Ω k) = algebraMap K Ω (τ k))
    (x : _root_.TopologicalAbelianization Gal(Ω/K)) :
    absoluteGaloisClosureAbelianizationEquiv K Ω
        (TopologicalAbelianization.congr (semilinearGaloisConjugateContinuousEquiv τ a ha) x) =
      absoluteGaloisAbelianizationAction τ (absoluteGaloisClosureAbelianizationEquiv K Ω x)

Module documentation

Comparing conjugation with the canonical absolute Galois action

Declarations

galoisClosureTransport_abelianization_conjugation_mk

absoluteGaloisClosureEquiv

absoluteGaloisClosureAbelianizationEquiv

absoluteGaloisClosureAbelianizationEquiv_conjugation