Module

Identity.lean

Nyll.ProCGroups.FoxDifferential.Completed.DifferentialModule.Identity

11 declarations indexed from sourceView source ↗

Module documentation

Fox differential: completed — differential module — identity

The principal declarations in this module are:

identityCompletedGroupAlgebraOpenSubgroup

The identity completed-group-algebra open subgroup used for the identity quotient stage.

identityCompletedGroupAlgebraOpenNormalSubgroup

The identity open normal subgroup of a discrete group.

identityCompletedGroupAlgebraOpenNormalSubgroup_coe

The identity completed-group-algebra open normal subgroup coerces to the corresponding open subgroup.

openNormalSubgroupInClassProj_identityCompletedGroupAlgebraIndex_injective

The projection to the identity completed stage is injective on group elements.

Imports1

Nyll.ProCGroups.FoxDifferential.Completed.FiniteStage.Bifiltered.InverseSystem

Imported by3

def

identityCompletedGroupAlgebraOpenSubgroup

L39 ↗

FoxDifferential.identityCompletedGroupAlgebraOpenSubgroup

Documentation

The identity completed-group-algebra open subgroup used for the identity quotient stage.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups
open ProCGroups.ProC
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

def identityCompletedGroupAlgebraOpenSubgroup
    (G : Type u) [Group G] [TopologicalSpace G] [DiscreteTopology G] :
    OpenSubgroup G

def

identityCompletedGroupAlgebraOpenNormalSubgroup

L45 ↗

FoxDifferential.identityCompletedGroupAlgebraOpenNormalSubgroup

Documentation

The identity open normal subgroup of a discrete group.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups
open ProCGroups.ProC
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

def identityCompletedGroupAlgebraOpenNormalSubgroup
    (G : Type u) [Group G] [TopologicalSpace G] [DiscreteTopology G] :
    OpenNormalSubgroup G

theorem

identityCompletedGroupAlgebraOpenNormalSubgroup_coe

L61 ↗

FoxDifferential.identityCompletedGroupAlgebraOpenNormalSubgroup_coe

Documentation

The identity completed-group-algebra open normal subgroup coerces to the corresponding open subgroup.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups
open ProCGroups.ProC
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem identityCompletedGroupAlgebraOpenNormalSubgroup_coe
    (G : Type u) [Group G] [TopologicalSpace G] [DiscreteTopology G] :
    ((identityCompletedGroupAlgebraOpenNormalSubgroup G : OpenNormalSubgroup G) :
        Subgroup G) = ⊥

def

identityCompletedGroupAlgebraSubgroupInClass

L69 ↗

FoxDifferential.identityCompletedGroupAlgebraSubgroupInClass

Documentation

The identity quotient \(G/1\), as a completed-group-algebra index for a finite discrete group.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups
open ProCGroups.ProC
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

def identityCompletedGroupAlgebraSubgroupInClass
    (G : Type u) [Group G] [TopologicalSpace G]
    [DiscreteTopology G] [Finite G] :
    OpenNormalSubgroupInClass ProCGroups.FiniteGroupClass.allFinite G

def

identityCompletedGroupAlgebraSubgroupInClassOfMem

L84 ↗

FoxDifferential.identityCompletedGroupAlgebraSubgroupInClassOfMem

Documentation

The identity quotient \(G/1\), as a class-restricted completed-group-algebra stage whenever G itself lies in the finite-group class.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups
open ProCGroups.ProC
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

def identityCompletedGroupAlgebraSubgroupInClassOfMem
    (C : ProCGroups.FiniteGroupClass.{u})
    (G : Type u) [Group G] [TopologicalSpace G] [DiscreteTopology G]
    (hIso : ProCGroups.FiniteGroupClass.IsomClosed C) (hG : C G) :
    OpenNormalSubgroupInClass C G

def

identityCompletedGroupAlgebraIndex

L94 ↗

FoxDifferential.identityCompletedGroupAlgebraIndex

Documentation

The completed-group-algebra stage whose group quotient is \(G/1\).

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups
open ProCGroups.ProC
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

