Module

NormalRestrictionKernel.lean

Nyll.GaloisCohomology.Kummer.Concrete.NormalRestrictionKernel

10 declarations indexed from sourceView source ↗

Module documentation

The actual normal-restriction kernel

The kernel of restriction from Gal(Ω/K) to Gal(M/K) is Gal(Ω/M), with the same underlying field automorphisms. For finite M/K and Galois Ω/K this is a continuous equivalence. Actual subgroup conjugation becomes semilinear conjugation by the same ambient automorphism.

Imports8

Nyll.GaloisCohomology.Kummer.Concrete.NormalRestrictionKernelFinite
Nyll.GaloisCohomology.Kummer.Concrete.SemilinearConjugation
Mathlib.FieldTheory.KrullTopology
Mathlib.FieldTheory.Galois.Profinite
Mathlib.FieldTheory.Normal.Defs
Mathlib.Topology.Algebra.ContinuousMonoidHom
Mathlib.Topology.Algebra.OpenSubgroup
Mathlib.Topology.Homeomorph.Lemmas

Imported by2

def

normalRestrictionKernelEquiv

L38 ↗

KummerTheory.normalRestrictionKernelEquiv

Documentation

Reinterpret an automorphism in the restriction kernel as an M-linear automorphism, and restrict scalars for the inverse.

Source context 4 commands

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

namespace KummerTheory
open scoped Topology
universe u
variable {K : Type u} (M : Type u) (Ω : Type u)
  [Field K] [Field M] [Field Ω]
  [Algebra K M] [Algebra K Ω] [Algebra M Ω] [IsScalarTower K M Ω]
  [Normal K M]

Lean source · full declaration

def normalRestrictionKernelEquiv :
    (AlgEquiv.restrictNormalHom M : Gal(Ω/K) →* Gal(M/K)).ker ≃* Gal(Ω/M) where
  toFun σ :=
    { σ.val.toRingEquiv with
      commutes' := fun m => by
        change σ.val (algebraMap M Ω m) = algebraMap M Ω m
        rw [← σ.val.restrictNormal_commutes M m]
        have hσ : σ.val.restrictNormal M = 1 := σ.property
        rw [hσ]
        rfl }
  invFun σ := ⟨σ.restrictScalars K, by
    apply AlgEquiv.ext
    intro m
    apply (algebraMap M Ω).injective
    change algebraMap M Ω ((σ.restrictScalars K).restrictNormal M m) = algebraMap M Ω m
    rw [AlgEquiv.restrictNormal_commutes]
    exact σ.commutes m⟩
  left_inv σ := by
    apply Subtype.ext
    apply AlgEquiv.ext
    intro x
    rfl
  right_inv σ := by
    apply AlgEquiv.ext
    intro x
    rfl
  map_mul' σ τ := by
    apply AlgEquiv.ext
    intro x
    rfl

theorem

normalRestrictionKernelEquiv_apply

L70 ↗

KummerTheory.normalRestrictionKernelEquiv_apply

Documentation

Forward reinterpretation leaves ambient evaluation unchanged.

Source context 4 commands

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

namespace KummerTheory
open scoped Topology
universe u
variable {K : Type u} (M : Type u) (Ω : Type u)
  [Field K] [Field M] [Field Ω]
  [Algebra K M] [Algebra K Ω] [Algebra M Ω] [IsScalarTower K M Ω]
  [Normal K M]

Lean source · statement

theorem normalRestrictionKernelEquiv_apply
    (σ : (AlgEquiv.restrictNormalHom M : Gal(Ω/K) →* Gal(M/K)).ker) (x : Ω) :
    normalRestrictionKernelEquiv M Ω σ x = (σ : Gal(Ω/K)) x

theorem

normalRestrictionKernelEquiv_symm_apply

L75 ↗

KummerTheory.normalRestrictionKernelEquiv_symm_apply

Documentation

The inverse is actual restriction of scalars.

Source context 4 commands

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

