Module

AugmentationIdeal.lean

Nyll.ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.AugmentationIdeal

20 declarations indexed from sourceView source ↗

Module documentation

Fox differential: completed — coefficient rings — mod-\(n\) completed group algebra —

augmentation ideal

The principal declarations in this module are:

modNCompletedGroupAlgebraStageAugmentationIdeal

The augmentation ideal on one residue-coefficient finite stage.

modNCompletedGroupAlgebraAugmentationKernel

The kernel of the canonical augmentation on the residue-coefficient completed group algebra.

mem_modNCompletedGroupAlgebraStageAugmentationIdeal_iff

Membership in a mod-\(N\) finite-stage augmentation ideal is equivalent to vanishing under the stage augmentation map.

mem_modNCompletedGroupAlgebraAugmentationKernel_iff

Membership in the relevant augmentation kernel or augmentation ideal is equivalent to the corresponding vanishing condition.

Imports1

Nyll.ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.Augmentation

Imported by2

def

modNCompletedGroupAlgebraStageAugmentationIdeal

L46 ↗

FoxDifferential.modNCompletedGroupAlgebraStageAugmentationIdeal

Documentation

The augmentation ideal on one residue-coefficient finite stage.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
section AugmentationIdeal
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

def modNCompletedGroupAlgebraStageAugmentationIdeal (U :
    _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) :
    Ideal (ModNCompletedGroupAlgebraStage n G U)

def

modNCompletedGroupAlgebraAugmentationKernel

L52 ↗

FoxDifferential.modNCompletedGroupAlgebraAugmentationKernel

Documentation

The kernel of the canonical augmentation on the residue-coefficient completed group algebra.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
section AugmentationIdeal
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

def modNCompletedGroupAlgebraAugmentationKernel :
    Set (ModNCompletedGroupAlgebra n G)

abbrev

ModNCompletedGroupAlgebraAugmentationKernel

L57 ↗

FoxDifferential.ModNCompletedGroupAlgebraAugmentationKernel

Documentation

The kernel of the canonical augmentation is viewed as a subtype.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
section AugmentationIdeal
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

abbrev ModNCompletedGroupAlgebraAugmentationKernel

theorem

mem_modNCompletedGroupAlgebraStageAugmentationIdeal_iff

L67 ↗

FoxDifferential.mem_modNCompletedGroupAlgebraStageAugmentationIdeal_iff

Documentation

Membership in a mod-\(N\) finite-stage augmentation ideal is equivalent to vanishing under the stage augmentation map.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
section AugmentationIdeal
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {n G} in

Lean source · statement

theorem mem_modNCompletedGroupAlgebraStageAugmentationIdeal_iff
    {U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G} {x :
        ModNCompletedGroupAlgebraStage n G U} :
    x ∈ modNCompletedGroupAlgebraStageAugmentationIdeal n G U ↔
      modNCompletedGroupAlgebraStageAugmentation n G U x = 0

theorem

mem_modNCompletedGroupAlgebraAugmentationKernel_iff

L81 ↗

FoxDifferential.mem_modNCompletedGroupAlgebraAugmentationKernel_iff

Documentation

Membership in the relevant augmentation kernel or augmentation ideal is equivalent to the corresponding vanishing condition.

Source context 12 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
section AugmentationIdeal
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {n G} in
variable {n G} in

Lean source · statement

theorem mem_modNCompletedGroupAlgebraAugmentationKernel_iff
    {x : ModNCompletedGroupAlgebra n G} :
    x ∈ modNCompletedGroupAlgebraAugmentationKernel n G ↔
      modNCompletedGroupAlgebraAugmentation n G x = 0

theorem

mem_modNCompletedGroupAlgebraProjection_stageAugmentationIdeal_iff

L94 ↗

FoxDifferential.mem_modNCompletedGroupAlgebraProjection_stageAugmentationIdeal_iff

Documentation

A mod-\(N\) completed group-algebra element projects into the stage augmentation ideal iff it lies in the completed augmentation kernel.

Source context 13 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
section AugmentationIdeal
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {n G} in
variable {n G} in
variable {n G} in

Lean source · statement

