Module

KummerFixedField.lean

Nyll.GaloisCohomology.Kummer.Abstract.KummerFixedField

5 declarations indexed from sourceView source ↗

Module documentation

finite abelian Kummer theory: the abstract field `K(S)`

in this construction, for a subset S of the coefficient module, K(S) is the abstract field whose subgroup consists of the elements of G_K fixing every member of S. This file constructs that subgroup and proves that it is closed. Closedness follows directly from continuity of each orbit map and the discrete topology on the coefficient module.

Imports2

Imported by2

def

setFixingSubgroup

L30 ↗

KummerTheory.setFixingSubgroup

Documentation

The subgroup of G_K fixing every element of S, viewed as a subgroup of the ambient abstract Galois group G.

Source context 3 commands

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

namespace KummerTheory
open CyclicCohomology
noncomputable section

Lean source · statement

def setFixingSubgroup
    {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
    (A : Rep ℤ G) (K : ClosedSubgroup G) (S : Set A.V) : Subgroup G

theorem

isClosed_setOf_representation_fixed

L58 ↗

KummerTheory.isClosed_setOf_representation_fixed

Documentation

For a continuous discrete representation, the stabilizer of one coefficient element is closed.

Source context 3 commands

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

namespace KummerTheory
open CyclicCohomology
noncomputable section

Lean source · statement

theorem isClosed_setOf_representation_fixed
    {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
    (A : Rep ℤ G) (hcontinuous : IsContinuousDiscreteRepresentation A)
    (a : A.V) : IsClosed {σ : G | A.ρ σ a = a}

theorem

setFixingSubgroup_isClosed

L71 ↗

KummerTheory.setFixingSubgroup_isClosed

Documentation

The subgroup defining K(S) is closed.

Source context 3 commands

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

namespace KummerTheory
open CyclicCohomology
noncomputable section

Lean source · statement

theorem setFixingSubgroup_isClosed
    {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
    (A : Rep ℤ G) (hcontinuous : IsContinuousDiscreteRepresentation A)
    (K : ClosedSubgroup G) (S : Set A.V) :
    IsClosed (setFixingSubgroup A K S : Set G)

def

closedSetFixingSubgroup

L89 ↗

KummerTheory.closedSetFixingSubgroup

Documentation

The closed subgroup representing the abstract field K(S). Its underlying subgroup is exactly the elements of G_K which fix S pointwise.

Source context 3 commands

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

namespace KummerTheory
open CyclicCohomology
noncomputable section

Lean source · statement

def closedSetFixingSubgroup
    {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
    (A : Rep ℤ G) (hcontinuous : IsContinuousDiscreteRepresentation A)
    (K : ClosedSubgroup G) (S : Set A.V) : ClosedSubgroup G

theorem

mem_closedSetFixingSubgroup_iff

L98 ↗

KummerTheory.mem_closedSetFixingSubgroup_iff

Documentation

An automorphism lies in the fixing subgroup exactly when it fixes every element of the closed set.

Source context 3 commands

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

namespace KummerTheory
open CyclicCohomology
noncomputable section

Lean source · statement

theorem mem_closedSetFixingSubgroup_iff
    {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
    (A : Rep ℤ G) (hcontinuous : IsContinuousDiscreteRepresentation A)
    (K : ClosedSubgroup G) (S : Set A.V) (σ : G) :
    σ ∈ closedSetFixingSubgroup A hcontinuous K S ↔
      σ ∈ K ∧ ∀ a, a ∈ S → A.ρ σ a = a

Module documentation

finite abelian Kummer theory: the abstract field K(S)

Declarations

setFixingSubgroup

isClosed_setOf_representation_fixed

setFixingSubgroup_isClosed

closedSetFixingSubgroup

mem_closedSetFixingSubgroup_iff

finite abelian Kummer theory: the abstract field `K(S)`