NYLL
Module

ProfiniteModule.lean

Nyll.ProCGroups.CompletedGroupAlgebra.UniversalProperty.ProfiniteModule
17 declarations indexed from sourceView source ↗

Module documentation

Lifts to profinite modules

Compatible lifts to all open-submodule quotients are assembled by compactness into a continuous linear map to a profinite module. This file proves existence and uniqueness and applies it to the free profinite-module property of completed group algebras.

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
def

completedGroupAlgebraLiftFiberSet

L44 ↗
CompletedGroupAlgebra.completedGroupAlgebraLiftFiberSet
Documentation

The closed fiber in a profinite target determined by the quotient-valued extension modulo one open submodule.

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 completedGroupAlgebraLiftFiberSet
    (N : ProfiniteModule.{u, w} R.toProfiniteRing)
    (f : G → N) (hf : Continuous f)
    (x : CompletedGroupAlgebraCarrier R G)
    (W : ProfiniteModuleOpenSubmodule (R := R) N) : Set N
theorem

completedGroupAlgebraLiftFiberSet_isClosed

L54 ↗
CompletedGroupAlgebra.completedGroupAlgebraLiftFiberSet_isClosed
Documentation

The quotient fiber attached to an open submodule is closed.

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 completedGroupAlgebraLiftFiberSet_isClosed
    (N : ProfiniteModule.{u, w} R.toProfiniteRing)
    (f : G → N) (hf : Continuous f)
    (x : CompletedGroupAlgebraCarrier R G)
    (W : ProfiniteModuleOpenSubmodule (R := R) N) :
    IsClosed (completedGroupAlgebraLiftFiberSet
      (R := R) (G := G) N f hf x W)
theorem

completedGroupAlgebraLiftFiberSet_finite_inter_nonempty

L73 ↗
CompletedGroupAlgebra.completedGroupAlgebraLiftFiberSet_finite_inter_nonempty
Documentation

Finite intersection property for the fibers used to assemble the profinite-target lift.

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 completedGroupAlgebraLiftFiberSet_finite_inter_nonempty
    (N : ProfiniteModule.{u, w} R.toProfiniteRing)
    (f : G → N) (hf : Continuous f)
    (x : CompletedGroupAlgebraCarrier R G)
    (s : Finset (ProfiniteModuleOpenSubmodule (R := R) N)) :
    (⋂ W ∈ s, completedGroupAlgebraLiftFiberSet
      (R := R) (G := G) N f hf x W).Nonempty
theorem

completedGroupAlgebraLiftFiberSet_iInter_nonempty

L105 ↗
CompletedGroupAlgebra.completedGroupAlgebraLiftFiberSet_iInter_nonempty
Documentation

Compactness of the profinite target gives a simultaneous lift of the compatible quotient values.

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 completedGroupAlgebraLiftFiberSet_iInter_nonempty
    (N : ProfiniteModule.{u, w} R.toProfiniteRing)
    (f : G → N) (hf : Continuous f)
    (x : CompletedGroupAlgebraCarrier R G) :
    (⋂ W : ProfiniteModuleOpenSubmodule (R := R) N,
      completedGroupAlgebraLiftFiberSet
        (R := R) (G := G) N f hf x W).Nonempty
def

completedGroupAlgebraLiftToProfiniteModuleFun

L122 ↗
CompletedGroupAlgebra.completedGroupAlgebraLiftToProfiniteModuleFun
Documentation

The assembled pointwise lift from \(\widehat{R[G]}\) to a profinite target module.

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 completedGroupAlgebraLiftToProfiniteModuleFun
    (N : ProfiniteModule.{u, w} R.toProfiniteRing)
    (f : G → N) (hf : Continuous f) :
    CompletedGroupAlgebraCarrier R G → N
theorem

completedGroupAlgebraLiftToProfiniteModuleFun_quotient

L134 ↗
CompletedGroupAlgebra.completedGroupAlgebraLiftToProfiniteModuleFun_quotient
Documentation

