Module

NormTopology.lean

Nyll.ClassFieldTheory.AbstractClassFieldTheory.Reciprocity.NormTopology

25 declarations indexed from sourceView source ↗

Module documentation

Abstract reciprocity: the norm topology

The neighbourhood basis at zero consists literally of the norm subgroups N_{L/K} A_L as L / K ranges over finite Galois extensions. Composita make this family downward directed.

Imports6

Mathlib.Algebra.Group.TransferInstance
Mathlib.Topology.Algebra.FilterBasis
Mathlib.Topology.Algebra.Group.ClosedSubgroup
Nyll.ClassFieldTheory.AbstractClassFieldTheory.Reciprocity.FiniteGaloisSubextension
Nyll.GaloisCohomology.Cyclic.IntegralRepUniverse
Nyll.ValuedFieldTheory.Valuation.Topology.Models

Imported by9

def

normSubgroup_compositum_le_left

L45 ↗

ClassFormation.FiniteGaloisSubextension.normSubgroup_compositum_le_left

Documentation

Proves the bound normSubgroup A (L₁.compositum L₂) ≤ normSubgroup A L₁.

Source context 6 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}

Lean source · statement

theorem normSubgroup_compositum_le_left
    (A : Rep ℤ G) (L₁ L₂ : FiniteGaloisSubextension K) :
    normSubgroup A (L₁.compositum L₂) ≤ normSubgroup A L₁

theorem

normSubgroup_compositum_le_right

L52 ↗

ClassFormation.FiniteGaloisSubextension.normSubgroup_compositum_le_right

Documentation

Proves the bound normSubgroup A (L₁.compositum L₂) ≤ normSubgroup A L₂.

Source context 6 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}

Lean source · statement

theorem normSubgroup_compositum_le_right
    (A : Rep ℤ G) (L₁ L₂ : FiniteGaloisSubextension K) :
    normSubgroup A (L₁.compositum L₂) ≤ normSubgroup A L₂

def

WithNormTopology

L107 ↗

ClassFormation.WithNormTopology

Documentation

The fixed subgroup with its norm topology recorded in the type. This is the public carrier model for norm-topological statements; choosing the norm topology no longer mutates the topology instance of the underlying group.

Source context 5 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
open FiniteGaloisSubextension

Lean source · statement

def WithNormTopology (A : Rep ℤ G) (K : ClosedSubgroup G) : Type _

instance

instTopologicalSpace

L112 ↗

ClassFormation.withNormTopology.instTopologicalSpace

Documentation

Installs the norm topology on the WithNormTopology carrier.

Source context 5 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
open FiniteGaloisSubextension

Lean source · statement

instance withNormTopology.instTopologicalSpace
    (A : Rep ℤ G) (K : ClosedSubgroup G) :
    TopologicalSpace (WithNormTopology A K)

instance

instAddCommGroup

L121 ↗

ClassFormation.withNormTopology.instAddCommGroup

Documentation

Transports the additive commutative group structure to the WithNormTopology carrier.

Source context 5 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
open FiniteGaloisSubextension

Lean source · statement

instance withNormTopology.instAddCommGroup
    (A : Rep ℤ G) (K : ClosedSubgroup G) :
    AddCommGroup (WithNormTopology A K)

def

withNormTopologyEquiv

L130 ↗

ClassFormation.withNormTopologyEquiv

Documentation

Forget the norm-topology wrapper without changing the underlying point.

Source context 5 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
open FiniteGaloisSubextension

Lean source · statement

def withNormTopologyEquiv (A : Rep ℤ G) (K : ClosedSubgroup G) :
    WithNormTopology A K ≃ ambientFixedAddSubgroup A K

def

IsNormOpen

L137 ↗

ClassFormation.IsNormOpen

Documentation

Openness in the norm topology, expressed through the type-level norm topology model.

Source context 5 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
open FiniteGaloisSubextension

Lean source · statement

def IsNormOpen (A : Rep ℤ G) (K : ClosedSubgroup G)
    (s : Set (ambientFixedAddSubgroup A K)) : Prop

