Module

Duality.lean

Nyll.ProCGroups.Duality

20 declarations indexed from sourceView source ↗

Module documentation

Pro C Groups / Duality

This module formalizes elementary duality constructions for profinite groups.

Imports7

Mathlib.Algebra.Polynomial.Roots
Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
Mathlib.FieldTheory.Finite.Basic
Mathlib.GroupTheory.Torsion
Mathlib.Topology.Algebra.PontryaginDual
Mathlib.Topology.Instances.AddCircle.DenseSubgroup
Nyll.ProCGroups.Topologies.ContinuousMulEquiv

Imported by2

theorem

properClosedAddSubgroup_addCircle_finite

L32 ↗

ProCGroups.Duality.properClosedAddSubgroup_addCircle_finite

Documentation

A closed proper additive subgroup of an additive circle AddCircle p is finite.

Source context 5 commands

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

open scoped Topology
namespace ProCGroups.Duality
universe u v
section Basic
variable (G : Type u) [CommGroup G] [TopologicalSpace G]

Lean source · statement

theorem properClosedAddSubgroup_addCircle_finite
    {p : ℝ} [Fact (0 < p)] (B : AddSubgroup (AddCircle p))
    (hBclosed : IsClosed (B : Set (AddCircle p))) (hBproper : B ≠ ⊤) :
    Finite B

def

circleSubgroupToAddCircleSubgroup

L61 ↗

ProCGroups.Duality.circleSubgroupToAddCircleSubgroup

Documentation

Transport a multiplicative subgroup of Circle to the standard additive circle ℝ / (2π)ℤ. This is convenient for applying AddCircle subgroup-classification lemmas.

Source context 5 commands

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

open scoped Topology
namespace ProCGroups.Duality
universe u v
section Basic
variable (G : Type u) [CommGroup G] [TopologicalSpace G]

Lean source · statement

def circleSubgroupToAddCircleSubgroup (A : Subgroup Circle) :
    AddSubgroup (AddCircle (2 * Real.pi))

theorem

mem_circleSubgroupToAddCircleSubgroup_iff

L87 ↗

ProCGroups.Duality.mem_circleSubgroupToAddCircleSubgroup_iff

Documentation

Membership in the transported additive subgroup is detected by the circle homeomorphism.

Source context 5 commands

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

open scoped Topology
namespace ProCGroups.Duality
universe u v
section Basic
variable (G : Type u) [CommGroup G] [TopologicalSpace G]

Lean source · statement

theorem mem_circleSubgroupToAddCircleSubgroup_iff
    {A : Subgroup Circle} {θ : AddCircle (2 * Real.pi)} :
    θ ∈ circleSubgroupToAddCircleSubgroup A ↔ AddCircle.homeomorphCircle' θ ∈ A

theorem

isClosed_circleSubgroupToAddCircleSubgroup

L93 ↗

ProCGroups.Duality.isClosed_circleSubgroupToAddCircleSubgroup

Documentation

Transporting a closed circle subgroup to the additive circle preserves closedness.

Source context 5 commands

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

open scoped Topology
namespace ProCGroups.Duality
universe u v
section Basic
variable (G : Type u) [CommGroup G] [TopologicalSpace G]

Lean source · statement

theorem isClosed_circleSubgroupToAddCircleSubgroup
    (A : Subgroup Circle) (hAclosed : IsClosed (A : Set Circle)) :
    IsClosed (circleSubgroupToAddCircleSubgroup A : Set (AddCircle (2 * Real.pi)))

theorem

circleSubgroupToAddCircleSubgroup_ne_top

L100 ↗

ProCGroups.Duality.circleSubgroupToAddCircleSubgroup_ne_top

Documentation

Transporting a proper circle subgroup to the additive circle preserves properness.

Source context 5 commands

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

open scoped Topology
namespace ProCGroups.Duality
universe u v
section Basic
variable (G : Type u) [CommGroup G] [TopologicalSpace G]

Lean source · statement

theorem circleSubgroupToAddCircleSubgroup_ne_top
    (A : Subgroup Circle) (hAproper : A ≠ ⊤) :
    circleSubgroupToAddCircleSubgroup A ≠ ⊤

theorem

properClosedSubgroup_circleTarget_finite

L116 ↗

ProCGroups.Duality.properClosedSubgroup_circleTarget_finite

Documentation

Every proper closed subgroup of the circle is finite.

Source context 5 commands

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

open scoped Topology
namespace ProCGroups.Duality
universe u v
section Basic
variable (G : Type u) [CommGroup G] [TopologicalSpace G]

Lean source · statement

theorem properClosedSubgroup_circleTarget_finite
    (A : Subgroup Circle) (hAclosed : IsClosed (A : Set Circle))
    (hAproper : A ≠ ⊤) :
    Finite A

theorem

circleTarget_one_ne_exp_pi