namespace KummerTheory
open scoped Topology
universe u
variable {K : Type u} (M : Type u) (Ω : Type u)
  [Field K] [Field M] [Field Ω]
  [Algebra K M] [Algebra K Ω] [Algebra M Ω] [IsScalarTower K M Ω]
  [Normal K M]

Lean source · statement

theorem normalRestrictionKernelEquiv_symm_apply (σ : Gal(Ω/M)) :
    ((normalRestrictionKernelEquiv (K := K) M Ω).symm σ : Gal(Ω/K)) =
      σ.restrictScalars K

theorem

normalRestriction_algebraMap

L80 ↗

KummerTheory.normalRestriction_algebraMap

Documentation

An ambient automorphism is semilinear over its actual restriction to M.

Source context 4 commands

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

namespace KummerTheory
open scoped Topology
universe u
variable {K : Type u} (M : Type u) (Ω : Type u)
  [Field K] [Field M] [Field Ω]
  [Algebra K M] [Algebra K Ω] [Algebra M Ω] [IsScalarTower K M Ω]
  [Normal K M]

Lean source · statement

theorem normalRestriction_algebraMap (g : Gal(Ω/K)) (m : M) :
    g.toRingEquiv (algebraMap M Ω m) =
      algebraMap M Ω ((g.restrictNormal M).toRingEquiv m)

theorem

normalRestrictionKernelEquiv_conjNormal

L86 ↗

KummerTheory.normalRestrictionKernelEquiv_conjNormal

Documentation

Kernel conjugation and semilinear conjugation use the same representative.

Source context 4 commands

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

namespace KummerTheory
open scoped Topology
universe u
variable {K : Type u} (M : Type u) (Ω : Type u)
  [Field K] [Field M] [Field Ω]
  [Algebra K M] [Algebra K Ω] [Algebra M Ω] [IsScalarTower K M Ω]
  [Normal K M]

Lean source · statement

theorem normalRestrictionKernelEquiv_conjNormal (g : Gal(Ω/K))
    (σ : (AlgEquiv.restrictNormalHom M : Gal(Ω/K) →* Gal(M/K)).ker) :
    normalRestrictionKernelEquiv M Ω (MulAut.conjNormal g σ) =
      semilinearGaloisConjugate (g.restrictNormal M).toRingEquiv g.toRingEquiv
        (normalRestriction_algebraMap M Ω g) (normalRestrictionKernelEquiv M Ω σ)

theorem

normalRestrictionKernelEquiv_continuous

L102 ↗

KummerTheory.normalRestrictionKernelEquiv_continuous

Source context 5 commands

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

namespace KummerTheory
open scoped Topology
universe u
variable {K : Type u} (M : Type u) (Ω : Type u)
  [Field K] [Field M] [Field Ω]
  [Algebra K M] [Algebra K Ω] [Algebra M Ω] [IsScalarTower K M Ω]
  [Normal K M]
variable [FiniteDimensional K M]

-- The finite intermediate field E adds only its canonical scalar restrictions.
-- The K/M/Ω field-algebra tower is fixed once; no alternate module is installed.

Lean source · statement

theorem normalRestrictionKernelEquiv_continuous :
    Continuous (normalRestrictionKernelEquiv (K := K) M Ω)

def

normalRestrictionKernelContinuousEquiv

L127 ↗

KummerTheory.normalRestrictionKernelContinuousEquiv

Documentation

The actual restriction-kernel identification is a homeomorphism for the subgroup and Krull topologies.

Source context 6 commands

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

namespace KummerTheory
open scoped Topology
universe u
variable {K : Type u} (M : Type u) (Ω : Type u)
  [Field K] [Field M] [Field Ω]
  [Algebra K M] [Algebra K Ω] [Algebra M Ω] [IsScalarTower K M Ω]
  [Normal K M]
variable [FiniteDimensional K M]

-- The finite intermediate field E adds only its canonical scalar restrictions.
-- The K/M/Ω field-algebra tower is fixed once; no alternate module is installed.
variable [IsGalois K Ω]

