NYLL
Module

FiniteQuotient.lean

Nyll.ProCGroups.CompletedGroupAlgebra.UniversalProperty.FiniteQuotient
9 declarations indexed from sourceView source ↗

Module documentation

Lifts to finite and discrete quotients

Maps from the algebraic group algebra that factor through a finite stage extend uniquely from the completion. This file constructs those lifts, specializes them to discrete modules, and proves joint injectivity of the finite-stage projections.

Imports1
Imported by2

Declarations

def

completedGroupAlgebraLiftOfFiniteQuotient

L38 ↗
CompletedGroupAlgebra.completedGroupAlgebraLiftOfFiniteQuotient
Documentation

Finite-quotient construction used in Lemma 5.3.5(d): a map on one finite quotient \(G/U\) extends linearly and continuously from \(\widehat{R[G]}\).

Source context 10 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
Lean source · statement
def completedGroupAlgebraLiftOfFiniteQuotient
    (U : CompletedGroupAlgebraIndex G) (N : Type w)
    [AddCommGroup N] [TopologicalSpace N] [Module R N] [ContinuousAdd N]
    [ContinuousSMul R N] (f : CompletedGroupAlgebraQuotient G U → N) :
    CompletedGroupAlgebraCarrier R G →L[R] N
theorem

completedGroupAlgebraLiftOfFiniteQuotient_apply_of

L51 ↗
CompletedGroupAlgebra.completedGroupAlgebraLiftOfFiniteQuotient_apply_of
Documentation

The finite-quotient lift has the prescribed value on completed group-like elements.