theorem mem_modNCompletedGroupAlgebraProjection_stageAugmentationIdeal_iff
    {U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G} {x :
        ModNCompletedGroupAlgebra n G} :
    modNCompletedGroupAlgebraProjection n G U x ∈
        modNCompletedGroupAlgebraStageAugmentationIdeal n G U ↔
      x ∈ modNCompletedGroupAlgebraAugmentationKernel n G

def

modNCompletedGroupAlgebraStageAugmentationIdealTransition

L107 ↗

FoxDifferential.modNCompletedGroupAlgebraStageAugmentationIdealTransition

Documentation

The transition maps on the residue-coefficient finite-stage augmentation ideals.

Source context 13 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
section AugmentationIdeal
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {n G} in
variable {n G} in
variable {n G} in

Lean source · statement

def modNCompletedGroupAlgebraStageAugmentationIdealTransition
    {U V : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G} (hUV : U ≤ V) :
    modNCompletedGroupAlgebraStageAugmentationIdeal n G V →
      modNCompletedGroupAlgebraStageAugmentationIdeal n G U

theorem

modNCompletedGroupAlgebraStageAugmentationIdealTransition_val

L129 ↗

FoxDifferential.modNCompletedGroupAlgebraStageAugmentationIdealTransition_val

Documentation

The transition map between finite-stage augmentation ideals is evaluated by the corresponding stage transition.

Source context 14 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
section AugmentationIdeal
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {n G} in
variable {n G} in
variable {n G} in
omit [Fact (0 < n)] in

Lean source · statement

theorem modNCompletedGroupAlgebraStageAugmentationIdealTransition_val
    {U V : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G} (hUV : U ≤ V)
    (x : modNCompletedGroupAlgebraStageAugmentationIdeal n G V) :
    ((modNCompletedGroupAlgebraStageAugmentationIdealTransition
        (n := n) (G := G) hUV x : modNCompletedGroupAlgebraStageAugmentationIdeal n G U) :
      ModNCompletedGroupAlgebraStage n G U) =
      modNCompletedGroupAlgebraTransition n G hUV x.1

def

modNCompletedGroupAlgebraAugmentationIdealSystem

L138 ↗

FoxDifferential.modNCompletedGroupAlgebraAugmentationIdealSystem

Documentation

The inverse system of residue-coefficient finite-stage augmentation ideals.

Source context 13 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
section AugmentationIdeal
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {n G} in
variable {n G} in
variable {n G} in

Lean source · full declaration

def modNCompletedGroupAlgebraAugmentationIdealSystem :
    InverseSystem (I := _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) where
  X := fun U => ↥(modNCompletedGroupAlgebraStageAugmentationIdeal n G U)
  topologicalSpace := fun _ => ⊥
  map := fun {U V} hUV => modNCompletedGroupAlgebraStageAugmentationIdealTransition
    (n := n) (G := G) hUV
  continuous_map := by
    intro U V hUV
    let : TopologicalSpace (modNCompletedGroupAlgebraStageAugmentationIdeal n G U) := ⊥
    let : TopologicalSpace (modNCompletedGroupAlgebraStageAugmentationIdeal n G V) := ⊥
    let : DiscreteTopology (modNCompletedGroupAlgebraStageAugmentationIdeal n G V) := ⟨rfl⟩
    exact continuous_of_discreteTopology
  map_id := by
    intro U
    funext x
    apply Subtype.ext
    exact congrFun
      (congrArg DFunLike.coe (modNCompletedGroupAlgebraTransition_id (n := n) (G := G) U))
      x.1
  map_comp := by
    intro U V W hUV hVW
    funext x
    apply Subtype.ext
    exact congrFun
      (congrArg DFunLike.coe
        (modNCompletedGroupAlgebraTransition_comp (n := n) (G := G) hUV hVW))
      x.1

abbrev

ModNCompletedGroupAlgebraAugmentationIdeal

L167 ↗

FoxDifferential.ModNCompletedGroupAlgebraAugmentationIdeal

Documentation

The inverse-limit object of the residue-coefficient finite-stage augmentation ideals.

Source context 13 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
section AugmentationIdeal
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {n G} in
variable {n G} in
variable {n G} in

Lean source · statement

abbrev ModNCompletedGroupAlgebraAugmentationIdeal

abbrev

modNCompletedGroupAlgebraAugmentationIdealProjection

L171 ↗