Lean source · statement

def normalRestrictionKernelContinuousEquiv :
    (AlgEquiv.restrictNormalHom M : Gal(Ω/K) →* Gal(M/K)).ker ≃ₜ* Gal(Ω/M)

theorem

normalRestrictionKernelContinuousEquiv_apply

L145 ↗

KummerTheory.normalRestrictionKernelContinuousEquiv_apply

Documentation

Evaluation of the continuous equivalence preserves the representative.

Source context 6 commands

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

namespace KummerTheory
open scoped Topology
universe u
variable {K : Type u} (M : Type u) (Ω : Type u)
  [Field K] [Field M] [Field Ω]
  [Algebra K M] [Algebra K Ω] [Algebra M Ω] [IsScalarTower K M Ω]
  [Normal K M]
variable [FiniteDimensional K M]

-- The finite intermediate field E adds only its canonical scalar restrictions.
-- The K/M/Ω field-algebra tower is fixed once; no alternate module is installed.
variable [IsGalois K Ω]

Lean source · statement

theorem normalRestrictionKernelContinuousEquiv_apply
    (σ : (AlgEquiv.restrictNormalHom M : Gal(Ω/K) →* Gal(M/K)).ker) (x : Ω) :
    normalRestrictionKernelContinuousEquiv M Ω σ x = (σ : Gal(Ω/K)) x

theorem

normalRestrictionKernelContinuousEquiv_symm_apply

L150 ↗

KummerTheory.normalRestrictionKernelContinuousEquiv_symm_apply

Documentation

The inverse continuous equivalence restricts scalars on the representative.

Source context 6 commands

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

namespace KummerTheory
open scoped Topology
universe u
variable {K : Type u} (M : Type u) (Ω : Type u)
  [Field K] [Field M] [Field Ω]
  [Algebra K M] [Algebra K Ω] [Algebra M Ω] [IsScalarTower K M Ω]
  [Normal K M]
variable [FiniteDimensional K M]

-- The finite intermediate field E adds only its canonical scalar restrictions.
-- The K/M/Ω field-algebra tower is fixed once; no alternate module is installed.
variable [IsGalois K Ω]

Lean source · statement

theorem normalRestrictionKernelContinuousEquiv_symm_apply (σ : Gal(Ω/M)) :
    ((normalRestrictionKernelContinuousEquiv (K := K) M Ω).symm σ : Gal(Ω/K)) =
      σ.restrictScalars K

theorem

normalRestrictionKernelContinuousEquiv_conjNormal

L156 ↗

KummerTheory.normalRestrictionKernelContinuousEquiv_conjNormal

Documentation

Continuous kernel transport intertwines actual conjugation with semilinear conjugation by the same ambient lift.

Source context 6 commands

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

namespace KummerTheory
open scoped Topology
universe u
variable {K : Type u} (M : Type u) (Ω : Type u)
  [Field K] [Field M] [Field Ω]
  [Algebra K M] [Algebra K Ω] [Algebra M Ω] [IsScalarTower K M Ω]
  [Normal K M]
variable [FiniteDimensional K M]

-- The finite intermediate field E adds only its canonical scalar restrictions.
-- The K/M/Ω field-algebra tower is fixed once; no alternate module is installed.
variable [IsGalois K Ω]

Lean source · statement

theorem normalRestrictionKernelContinuousEquiv_conjNormal (g : Gal(Ω/K))
    (σ : (AlgEquiv.restrictNormalHom M : Gal(Ω/K) →* Gal(M/K)).ker) :
    normalRestrictionKernelContinuousEquiv M Ω (MulAut.conjNormal g σ) =
      semilinearGaloisConjugate (g.restrictNormal M).toRingEquiv g.toRingEquiv
        (normalRestriction_algebraMap M Ω g)
        (normalRestrictionKernelContinuousEquiv M Ω σ)

Module documentation

The actual normal-restriction kernel

Declarations