Module

ProfiniteCompletionCriteria.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Infinite.ProfiniteCompletionCriteria

3 declarations indexed from sourceView source ↗

Module documentation

Bijectivity criteria for maps out of the open-quotient completion

The universal lift to a profinite target is onto when the original map has dense range. It is one-to-one when pullbacks of open normal subgroups of the target are cofinal among the defining open finite-index normal subgroups of the source. These criteria isolate the purely topological part of infinite local reciprocity from the arithmetic existence theorem.

Imports1

Nyll.ClassFieldTheory.LocalClassFieldTheory.Infinite.ProfiniteCompletion

Imported by2

theorem

topologicalProfiniteCompletionFiniteQuotientMap_injective

L33 ↗

LocalClassFieldTheory.topologicalProfiniteCompletionFiniteQuotientMap_injective

Documentation

Quotienting by the exact pullback of an open normal subgroup gives an injective map to the corresponding finite quotient of the target.

Source context 5 commands

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

noncomputable section
open CategoryTheory
namespace LocalClassFieldTheory
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]

Lean source · statement

theorem topologicalProfiniteCompletionFiniteQuotientMap_injective
    (P : ProfiniteGrp.{u}) (f : G →ₜ* P) (N : OpenNormalSubgroup P) :
    Function.Injective
      (topologicalProfiniteCompletionFiniteQuotientMap P f N)

theorem

topologicalProfiniteCompletionLift_surjective_of_denseRange

L51 ↗

LocalClassFieldTheory.topologicalProfiniteCompletionLift_surjective_of_denseRange

Documentation

Dense range of the original map implies surjectivity of its canonical extension from the open-quotient completion.

Source context 6 commands

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

noncomputable section
open CategoryTheory
namespace LocalClassFieldTheory
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
variable [IsTopologicalGroup G]

Lean source · statement

theorem topologicalProfiniteCompletionLift_surjective_of_denseRange
    (P : ProfiniteGrp.{u}) (f : G →ₜ* P) (hf : DenseRange f) :
    Function.Surjective (topologicalProfiniteCompletionLift P f)

theorem

topologicalProfiniteCompletionLift_injective_of_preimage_cofinal

L68 ↗

LocalClassFieldTheory.topologicalProfiniteCompletionLift_injective_of_preimage_cofinal

Documentation

Cofinality of pulled-back target quotients implies injectivity of the canonical lift from the open-quotient completion.

Source context 6 commands

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

noncomputable section
open CategoryTheory
namespace LocalClassFieldTheory
universe u
variable {G : Type u} [Group G] [TopologicalSpace G]
variable [IsTopologicalGroup G]

Lean source · statement

theorem topologicalProfiniteCompletionLift_injective_of_preimage_cofinal
    (P : ProfiniteGrp.{u}) (f : G →ₜ* P)
    (hcofinal : ∀ H : OpenFiniteIndexNormalSubgroup G,
      ∃ N : OpenNormalSubgroup P,
        topologicalProfiniteCompletionPreimageIndex P f N ≤ H) :
    Function.Injective (topologicalProfiniteCompletionLift P f)

Module documentation

Bijectivity criteria for maps out of the open-quotient completion

Declarations

topologicalProfiniteCompletionFiniteQuotientMap_injective

topologicalProfiniteCompletionLift_surjective_of_denseRange

topologicalProfiniteCompletionLift_injective_of_preimage_cofinal