FoxDifferential.modNCompletedGroupAlgebraAugmentationIdealProjection

Documentation

The projection from the residue-coefficient augmentation-ideal inverse limit to one stage.

Source context 13 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
section AugmentationIdeal
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {n G} in
variable {n G} in
variable {n G} in

Lean source · statement

abbrev modNCompletedGroupAlgebraAugmentationIdealProjection (U :
    _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) :
    ModNCompletedGroupAlgebraAugmentationIdeal n G →
      modNCompletedGroupAlgebraStageAugmentationIdeal n G U

def

toModNCompletedGroupAlgebraAugmentationIdeal

L181 ↗

FoxDifferential.toModNCompletedGroupAlgebraAugmentationIdeal

Documentation

A residue-coefficient augmentation-kernel point determines a compatible family in the finite-stage augmentation ideals.

Source context 13 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
section AugmentationIdeal
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {n G} in
variable {n G} in
variable {n G} in

Lean source · statement

def toModNCompletedGroupAlgebraAugmentationIdeal :
    ModNCompletedGroupAlgebraAugmentationKernel n G →
      ModNCompletedGroupAlgebraAugmentationIdeal n G

theorem

modNCompletedGroupAlgebraAugmentationIdealProjection_to

L200 ↗

FoxDifferential.modNCompletedGroupAlgebraAugmentationIdealProjection_to

Documentation

The projection-to-stage map is one direction of the completed augmentation-ideal stage equivalence.

Source context 14 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
section AugmentationIdeal
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {n G} in
variable {n G} in
variable {n G} in
omit [Fact (0 < n)] in

Lean source · statement

theorem modNCompletedGroupAlgebraAugmentationIdealProjection_to
    (x : ModNCompletedGroupAlgebraAugmentationKernel n G) (U :
        _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) :
    ((modNCompletedGroupAlgebraAugmentationIdealProjection (n := n) (G := G) U
        (toModNCompletedGroupAlgebraAugmentationIdeal (n := n) (G := G) x)) :
      ModNCompletedGroupAlgebraStage n G U) =
      modNCompletedGroupAlgebraProjection n G U x.1

def

ofModNCompletedGroupAlgebraAugmentationIdeal

L212 ↗

FoxDifferential.ofModNCompletedGroupAlgebraAugmentationIdeal

Documentation

A compatible family of finite-stage augmentation-ideal elements determines a residue-coefficient completed augmentation-kernel point.

Source context 13 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
section AugmentationIdeal
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {n G} in
variable {n G} in
variable {n G} in

Lean source · statement

def ofModNCompletedGroupAlgebraAugmentationIdeal :
    ModNCompletedGroupAlgebraAugmentationIdeal n G →
      ModNCompletedGroupAlgebraAugmentationKernel n G

theorem

modNCompletedGroupAlgebraProjection_ofAugmentationIdeal

L240 ↗

FoxDifferential.modNCompletedGroupAlgebraProjection_ofAugmentationIdeal

Documentation

Projecting an element of the completed augmentation ideal gives its corresponding finite-stage augmentation-ideal coordinate.

Source context 14 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
section AugmentationIdeal
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {n G} in
variable {n G} in
variable {n G} in
omit [Fact (0 < n)] in

Lean source · statement

theorem modNCompletedGroupAlgebraProjection_ofAugmentationIdeal
    (x : ModNCompletedGroupAlgebraAugmentationIdeal n G) (U :
        _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) :
    modNCompletedGroupAlgebraProjection n G U
        (ofModNCompletedGroupAlgebraAugmentationIdeal (n := n) (G := G) x).1 =
      ((modNCompletedGroupAlgebraAugmentationIdealProjection (n := n) (G := G) U x) :
        ModNCompletedGroupAlgebraStage n G U)

theorem

ofModNCompletedGroupAlgebraAugmentationIdeal_to

L254 ↗

FoxDifferential.ofModNCompletedGroupAlgebraAugmentationIdeal_to

Documentation

The completion-to-stage map is one direction of the completed augmentation-ideal stage equivalence.

Source context 14 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
section AugmentationIdeal
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {n G} in
variable {n G} in
variable {n G} in
omit [Fact (0 < n)] in

Lean source · statement