L145 ↗

ProCGroups.Duality.circleTarget_one_ne_exp_pi

Documentation

The circle target contains two distinct points.

Source context 6 commands

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

open scoped Topology
namespace ProCGroups.Duality
universe u v
section Basic
variable (G : Type u) [CommGroup G] [TopologicalSpace G]
variable {G}

Lean source · statement

theorem circleTarget_one_ne_exp_pi :
    (1 : Circle) ≠ Circle.exp Real.pi

theorem

not_totallyDisconnectedSpace_circleTarget

L150 ↗

ProCGroups.Duality.not_totallyDisconnectedSpace_circleTarget

Documentation

The circle target is not totally disconnected.

Source context 6 commands

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

open scoped Topology
namespace ProCGroups.Duality
universe u v
section Basic
variable (G : Type u) [CommGroup G] [TopologicalSpace G]
variable {G}

Lean source · statement

theorem not_totallyDisconnectedSpace_circleTarget :
    ¬ TotallyDisconnectedSpace Circle

theorem

subgroup_eq_bot_of_isCompact_subset_rightHalfPlane

L159 ↗

ProCGroups.Duality.subgroup_eq_bot_of_isCompact_subset_rightHalfPlane

Documentation

A compact subgroup of T contained in the open right half-plane is trivial.

Source context 6 commands

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

open scoped Topology
namespace ProCGroups.Duality
universe u v
section Basic
variable (G : Type u) [CommGroup G] [TopologicalSpace G]
variable {G}

Lean source · statement

theorem subgroup_eq_bot_of_isCompact_subset_rightHalfPlane
    (A : Subgroup Circle) (hAcompact : IsCompact (A : Set Circle))
    (hApos : ∀ z ∈ A, 0 < Complex.re (z : ℂ)) :
    A = ⊥

theorem

dualGroup_discrete_of_compact

L215 ↗

ProCGroups.Duality.dualGroup_discrete_of_compact

Documentation

The Pontryagin dual of a compact abelian group is discrete.

Source context 6 commands

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

open scoped Topology
namespace ProCGroups.Duality
universe u v
section Basic
variable (G : Type u) [CommGroup G] [TopologicalSpace G]
variable {G}

Lean source · statement

theorem dualGroup_discrete_of_compact [CompactSpace G] :
    DiscreteTopology (PontryaginDual G)

instance

dualCompactSpaceOfDiscreteTopology

L263 ↗

ProCGroups.Duality.dualCompactSpaceOfDiscreteTopology

Documentation

A discrete abelian group has compact Pontryagin dual.

Source context 6 commands

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

open scoped Topology
namespace ProCGroups.Duality
universe u v
section Basic
variable (G : Type u) [CommGroup G] [TopologicalSpace G]
variable {G}

Lean source · statement

instance dualCompactSpaceOfDiscreteTopology [DiscreteTopology G] :
    CompactSpace (PontryaginDual G)

theorem

dualGroup_compact_of_discrete

L268 ↗

ProCGroups.Duality.dualGroup_compact_of_discrete

Documentation

The Pontryagin dual of a discrete abelian group is compact.

Source context 6 commands

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

open scoped Topology
namespace ProCGroups.Duality
universe u v
section Basic
variable (G : Type u) [CommGroup G] [TopologicalSpace G]
variable {G}

Lean source · statement

theorem dualGroup_compact_of_discrete [DiscreteTopology G] :
    CompactSpace (PontryaginDual G)

def

torsionPowerWitnessOfElement

L272 ↗

ProCGroups.Duality.torsionPowerWitnessOfElement

Source context 6 commands

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

open scoped Topology
namespace ProCGroups.Duality
universe u v
section Basic
variable (G : Type u) [CommGroup G] [TopologicalSpace G]
variable {G}

Lean source · statement

