Module

TransferOrbitClosure.lean

Nyll.ClassFieldTheory.AbstractClassFieldTheory.Reciprocity.Construction.TransferOrbitClosure

2 declarations indexed from sourceView source ↗

Module documentation

The closed cyclic subgroup attached to one transfer orbit

For a finite-index subgroup H and an element g, the intersection of the closed cyclic subgroup generated by g with the stabilizer of a coset is generated by the power whose exponent is that orbit's minimal period. This is the topological group calculation used in transfer--norm naturality.

Imports3

Nyll.GaloisCohomology.ProfiniteIntegers.TopologicalGeneration
Mathlib.GroupTheory.Transfer
Mathlib.Topology.Algebra.Group.ClosedSubgroup

Imported by2

theorem

closedSubgroupGenerated_pow_eq_inf_stabilizer

L31 ↗

ClassFormation.closedSubgroupGenerated_pow_eq_inf_stabilizer

Documentation

The closed cyclic subgroup generated by the transfer power is the intersection of the original closed cyclic subgroup with the stabilizer of the chosen coset.

Source context 3 commands

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

namespace ClassFormation
noncomputable section
open MulAction

Lean source · statement

theorem closedSubgroupGenerated_pow_eq_inf_stabilizer
    {Q : Type*} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
    (H : Subgroup Q) [H.FiniteIndex]
    (hHclosed : IsClosed (H : Set Q)) (g : Q) (x : Q ⧸ H) :
    (closedSubgroupGenerated
        ({g ^ Function.minimalPeriod (g • ·) x} : Set Q) : Subgroup Q) =
      (closedSubgroupGenerated ({g} : Set Q) : Subgroup Q) ⊓
        MulAction.stabilizer Q x

theorem

mem_closedSubgroupGenerated_conjugate_iff

L114 ↗

ClassFormation.mem_closedSubgroupGenerated_conjugate_iff