ModuleProfiniteBidual.lean
Nyll.ProCGroups.Abelian.ProfiniteBidual
7 declarations indexed from sourceView source ↗ Module documentation
Pontryagin biduality for profinite abelian groups
Every circle-valued character factors through a finite quotient, because the circle has no subgroup contained in a sufficiently small arc. Finite duality therefore solves any finite set of evaluation equations. Compactness solves all of them simultaneously. Finite quotients also prove injectivity, giving the actual topological bidual isomorphism, including finite torsion.
Declarations
ProCGroups.Duality.exists_openNormal_le_character_ker
DocumentationA continuous circle-valued character on a profinite group kills an open normal subgroup.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open ProCGroups.ProC
namespace ProCGroups.Duality
universe u
variable {G : Type u} [CommGroup G] [TopologicalSpace G]
[IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G]
ProCGroups.Duality.exists_openNormal_le_character_kers
DocumentationA finite family of continuous characters factors through a common finite quotient.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open ProCGroups.ProC
namespace ProCGroups.Duality
universe u
variable {G : Type u} [CommGroup G] [TopologicalSpace G]
[IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G]
ProCGroups.Duality.exists_finite_evaluation
DocumentationEach finite family of bidual evaluation equations has a solution in the original group.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open ProCGroups.ProC
namespace ProCGroups.Duality
universe u
variable {G : Type u} [CommGroup G] [TopologicalSpace G]
[IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G]
ProCGroups.Duality.profinite_bidualEvaluation_surjective
DocumentationCompactness turns finite evaluation solvability into surjectivity onto the actual bidual.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open ProCGroups.ProC
namespace ProCGroups.Duality
universe u
variable {G : Type u} [CommGroup G] [TopologicalSpace G]
[IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G]
ProCGroups.Duality.profinite_bidualEvaluation_injective
DocumentationFinite quotient characters separate distinct elements of a profinite abelian group.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open ProCGroups.ProC
namespace ProCGroups.Duality
universe u
variable {G : Type u} [CommGroup G] [TopologicalSpace G]
[IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G]
ProCGroups.Duality.profiniteBidualEquiv
DocumentationA profinite abelian group is canonically isomorphic, with its actual topology, to its Pontryagin double dual. This retains all torsion.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open ProCGroups.ProC
namespace ProCGroups.Duality
universe u
variable {G : Type u} [CommGroup G] [TopologicalSpace G]
[IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G]
ProCGroups.Duality.profiniteBidualEquiv_apply
DocumentationThe bidual isomorphism is the canonical evaluation pairing.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open ProCGroups.ProC
namespace ProCGroups.Duality
universe u
variable {G : Type u} [CommGroup G] [TopologicalSpace G]
[IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G]