def torsionPowerWitnessOfElement
    {G : Type u} [CommGroup G] (htors : IsMulTorsion G) (g : G) :
    {n : ℕ // 0 < n ∧ g ^ n = 1}

theorem

dualGroup_totallyDisconnected_of_discrete_torsion

L279 ↗

ProCGroups.Duality.dualGroup_totallyDisconnected_of_discrete_torsion

Documentation

The Pontryagin dual of a discrete torsion abelian group is totally disconnected.

Source context 6 commands

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

open scoped Topology
namespace ProCGroups.Duality
universe u v
section Basic
variable (G : Type u) [CommGroup G] [TopologicalSpace G]
variable {G}

Lean source · statement

theorem dualGroup_totallyDisconnected_of_discrete_torsion
    (G : Type u) [CommGroup G] [TopologicalSpace G]
    [DiscreteTopology G] (htors : IsMulTorsion G) :
    TotallyDisconnectedSpace (PontryaginDual G)

def

dualGroupEquivAddCharCircle

L340 ↗

ProCGroups.Duality.dualGroupEquivAddCharCircle

Documentation

For a discrete abelian group, multiplicative characters to the circle are the same as additive characters on the additive type synonym.

Source context 6 commands

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

open scoped Topology
namespace ProCGroups.Duality
universe u v
section Basic
variable (G : Type u) [CommGroup G] [TopologicalSpace G]
variable {G}

Lean source · full declaration

def dualGroupEquivAddCharCircle
    (A : Type u) [CommGroup A] [TopologicalSpace A] [DiscreteTopology A] :
    PontryaginDual A ≃ AddChar (Additive A) Circle where
  toFun := fun χ =>
    { toFun := fun a => χ a.toMul
      map_zero_eq_one' := by simp only [toMul_zero, map_one]
      map_add_eq_mul' := by
        intro a b
        exact map_mul χ a.toMul b.toMul }
  invFun := fun χ =>
    { toFun := fun a => χ (Additive.ofMul a)
      map_one' := by simp only [ofMul_one, AddChar.map_zero_eq_one]
      map_mul' := by
        intro a b
        exact χ.map_add_eq_mul (Additive.ofMul a) (Additive.ofMul b)
      continuous_toFun := continuous_of_discreteTopology }
  left_inv := by
    intro χ
    apply ContinuousMonoidHom.ext
    intro a
    rfl
  right_inv := by
    intro χ
    ext a
    rfl

theorem

dualGroup_finite_of_finite_discrete

L367 ↗

ProCGroups.Duality.dualGroup_finite_of_finite_discrete

Documentation

The Pontryagin dual of a finite discrete abelian group is finite.

Source context 6 commands

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

open scoped Topology
namespace ProCGroups.Duality
universe u v
section Basic
variable (G : Type u) [CommGroup G] [TopologicalSpace G]
variable {G}

Lean source · statement

theorem dualGroup_finite_of_finite_discrete
    (A : Type u) [CommGroup A] [TopologicalSpace A] [Finite A] [DiscreteTopology A] :
    Finite (PontryaginDual A)

theorem

card_dualGroup_eq_card_of_finite_discrete

L375 ↗

ProCGroups.Duality.card_dualGroup_eq_card_of_finite_discrete

Documentation

A finite discrete abelian group and its Pontryagin dual have the same cardinality.

Source context 6 commands

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

open scoped Topology
namespace ProCGroups.Duality
universe u v
section Basic
variable (G : Type u) [CommGroup G] [TopologicalSpace G]
variable {G}

Lean source · statement

theorem card_dualGroup_eq_card_of_finite_discrete
    (A : Type u) [CommGroup A] [TopologicalSpace A] [Finite A] [DiscreteTopology A] :
    Nat.card (PontryaginDual A) = Nat.card A

def

dualGroupEquiv

L392 ↗

ProCGroups.Duality.dualGroupEquiv

Documentation

A topological group equivalence induces an equivalence on Pontryagin duals.

Source context 6 commands

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

open scoped Topology
namespace ProCGroups.Duality
universe u v
section Basic
variable (G : Type u) [CommGroup G] [TopologicalSpace G]
variable {G}

Lean source · statement

def dualGroupEquiv
    {H : Type v} [CommGroup H] [TopologicalSpace H]
    (e : G ≃ₜ* H) :
    PontryaginDual H ≃* PontryaginDual G

def

dualGroupContinuousMulEquiv

L415 ↗

ProCGroups.Duality.dualGroupContinuousMulEquiv

Documentation

A topological group equivalence induces a continuous equivalence on Pontryagin duals.

Source context 6 commands

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

open scoped Topology
namespace ProCGroups.Duality
universe u v
section Basic
variable (G : Type u) [CommGroup G] [TopologicalSpace G]
variable {G}

Lean source · statement

def dualGroupContinuousMulEquiv
    {H : Type v} [CommGroup H] [TopologicalSpace H]
    (e : G ≃ₜ* H) :
    PontryaginDual H ≃ₜ* PontryaginDual G

theorem

dualGroupContinuousMulEquiv_toMulEquiv

L437 ↗

ProCGroups.Duality.dualGroupContinuousMulEquiv_toMulEquiv

Documentation

Forgetting topology from the dual homeomorphism gives the algebraic dual-group equivalence.

Source context 6 commands

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

open scoped Topology
namespace ProCGroups.Duality
universe u v
section Basic
variable (G : Type u) [CommGroup G] [TopologicalSpace G]
variable {G}

Lean source · statement

theorem dualGroupContinuousMulEquiv_toMulEquiv
    {H : Type v} [CommGroup H] [TopologicalSpace H]
    (e : G ≃ₜ* H) :
    (dualGroupContinuousMulEquiv (G := G) e).toMulEquiv = dualGroupEquiv (G := G) e

Module documentation

Pro C Groups / Duality

Declarations