The assembled point maps to the prescribed quotient-valued extension modulo every open submodule.

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 completedGroupAlgebraLiftToProfiniteModuleFun_quotient
    (N : ProfiniteModule.{u, w} R.toProfiniteRing)
    (f : G → N) (hf : Continuous f)
    (W : ProfiniteModuleOpenSubmodule (R := R) N)
    (x : CompletedGroupAlgebraCarrier R G) :
    Submodule.mkQ W.1
        (completedGroupAlgebraLiftToProfiniteModuleFun
          (R := R) (G := G) N f hf x) =
      completedGroupAlgebraLiftToOpenSubmoduleQuotient
        (R := R) (G := G) N f hf W.1 W.2 x
theorem

completedGroupAlgebraLiftToProfiniteModuleFun_apply_of

L151 ↗
CompletedGroupAlgebra.completedGroupAlgebraLiftToProfiniteModuleFun_apply_of
Documentation

The assembled lift has the prescribed values on the 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 completedGroupAlgebraLiftToProfiniteModuleFun_apply_of
    (N : ProfiniteModule.{u, w} R.toProfiniteRing)
    (f : G → N) (hf : Continuous f)
    (g : G) :
    completedGroupAlgebraLiftToProfiniteModuleFun
        (R := R) (G := G) N f hf (completedGroupAlgebraOf R G g) = f g
theorem

completedGroupAlgebraLiftToProfiniteModuleFun_add

L166 ↗
CompletedGroupAlgebra.completedGroupAlgebraLiftToProfiniteModuleFun_add
Documentation

Additivity of the assembled profinite-target lift, checked after all open-submodule quotients.

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 completedGroupAlgebraLiftToProfiniteModuleFun_add
    (N : ProfiniteModule.{u, w} R.toProfiniteRing)
    (f : G → N) (hf : Continuous f)
    (x y : CompletedGroupAlgebraCarrier R G) :
    completedGroupAlgebraLiftToProfiniteModuleFun
        (R := R) (G := G) N f hf (x + y) =
      completedGroupAlgebraLiftToProfiniteModuleFun
        (R := R) (G := G) N f hf x +
      completedGroupAlgebraLiftToProfiniteModuleFun
        (R := R) (G := G) N f hf y
theorem

completedGroupAlgebraLiftToProfiniteModuleFun_smul

L191 ↗
CompletedGroupAlgebra.completedGroupAlgebraLiftToProfiniteModuleFun_smul
Documentation

The assembled profinite-target lift is compatible with scalar multiplication after all open-submodule quotients.

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 completedGroupAlgebraLiftToProfiniteModuleFun_smul
    (N : ProfiniteModule.{u, w} R.toProfiniteRing)
    (f : G → N) (hf : Continuous f)
    (r : R) (x : CompletedGroupAlgebraCarrier R G) :
    completedGroupAlgebraLiftToProfiniteModuleFun
        (R := R) (G := G) N f hf (r • x) =
      r • completedGroupAlgebraLiftToProfiniteModuleFun
        (R := R) (G := G) N f hf x
def

completedGroupAlgebraLiftToProfiniteModule

L212 ↗
CompletedGroupAlgebra.completedGroupAlgebraLiftToProfiniteModule
Documentation