theorem ofModNCompletedGroupAlgebraAugmentationIdeal_to
    (x : ModNCompletedGroupAlgebraAugmentationKernel n G) :
    ofModNCompletedGroupAlgebraAugmentationIdeal (n := n) (G := G)
        (toModNCompletedGroupAlgebraAugmentationIdeal (n := n) (G := G) x) = x

theorem

toModNCompletedGroupAlgebraAugmentationIdeal_of

L269 ↗

FoxDifferential.toModNCompletedGroupAlgebraAugmentationIdeal_of

Documentation

The stage-to-completion map is one direction of the completed augmentation-ideal stage equivalence.

Source context 14 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
section AugmentationIdeal
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {n G} in
variable {n G} in
variable {n G} in
omit [Fact (0 < n)] in

Lean source · statement

theorem toModNCompletedGroupAlgebraAugmentationIdeal_of
    (x : ModNCompletedGroupAlgebraAugmentationIdeal n G) :
    toModNCompletedGroupAlgebraAugmentationIdeal (n := n) (G := G)
        (ofModNCompletedGroupAlgebraAugmentationIdeal (n := n) (G := G) x) = x

def

modNCompletedGroupAlgebraAugmentationKernelEquivInverseLimit

L282 ↗

FoxDifferential.modNCompletedGroupAlgebraAugmentationKernelEquivInverseLimit

Documentation

The residue-coefficient completed augmentation kernel is canonically equivalent to the inverse limit of the finite-stage augmentation ideals.

Source context 13 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
section AugmentationIdeal
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {n G} in
variable {n G} in
variable {n G} in

Lean source · full declaration

def modNCompletedGroupAlgebraAugmentationKernelEquivInverseLimit :
    ModNCompletedGroupAlgebraAugmentationKernel n G ≃
      ModNCompletedGroupAlgebraAugmentationIdeal n G where
  toFun := toModNCompletedGroupAlgebraAugmentationIdeal (n := n) (G := G)
  invFun := ofModNCompletedGroupAlgebraAugmentationIdeal (n := n) (G := G)
  left_inv := ofModNCompletedGroupAlgebraAugmentationIdeal_to (n := n) (G := G)
  right_inv := toModNCompletedGroupAlgebraAugmentationIdeal_of (n := n) (G := G)

theorem

modNCompletedGroupAlgebraAugmentationKernelEquivInverseLimit_apply

L296 ↗

FoxDifferential.modNCompletedGroupAlgebraAugmentationKernelEquivInverseLimit_apply

Documentation

The forward mod-\(n\) augmentation-kernel equivalence is the canonical map to the inverse-limit augmentation ideal.

Source context 14 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
section AugmentationIdeal
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {n G} in
variable {n G} in
variable {n G} in
omit [Fact (0 < n)] in

Lean source · statement

theorem modNCompletedGroupAlgebraAugmentationKernelEquivInverseLimit_apply
    (x : ModNCompletedGroupAlgebraAugmentationKernel n G) :
    modNCompletedGroupAlgebraAugmentationKernelEquivInverseLimit (n := n) (G := G) x =
      toModNCompletedGroupAlgebraAugmentationIdeal (n := n) (G := G) x

theorem

modNCompletedGroupAlgebraAugmentationKernelEquivInverseLimit_symm_apply

L307 ↗

FoxDifferential.modNCompletedGroupAlgebraAugmentationKernelEquivInverseLimit_symm_apply

Documentation

The inverse mod-\(n\) augmentation-kernel equivalence reconstructs a kernel element from an inverse-limit augmentation-ideal element.

Source context 14 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
section AugmentationIdeal
variable (n : ℕ) [Fact (0 < n)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {n G} in
variable {n G} in
variable {n G} in
omit [Fact (0 < n)] in

Lean source · statement

theorem modNCompletedGroupAlgebraAugmentationKernelEquivInverseLimit_symm_apply
    (x : ModNCompletedGroupAlgebraAugmentationIdeal n G) :
    (modNCompletedGroupAlgebraAugmentationKernelEquivInverseLimit (n := n) (G := G)).symm x =
      ofModNCompletedGroupAlgebraAugmentationIdeal (n := n) (G := G) x

Module documentation

Fox differential: completed — coefficient rings — mod-\(n\) completed group algebra —

Declarations