Module

GaloisClosureTransport.lean

Nyll.GaloisCohomology.Kummer.Concrete.GaloisClosureTransport

6 declarations indexed from sourceView source ↗

Module documentation

Transport of Galois groups between equivalent extension fields

A base-linear field equivalence conjugates the relative Galois groups and preserves their Krull topologies. A finite intermediate field pulls back to a finite intermediate field under the inverse equivalence, so no algebraicity assumption on the ambient extensions is needed.

Imports4

Mathlib.Algebra.Algebra.Equiv
Mathlib.FieldTheory.KrullTopology
Mathlib.Topology.Algebra.Group.Basic
Mathlib.Topology.Algebra.ContinuousMonoidHom

Imported by5

theorem

galoisClosureTransport_continuous

KummerTheory.galoisClosureTransport_continuous

Documentation

Conjugation by an algebra equivalence is continuous for the Krull topologies on the relative Galois groups.

Source context 3 commands

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

namespace KummerTheory
open scoped Topology
variable {K Ω Ω' : Type*} [Field K] [Field Ω] [Field Ω']
  [Algebra K Ω] [Algebra K Ω']

Lean source · statement

theorem galoisClosureTransport_continuous (e : Ω ≃ₐ[K] Ω') :
    Continuous (AlgEquiv.autCongr e)

def

galoisClosureTransport

KummerTheory.galoisClosureTransport

Documentation

A base-linear field equivalence transports relative Galois groups as topological groups with the Krull topology.

Source context 3 commands

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

namespace KummerTheory
open scoped Topology
variable {K Ω Ω' : Type*} [Field K] [Field Ω] [Field Ω']
  [Algebra K Ω] [Algebra K Ω']

Lean source · full declaration

def galoisClosureTransport (e : Ω ≃ₐ[K] Ω') : Gal(Ω/K) ≃ₜ* Gal(Ω'/K) where
  toMulEquiv := AlgEquiv.autCongr e
  continuous_toFun := galoisClosureTransport_continuous e
  continuous_invFun := galoisClosureTransport_continuous e.symm

theorem

galoisClosureTransport_toMulEquiv

KummerTheory.galoisClosureTransport_toMulEquiv

Documentation

Forgetting topology recovers the algebraic conjugation equivalence.

Source context 3 commands

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

namespace KummerTheory
open scoped Topology
variable {K Ω Ω' : Type*} [Field K] [Field Ω] [Field Ω']
  [Algebra K Ω] [Algebra K Ω']

Lean source · statement

theorem galoisClosureTransport_toMulEquiv (e : Ω ≃ₐ[K] Ω') :
    (galoisClosureTransport e).toMulEquiv = AlgEquiv.autCongr e

theorem

galoisClosureTransport_apply

KummerTheory.galoisClosureTransport_apply

Documentation

The transported automorphism evaluates by conjugating in the extension fields.

Source context 3 commands

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

namespace KummerTheory
open scoped Topology
variable {K Ω Ω' : Type*} [Field K] [Field Ω] [Field Ω']
  [Algebra K Ω] [Algebra K Ω']

Lean source · statement

theorem galoisClosureTransport_apply (e : Ω ≃ₐ[K] Ω') (σ : Gal(Ω/K)) (x : Ω') :
    galoisClosureTransport e σ x = e (σ (e.symm x))

theorem

galoisClosureTransport_symm_apply

KummerTheory.galoisClosureTransport_symm_apply

Documentation

The inverse transport evaluates by the inverse field equivalence.

Source context 3 commands

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

namespace KummerTheory
open scoped Topology
variable {K Ω Ω' : Type*} [Field K] [Field Ω] [Field Ω']
  [Algebra K Ω] [Algebra K Ω']

Lean source · statement

theorem galoisClosureTransport_symm_apply (e : Ω ≃ₐ[K] Ω')
    (σ : Gal(Ω'/K)) (x : Ω) :
    (galoisClosureTransport e).symm σ x = e.symm (σ (e x))

theorem

galoisClosureTransport_symm

KummerTheory.galoisClosureTransport_symm

Documentation

Transport in the reverse direction is transport by the inverse algebra equivalence.

Source context 3 commands

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

namespace KummerTheory
open scoped Topology
variable {K Ω Ω' : Type*} [Field K] [Field Ω] [Field Ω']
  [Algebra K Ω] [Algebra K Ω']

Lean source · statement

theorem galoisClosureTransport_symm (e : Ω ≃ₐ[K] Ω') :
    (galoisClosureTransport e).symm = galoisClosureTransport e.symm