Existence half of Lemma 5.3.5(d): a continuous map from the profinite group \(G\) to a profinite \(R\)-module extends to a continuous \(R\)-linear map out of \(\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 · full declaration
def completedGroupAlgebraLiftToProfiniteModule
    (N : ProfiniteModule.{u, w} R.toProfiniteRing)
    (f : G → N) (hf : Continuous f) :
    CompletedGroupAlgebraCarrier R G →L[R] N where
  toFun := completedGroupAlgebraLiftToProfiniteModuleFun (R := R) (G := G) N f hf
  map_add' := completedGroupAlgebraLiftToProfiniteModuleFun_add
    (R := R) (G := G) N f hf
  map_smul' := completedGroupAlgebraLiftToProfiniteModuleFun_smul
    (R := R) (G := G) N f hf
  cont := by
    apply continuous_of_forall_openSubmodule_quotient_continuous (R := R) N
    intro W hW
    have hEq : (fun x : CompletedGroupAlgebraCarrier R G =>
        Submodule.mkQ W
          (completedGroupAlgebraLiftToProfiniteModuleFun
            (R := R) (G := G) N f hf x)) =
        completedGroupAlgebraLiftToOpenSubmoduleQuotient
          (R := R) (G := G) N f hf W hW := by
      funext x
      exact completedGroupAlgebraLiftToProfiniteModuleFun_quotient
        (R := R) (G := G) N f hf ⟨W, hW⟩ x
    rw [hEq]
    exact (completedGroupAlgebraLiftToOpenSubmoduleQuotient
      (R := R) (G := G) N f hf W hW).continuous
theorem

completedGroupAlgebraLiftToProfiniteModule_apply_of

L239 ↗
CompletedGroupAlgebra.completedGroupAlgebraLiftToProfiniteModule_apply_of
Documentation

The profinite-target 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 completedGroupAlgebraLiftToProfiniteModule_apply_of
    (N : ProfiniteModule.{u, w} R.toProfiniteRing)
    (f : G → N) (hf : Continuous f)
    (g : G) :
    completedGroupAlgebraLiftToProfiniteModule
        (R := R) (G := G) N f hf (completedGroupAlgebraOf R G g) = f g
theorem

completedGroupAlgebra_existsUnique_lift_to_profiniteModule

L252 ↗
CompletedGroupAlgebra.completedGroupAlgebra_existsUnique_lift_to_profiniteModule
Documentation

Lemma 5.3.5(d): the completed group algebra satisfies the full universal property for maps into profinite modules.

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_profiniteModule
    (N : ProfiniteModule.{u, w} R.toProfiniteRing)
    (f : G → N) (hf : Continuous f) :
    ∃! F : CompletedGroupAlgebraCarrier R G →L[R] N,
      ∀ g : G, F (completedGroupAlgebraOf R G g) = f g
def

completedGroupAlgebraProfiniteModule

L269 ↗
CompletedGroupAlgebra.completedGroupAlgebraProfiniteModule
Documentation

The completed group algebra as an object in profinite modules over a bundled profinite coefficient ring.

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 completedGroupAlgebraProfiniteModule
    (Λ : ProfiniteCommRing.{u}) (P : ProfiniteGrp.{v}) :
    ProfiniteModule Λ.toProfiniteRing
theorem

completedGroupAlgebraOf_hasFreeLiftTo

L290 ↗
CompletedGroupAlgebra.completedGroupAlgebraOf_hasFreeLiftTo
Documentation

Cross-universe extension property for the bundled completed group algebra.

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 · full declaration
theorem completedGroupAlgebraOf_hasFreeLiftTo
    (Λ : ProfiniteCommRing.{u}) (P : ProfiniteGrp.{v})
    (N : ProfiniteModule.{u, w} Λ.toProfiniteRing) :
    ProfiniteModule.HasFreeLiftTo
      (completedGroupAlgebraProfiniteModule Λ P)
      P.toProfinite (fun g => by
        change CompletedGroupAlgebraCarrier Λ P
        exact completedGroupAlgebraOf Λ P g) N := by
  let : Module Λ N := N.module
  dsimp [ProfiniteModule.HasFreeLiftTo, completedGroupAlgebraProfiniteModule,
    ProfiniteCommRing.toProfiniteRing]
  exact completedGroupAlgebra_existsUnique_lift_to_profiniteModule
    (R := Λ) (G := P) N
theorem

completedGroupAlgebraOf_freeProfiniteModule

L308 ↗
CompletedGroupAlgebra.completedGroupAlgebraOf_freeProfiniteModule
Documentation

Ribes--Zalesskii Lemma 5.3.5(d): \(\widehat{R[G]}\) is the free profinite \(R\)-module on the profinite space G, with basis map \(g\mapsto [g]\) inside the completed group algebra.

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 · full declaration
theorem completedGroupAlgebraOf_freeProfiniteModule
    (Λ : ProfiniteCommRing.{u}) (P : ProfiniteGrp.{v}) :
    (completedGroupAlgebraProfiniteModule Λ P).IsFreeOn
      P.toProfinite (fun g => by
        change CompletedGroupAlgebraCarrier Λ P
        exact completedGroupAlgebraOf Λ P g) := by
  refine ⟨continuous_completedGroupAlgebraOf (R := Λ) (G := P), ?_, ?_⟩
  · dsimp [completedGroupAlgebraProfiniteModule, ProfiniteCommRing.toProfiniteRing]
    exact completedGroupAlgebraOf_dense_span (R := Λ) (G := P)
  · intro N
    exact completedGroupAlgebraOf_hasFreeLiftTo Λ P N

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