Source context 11 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
omit [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] in
Lean source · statement
theorem completedGroupAlgebraLiftOfFiniteQuotient_apply_of
    (U : CompletedGroupAlgebraIndex G) (N : Type w)
    [AddCommGroup N] [TopologicalSpace N] [Module R N] [ContinuousAdd N]
    [ContinuousSMul R N] (f : CompletedGroupAlgebraQuotient G U → N) (g : G) :
    completedGroupAlgebraLiftOfFiniteQuotient (R := R) (G := G) U N f
        (completedGroupAlgebraOf R G g) =
      f (openNormalSubgroupInClassProj
        (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U g)
theorem

completedGroupAlgebra_existsUnique_lift_of_factors

L75 ↗
CompletedGroupAlgebra.completedGroupAlgebra_existsUnique_lift_of_factors
Documentation

If a continuous target map already factors through one finite quotient \(G/U\), the finite-quotient construction gives the required unique continuous linear extension.

Source context 11 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
omit [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] in
Lean source · statement
theorem completedGroupAlgebra_existsUnique_lift_of_factors
    (N : Type w) [AddCommGroup N] [TopologicalSpace N] [Module R N]
    [ContinuousAdd N] [ContinuousSMul R N] [T2Space N]
    (U : CompletedGroupAlgebraIndex G) (f : G → N)
    (fbar : CompletedGroupAlgebraQuotient G U → N)
    (hfac : ∀ g : G,
      fbar (openNormalSubgroupInClassProj
        (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U g) = f g) :
    ∃! F : CompletedGroupAlgebraCarrier R G →L[R] N,
      ∀ g : G, F (completedGroupAlgebraOf R G g) = f g
theorem

exists_completedGroupAlgebraIndex_factor_continuous_discrete

L99 ↗
CompletedGroupAlgebra.exists_completedGroupAlgebraIndex_factor_continuous_discrete
Documentation

A continuous map from a profinite group to a discrete space is unchanged on the cosets of some finite open normal quotient, providing the topological factorization input for Lemma 5.3.5(d).

Source context 11 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
omit [T2Space G] in
Lean source · statement
theorem exists_completedGroupAlgebraIndex_factor_continuous_discrete
    (N : Type w) [TopologicalSpace N] [DiscreteTopology N]
    (f : G → N) (hf : Continuous f) :
    ∃ U : CompletedGroupAlgebraIndex G, ∃ fbar : CompletedGroupAlgebraQuotient G U → N,
      ∀ g : G,
        fbar (openNormalSubgroupInClassProj
          (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U g) = f g
theorem

completedGroupAlgebra_existsUnique_lift_to_discreteModule

L151 ↗
CompletedGroupAlgebra.completedGroupAlgebra_existsUnique_lift_to_discreteModule
Documentation

Discrete-target form of Lemma 5.3.5(d): a continuous map from the profinite group \(G\) to a discrete \(R\)-module extends uniquely to a continuous \(R\)-linear map out of \(\widehat{R[G]}\).

Source context 11 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
omit [T2Space G] in
Lean source · statement
theorem completedGroupAlgebra_existsUnique_lift_to_discreteModule
    (N : Type w) [AddCommGroup N] [TopologicalSpace N] [Module R N]
    [ContinuousAdd N] [ContinuousSMul R N] [DiscreteTopology N]
    (f : G → N) (hf : Continuous f) :
    ∃! F : CompletedGroupAlgebraCarrier R G →L[R] N,
      ∀ g : G, F (completedGroupAlgebraOf R G g) = f g
def

completedGroupAlgebraLiftToDiscreteModule

L164 ↗
CompletedGroupAlgebra.completedGroupAlgebraLiftToDiscreteModule
Documentation

The discrete-target extension used in Lemma 5.3.5(d).

Source context 10 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
Lean source · statement
def completedGroupAlgebraLiftToDiscreteModule
    (N : Type w) [AddCommGroup N] [TopologicalSpace N] [Module R N]
    [ContinuousAdd N] [ContinuousSMul R N] [DiscreteTopology N]
    (f : G → N) (hf : Continuous f) :
    CompletedGroupAlgebraCarrier R G →L[R] N
theorem

completedGroupAlgebraLiftToDiscreteModule_apply_of

L176 ↗
CompletedGroupAlgebra.completedGroupAlgebraLiftToDiscreteModule_apply_of
Documentation

The chosen discrete-target lift has the prescribed value on completed group-like elements.

Source context 11 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
omit [T2Space G] in
Lean source · statement
theorem completedGroupAlgebraLiftToDiscreteModule_apply_of
    (N : Type w) [AddCommGroup N] [TopologicalSpace N] [Module R N]
    [ContinuousAdd N] [ContinuousSMul R N] [DiscreteTopology N]
    (f : G → N) (hf : Continuous f) (g : G) :
    completedGroupAlgebraLiftToDiscreteModule
        (R := R) (G := G) N f hf
        (completedGroupAlgebraOf R G g) = f g
theorem

ext_of_stageProjection_eq

L194 ↗
CompletedGroupAlgebra.CompletedGroupAlgebraModel.ext_of_stageProjection_eq
Documentation

Elements of a bundled completed-group-algebra model are determined by all of their finite-stage projections. This is the public finite-quotient extensionality principle for arbitrary models, not only for the concrete compatible-family carrier.

Source context 12 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
namespace CompletedGroupAlgebraModel
variable {R : ProfiniteCommRing.{u}} {G : ProfiniteGrp.{v}}
Lean source · statement
theorem ext_of_stageProjection_eq (M : CompletedGroupAlgebraModel R G)
    {x y : M.carrier}
    (h : ∀ U : CompletedGroupAlgebraIndex G,
      M.stageProjection U x = M.stageProjection U y) :
    x = y
theorem

stageProjection_jointly_injective

L205 ↗
CompletedGroupAlgebra.CompletedGroupAlgebraModel.stageProjection_jointly_injective
Documentation

The family of finite-stage projections of any bundled model is jointly injective.

Source context 12 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
namespace CompletedGroupAlgebraModel
variable {R : ProfiniteCommRing.{u}} {G : ProfiniteGrp.{v}}
Lean source · full declaration
theorem stageProjection_jointly_injective (M : CompletedGroupAlgebraModel R G) :
    Function.Injective (fun x : M.carrier => fun U => M.stageProjection U x) := by
  intro x y hxy
  apply M.ext_of_stageProjection_eq
  intro U
  exact congrFun hxy U

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.