def

IsNormClosed

L143 ↗

ClassFormation.IsNormClosed

Documentation

Closedness in the norm topology, expressed through the type-level norm topology model.

Source context 5 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
open FiniteGaloisSubextension

Lean source · statement

def IsNormClosed (A : Rep ℤ G) (K : ClosedSubgroup G)
    (s : Set (ambientFixedAddSubgroup A K)) : Prop

def

IsNormHausdorff

L148 ↗

ClassFormation.IsNormHausdorff

Documentation

Hausdorffness of the type-level norm-topology model.

Source context 5 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
open FiniteGaloisSubextension

Lean source · statement

def IsNormHausdorff (A : Rep ℤ G) (K : ClosedSubgroup G) : Prop

def

IsContinuousFromNormTopology

L153 ↗

ClassFormation.IsContinuousFromNormTopology

Documentation

Continuity from a norm-topological fixed subgroup to an explicitly topologized target.

Source context 5 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
open FiniteGaloisSubextension

Lean source · statement

def IsContinuousFromNormTopology
    (A : Rep ℤ G) (K : ClosedSubgroup G)
    {β : Type*} [TopologicalSpace β]
    (f : ambientFixedAddSubgroup A K → β) : Prop

def

IsNormContinuous

L160 ↗

ClassFormation.IsNormContinuous

Documentation

Continuity between two fixed subgroups carrying their norm topologies.

Source context 5 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
open FiniteGaloisSubextension

Lean source · statement

def IsNormContinuous
    (A : Rep ℤ G) (L K : ClosedSubgroup G)
    (f : ambientFixedAddSubgroup A L → ambientFixedAddSubgroup A K) : Prop

theorem

isNormOpen_iff_raw

L166 ↗

ClassFormation.isNormOpen_iff_raw

Source context 5 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
open FiniteGaloisSubextension

Lean source · statement

theorem isNormOpen_iff_raw
    (A : Rep ℤ G) (K : ClosedSubgroup G)
    (s : Set (ambientFixedAddSubgroup A K)) :
    IsNormOpen A K s ↔
      @IsOpen (ambientFixedAddSubgroup A K) (normTopology A K) s

theorem

isNormClosed_iff_raw

L173 ↗

ClassFormation.isNormClosed_iff_raw

Source context 5 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
open FiniteGaloisSubextension

Lean source · statement

theorem isNormClosed_iff_raw
    (A : Rep ℤ G) (K : ClosedSubgroup G)
    (s : Set (ambientFixedAddSubgroup A K)) :
    IsNormClosed A K s ↔
      @IsClosed (ambientFixedAddSubgroup A K) (normTopology A K) s

def

withNormTopologyHomeomorph

L180 ↗

ClassFormation.withNormTopologyHomeomorph

Source context 5 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
open FiniteGaloisSubextension

Lean source · statement

def withNormTopologyHomeomorph
    (A : Rep ℤ G) (K : ClosedSubgroup G) :
    @Homeomorph (WithNormTopology A K) (ambientFixedAddSubgroup A K)
      (inferInstance : TopologicalSpace (WithNormTopology A K))
      (normTopology A K)

theorem

mem_normFilterBasis_iff

L191 ↗

ClassFormation.mem_normFilterBasis_iff

Documentation

A set belongs to the defining filter basis exactly when it is one of the finite Galois norm subgroups.

Source context 5 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
open FiniteGaloisSubextension

Lean source · statement

theorem mem_normFilterBasis_iff
    (A : Rep ℤ G) (K : ClosedSubgroup G)
    (U : Set (ambientFixedAddSubgroup A K)) :
    U ∈ normFilterBasis A K ↔
      ∃ L : FiniteGaloisSubextension K,
        U = (normSubgroup A L : Set (ambientFixedAddSubgroup A K))

theorem

normTopology_addSubgroup_isOpen_iff

L201 ↗

ClassFormation.normTopology_addSubgroup_isOpen_iff

Documentation

A subgroup is open in the norm topology exactly when it contains one finite Galois norm subgroup.