def identityCompletedGroupAlgebraIndex
    (G : Type u) [Group G] [TopologicalSpace G]
    [DiscreteTopology G] [Finite G] :
    _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G

def

identityCompletedGroupAlgebraIndexInClassOfMem

L101 ↗

FoxDifferential.identityCompletedGroupAlgebraIndexInClassOfMem

Documentation

The class-restricted completed-group-algebra stage whose group quotient is \(G/1\).

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups
open ProCGroups.ProC
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

def identityCompletedGroupAlgebraIndexInClassOfMem
    (C : ProCGroups.FiniteGroupClass.{u})
    (G : Type u) [Group G] [TopologicalSpace G] [DiscreteTopology G]
    (hIso : ProCGroups.FiniteGroupClass.IsomClosed C) (hG : C G) :
    CompletedGroupAlgebraIndexInClass G C

theorem

openNormalSubgroupInClassProj_identityCompletedGroupAlgebraIndex_injective

L109 ↗

FoxDifferential.openNormalSubgroupInClassProj_identityCompletedGroupAlgebraIndex_injective

Documentation

The projection to the identity completed stage is injective on group elements.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups
open ProCGroups.ProC
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem openNormalSubgroupInClassProj_identityCompletedGroupAlgebraIndex_injective
    (G : Type u) [Group G] [TopologicalSpace G]
    [DiscreteTopology G] [Finite G] :
    Function.Injective
      (openNormalSubgroupInClassProj
        (C := ProCGroups.FiniteGroupClass.allFinite) (G := G)
        (identityCompletedGroupAlgebraIndex G))

theorem

openNormalSubgroupInClassProj_identityCompletedGAIndexInClassOfMem_inj

L126 ↗

FoxDifferential.openNormalSubgroupInClassProj_identityCompletedGAIndexInClassOfMem_inj

Documentation

The projection to the class-restricted identity completed stage is injective on group elements.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups
open ProCGroups.ProC
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem openNormalSubgroupInClassProj_identityCompletedGAIndexInClassOfMem_inj
    (C : ProCGroups.FiniteGroupClass.{u})
    (G : Type u) [Group G] [TopologicalSpace G] [DiscreteTopology G]
    (hIso : ProCGroups.FiniteGroupClass.IsomClosed C) (hG : C G) :
    Function.Injective
      (openNormalSubgroupInClassProj
        (C := C) (G := G)
        (identityCompletedGroupAlgebraIndexInClassOfMem C G hIso hG))

theorem

modNCompletedGroupAlgebraStageMap_identityCompletedGroupAlgebraIndex_injective

L142 ↗

FoxDifferential.modNCompletedGroupAlgebraStageMap_identityCompletedGroupAlgebraIndex_injective

Documentation

The residue group-algebra stage map to the identity completed stage is injective.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups
open ProCGroups.ProC
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem modNCompletedGroupAlgebraStageMap_identityCompletedGroupAlgebraIndex_injective
    (n : ℕ)
    (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [DiscreteTopology G] [Finite G] :
    Function.Injective
      (modNCompletedGroupAlgebraStageMap n G
        (identityCompletedGroupAlgebraIndex G))

theorem

modNCompletedGAStageMapInClass_identityCompletedGAIndexInClassOfMem_inj

L163 ↗

FoxDifferential.modNCompletedGAStageMapInClass_identityCompletedGAIndexInClassOfMem_inj

Documentation

The residue group-algebra stage map to the class-restricted identity completed stage is injective.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups
open ProCGroups.ProC
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem modNCompletedGAStageMapInClass_identityCompletedGAIndexInClassOfMem_inj
    (n : ℕ) (C : ProCGroups.FiniteGroupClass.{u})
    (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [DiscreteTopology G]
    (hIso : ProCGroups.FiniteGroupClass.IsomClosed C) (hG : C G) :
    Function.Injective
      (modNCompletedGroupAlgebraStageMapInClass n G C
        (identityCompletedGroupAlgebraIndexInClassOfMem C G hIso hG))

Module documentation

Fox differential: completed — differential module — identity

Declarations