NYLL
Module

OpenSubmoduleQuotient.lean

Nyll.ProCGroups.CompletedGroupAlgebra.UniversalProperty.OpenSubmoduleQuotient
6 declarations indexed from sourceView source ↗

Module documentation

Lifts to open-submodule quotients

The finite-quotient universal property yields a unique continuous linear lift to the quotient of a profinite module by an open submodule. This file constructs the lift and records its value on group-like generators and its factorization formula.

Imports1
Imported by2

Declarations

instance

(anonymous instance)

L33 ↗
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 : ProfiniteCommRing.{u})
variable (G : ProfiniteGrp.{v})
Lean source · statement
instance (N : ProfiniteModule.{u, w} R.toProfiniteRing) : Module R N
instance

(anonymous instance)

L36 ↗
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 : ProfiniteCommRing.{u})
variable (G : ProfiniteGrp.{v})
local instance (N : ProfiniteModule.{u, w} R.toProfiniteRing) : Module R N :=
  N.module
Lean source · statement
instance (N : ProfiniteModule.{u, w} R.toProfiniteRing) :
    ContinuousSMul R N
theorem

completedGroupAlgebra_existsUnique_lift_to_openSubmoduleQuotient

L45 ↗
CompletedGroupAlgebra.completedGroupAlgebra_existsUnique_lift_to_openSubmoduleQuotient
Documentation

The quotient-target form of the existence step in Lemma 5.3.5(d): after quotienting a profinite target module by an open submodule, the prescribed continuous map from \(G\) extends uniquely from \(\widehat{R[G]}\).

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 : ProfiniteCommRing.{u})
variable (G : ProfiniteGrp.{v})
local instance (N : ProfiniteModule.{u, w} R.toProfiniteRing) : Module R N :=
  N.module
local instance (N : ProfiniteModule.{u, w} R.toProfiniteRing) :
    ContinuousSMul R N :=
  N.continuousSMul
Lean source · statement
theorem completedGroupAlgebra_existsUnique_lift_to_openSubmoduleQuotient
    (N : ProfiniteModule.{u, w} R.toProfiniteRing)
    (f : G → N) (hf : Continuous f)
    (W : Submodule R N) (hW : IsOpen (W : Set N)) :
    ∃! F : CompletedGroupAlgebraCarrier R G →L[R] N ⧸ W,
      ∀ g : G, F (completedGroupAlgebraOf R G g) = Submodule.mkQ W (f g)
def

completedGroupAlgebraLiftToOpenSubmoduleQuotient

L67 ↗
CompletedGroupAlgebra.completedGroupAlgebraLiftToOpenSubmoduleQuotient
Documentation

The chosen quotient-valued extension attached to an open submodule of a profinite target.

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 : ProfiniteCommRing.{u})
variable (G : ProfiniteGrp.{v})
local instance (N : ProfiniteModule.{u, w} R.toProfiniteRing) : Module R N :=
  N.module
local instance (N : ProfiniteModule.{u, w} R.toProfiniteRing) :
    ContinuousSMul R N :=
  N.continuousSMul
Lean source · statement
def completedGroupAlgebraLiftToOpenSubmoduleQuotient
    (N : ProfiniteModule.{u, w} R.toProfiniteRing)
    (f : G → N) (hf : Continuous f)
    (W : Submodule R N) (hW : IsOpen (W : Set N)) :
    CompletedGroupAlgebraCarrier R G →L[R] N ⧸ W
theorem

completedGroupAlgebraLiftToOpenSubmoduleQuotient_apply_of

L78 ↗
CompletedGroupAlgebra.completedGroupAlgebraLiftToOpenSubmoduleQuotient_apply_of
Documentation

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

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 : ProfiniteCommRing.{u})
variable (G : ProfiniteGrp.{v})
local instance (N : ProfiniteModule.{u, w} R.toProfiniteRing) : Module R N :=
  N.module
local instance (N : ProfiniteModule.{u, w} R.toProfiniteRing) :
    ContinuousSMul R N :=
  N.continuousSMul
Lean source · statement
theorem completedGroupAlgebraLiftToOpenSubmoduleQuotient_apply_of
    (N : ProfiniteModule.{u, w} R.toProfiniteRing)
    (f : G → N) (hf : Continuous f)
    (W : Submodule R N) (hW : IsOpen (W : Set N)) (g : G) :
    completedGroupAlgebraLiftToOpenSubmoduleQuotient
        (R := R) (G := G) N f hf W hW
        (completedGroupAlgebraOf R G g) =
      Submodule.mkQ W (f g)
theorem

completedGroupAlgebraLiftToOpenSubmoduleQuotient_factor

L91 ↗
CompletedGroupAlgebra.completedGroupAlgebraLiftToOpenSubmoduleQuotient_factor
Documentation

The quotient-valued extensions are compatible with refinement of open submodules.

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 : ProfiniteCommRing.{u})
variable (G : ProfiniteGrp.{v})
local instance (N : ProfiniteModule.{u, w} R.toProfiniteRing) : Module R N :=
  N.module
local instance (N : ProfiniteModule.{u, w} R.toProfiniteRing) :
    ContinuousSMul R N :=
  N.continuousSMul
Lean source · statement
theorem completedGroupAlgebraLiftToOpenSubmoduleQuotient_factor
    (N : ProfiniteModule.{u, w} R.toProfiniteRing)
    (f : G → N) (hf : Continuous f)
    {W V : Submodule R N} (hWV : W ≤ V)
    (hW : IsOpen (W : Set N)) (hV : IsOpen (V : Set N))
    (x : CompletedGroupAlgebraCarrier R G) :
    Submodule.factor hWV
        (completedGroupAlgebraLiftToOpenSubmoduleQuotient
          (R := R) (G := G) N f hf W hW x) =
      completedGroupAlgebraLiftToOpenSubmoduleQuotient
        (R := R) (G := G) N f hf V hV x

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