Source context 5 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
open FiniteGaloisSubextension

Lean source · statement

theorem normTopology_addSubgroup_isOpen_iff
    (A : Rep ℤ G) (K : ClosedSubgroup G)
    (H : AddSubgroup (ambientFixedAddSubgroup A K)) :
    IsNormOpen A K H ↔
      ∃ L : FiniteGaloisSubextension K, normSubgroup A L ≤ H

theorem

normSubgroup_isOpen

L224 ↗

ClassFormation.normSubgroup_isOpen

Documentation

Every defining norm subgroup is open.

Source context 5 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
open FiniteGaloisSubextension

Lean source · statement

theorem normSubgroup_isOpen
    (A : Rep ℤ G) (K : ClosedSubgroup G)
    (L : FiniteGaloisSubextension K) :
    IsNormOpen A K (normSubgroup A L)

def

universalNormSubgroup

L232 ↗

ClassFormation.universalNormSubgroup

Documentation

The subgroup of universal norms used in Hausdorffness of the norm topology.

Source context 5 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
open FiniteGaloisSubextension

Lean source · statement

def universalNormSubgroup (A : Rep ℤ G) (K : ClosedSubgroup G) :
    AddSubgroup (ambientFixedAddSubgroup A K)

theorem

mem_universalNormSubgroup_iff

L241 ↗

ClassFormation.mem_universalNormSubgroup_iff

Documentation

Characterizes a ∈ universalNormSubgroup A K by the equivalent condition ∀ L : FiniteGaloisSubextension K, a ∈ normSubgroup A L.

Source context 5 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
open FiniteGaloisSubextension

Lean source · statement

theorem mem_universalNormSubgroup_iff
    (A : Rep ℤ G) (K : ClosedSubgroup G)
    (a : ambientFixedAddSubgroup A K) :
    a ∈ universalNormSubgroup A K ↔
      ∀ L : FiniteGaloisSubextension K, a ∈ normSubgroup A L

theorem

normTopology_hausdorff_raw

L248 ↗

ClassFormation.normTopology_hausdorff_raw

Source context 5 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
open FiniteGaloisSubextension

Lean source · statement

theorem normTopology_hausdorff_raw
    (A : Rep ℤ G) (K : ClosedSubgroup G) :
    @T2Space (ambientFixedAddSubgroup A K) (normTopology A K) ↔
      universalNormSubgroup A K = ⊥

theorem

normTopology_hausdorff

L278 ↗

ClassFormation.normTopology_hausdorff

Documentation

Hausdorffness of the norm topology: the norm-topology model is Hausdorff exactly when the universal norm subgroup is trivial.

Source context 5 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
open FiniteGaloisSubextension

Lean source · statement

theorem normTopology_hausdorff
    (A : Rep ℤ G) (K : ClosedSubgroup G) :
    IsNormHausdorff A K ↔ universalNormSubgroup A K = ⊥

theorem

normTopology_open_iff_closed_finiteIndex_of_finite_normQuotients

L299 ↗

ClassFormation.normTopology_open_iff_closed_finiteIndex_of_finite_normQuotients

Documentation

General norm-topology lemma: once every defining norm quotient is finite, openness is equivalent to closedness together with finite index. the norm-subgroup basis characterization supplies the finiteness premise from the abstract reciprocity theorem.

Source context 5 commands

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

noncomputable section
namespace ClassFormation
open CyclicCohomology KummerTheory

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
open FiniteGaloisSubextension

Lean source · statement

theorem normTopology_open_iff_closed_finiteIndex_of_finite_normQuotients
    (A : Rep ℤ G) (K : ClosedSubgroup G)
    (hfinite : ∀ L : FiniteGaloisSubextension K,
      Finite (ambientFixedAddSubgroup A K ⧸ normSubgroup A L))
    (H : AddSubgroup (ambientFixedAddSubgroup A K)) :
    IsNormOpen A K H ↔
      IsNormClosed A K H ∧
        Finite (ambientFixedAddSubgroup A K ⧸ H)

Module documentation

Abstract reciprocity: the norm topology

Declarations