NYLL
Module

CompletedGroupAlgebra.lean

Nyll.ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebra
22 declarations indexed from sourceView source ↗

Module documentation

Fox differential: completed — coefficient rings — completed group algebra

The principal declarations in this module are:

  • CompletedGroupAlgebraIndexInClass

The index set for a completed group algebra over finite quotients belonging to a class C.

  • CompletedGroupAlgebraQuotientInClass

The finite quotient of G attached to one class-restricted completed-group-algebra stage.

  • completedGroupAlgebraTransitionInClass_id

Identity case for completedGroupAlgebraTransitionInClass_id.

  • completedGroupAlgebraTransitionInClass_comp

Composition lemma completedGroupAlgebraTransitionInClass_comp.

Imports2
Imported by2

Declarations

abbrev

CompletedGroupAlgebraIndexInClass

L40 ↗
FoxDifferential.CompletedGroupAlgebraIndexInClass
Documentation

The index set for a completed group algebra over finite quotients belonging to a class C.

Source context 9 commands

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

namespace FoxDifferential
open Set
open ProCGroups
open ProCGroups.InverseSystems
open ProCGroups.ProC
open scoped Topology
noncomputable section
universe u v w
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
abbrev CompletedGroupAlgebraIndexInClass (C : ProCGroups.FiniteGroupClass.{u})
abbrev

CompletedGroupAlgebraQuotientInClass

L44 ↗
FoxDifferential.CompletedGroupAlgebraQuotientInClass
Documentation

The finite quotient of G attached to one class-restricted completed-group-algebra stage.

Source context 9 commands

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

namespace FoxDifferential
open Set
open ProCGroups
open ProCGroups.InverseSystems
open ProCGroups.ProC
open scoped Topology
noncomputable section
universe u v w
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
abbrev CompletedGroupAlgebraQuotientInClass
    (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C) : Type _
abbrev

CompletedGroupAlgebraStageInClass

L49 ↗
FoxDifferential.CompletedGroupAlgebraStageInClass
Documentation

The discrete group ring over one class-restricted finite quotient of G.

Source context 9 commands

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

namespace FoxDifferential
open Set
open ProCGroups
open ProCGroups.InverseSystems
open ProCGroups.ProC
open scoped Topology
noncomputable section
universe u v w
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
abbrev CompletedGroupAlgebraStageInClass
    (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C) : Type _
def

completedGroupAlgebraTransitionInClass

L54 ↗
FoxDifferential.completedGroupAlgebraTransitionInClass
Documentation

The transition map between two class-restricted completed-group-algebra stages.

Source context 9 commands

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

namespace FoxDifferential
open Set
open ProCGroups
open ProCGroups.InverseSystems
open ProCGroups.ProC
open scoped Topology
noncomputable section
universe u v w
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
def completedGroupAlgebraTransitionInClass
    (C : ProCGroups.FiniteGroupClass.{u})
    {U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V) :
    CompletedGroupAlgebraStageInClass G C V →+*
      CompletedGroupAlgebraStageInClass G C U
theorem

completedGroupAlgebraTransitionInClass_id

L66 ↗
FoxDifferential.completedGroupAlgebraTransitionInClass_id
Documentation

Identity case for completedGroupAlgebraTransitionInClass_id.

Source context 9 commands

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

namespace FoxDifferential
open Set
open ProCGroups
open ProCGroups.InverseSystems
open ProCGroups.ProC
open scoped Topology
noncomputable section
universe u v w
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem completedGroupAlgebraTransitionInClass_id
    (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C) :
    completedGroupAlgebraTransitionInClass G C (le_rfl : U ≤ U) = RingHom.id _
theorem

completedGroupAlgebraTransitionInClass_comp

L75 ↗
FoxDifferential.completedGroupAlgebraTransitionInClass_comp
Documentation

Composition lemma completedGroupAlgebraTransitionInClass_comp.

Source context 9 commands

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

namespace FoxDifferential
open Set
open ProCGroups
open ProCGroups.InverseSystems
open ProCGroups.ProC
open scoped Topology
noncomputable section
universe u v w
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem completedGroupAlgebraTransitionInClass_comp
    (C : ProCGroups.FiniteGroupClass.{u})
    {U V W : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V) (hVW : V ≤ W) :
    (completedGroupAlgebraTransitionInClass G C hUV).comp
        (completedGroupAlgebraTransitionInClass G C hVW) =
      completedGroupAlgebraTransitionInClass G C (hUV.trans hVW)
def

completedGroupAlgebraSystemInClass

L97 ↗
FoxDifferential.completedGroupAlgebraSystemInClass
Documentation

The class-restricted inverse system of finite-stage integral group rings.

Source context 9 commands

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

namespace FoxDifferential
open Set
open ProCGroups
open ProCGroups.InverseSystems
open ProCGroups.ProC
open scoped Topology
noncomputable section
universe u v w
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · full declaration
def completedGroupAlgebraSystemInClass
    (C : ProCGroups.FiniteGroupClass.{u}) :
    InverseSystem (I := CompletedGroupAlgebraIndexInClass G C) where
  X := CompletedGroupAlgebraStageInClass G C
  topologicalSpace := fun _ => ⊥
  map := fun {U V} hUV => completedGroupAlgebraTransitionInClass G C hUV
  continuous_map := by
    intro U V hUV
    let : TopologicalSpace (CompletedGroupAlgebraStageInClass G C U) := ⊥
    let : TopologicalSpace (CompletedGroupAlgebraStageInClass G C V) := ⊥
    let : DiscreteTopology (CompletedGroupAlgebraStageInClass G C V) := ⟨rfl⟩
    exact continuous_of_discreteTopology
  map_id := by
    intro U
    funext x
    exact congrFun
      (congrArg DFunLike.coe
        (completedGroupAlgebraTransitionInClass_id G C U)) x
  map_comp := by
    intro U V W hUV hVW
    funext x
    exact congrFun
      (congrArg DFunLike.coe
        (completedGroupAlgebraTransitionInClass_comp G C hUV hVW)) x
def

completedGroupAlgebraStageMapInClass

L123 ↗
FoxDifferential.completedGroupAlgebraStageMapInClass
Documentation

The quotient ring map from ℤ[G] to one class-restricted finite stage.

Source context 9 commands

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

namespace FoxDifferential
open Set
open ProCGroups
open ProCGroups.InverseSystems
open ProCGroups.ProC
open scoped Topology
noncomputable section
universe u v w
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
def completedGroupAlgebraStageMapInClass
    (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C) :
    MonoidAlgebra ℤ G →+* CompletedGroupAlgebraStageInClass G C U
theorem

completedGroupAlgebraStageMapInClass_of

L131 ↗
FoxDifferential.completedGroupAlgebraStageMapInClass_of
Documentation

Evaluation formula for completedGroupAlgebraStageMapInClass_of.

Source context 9 commands

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

namespace FoxDifferential
open Set
open ProCGroups
open ProCGroups.InverseSystems
open ProCGroups.ProC
open scoped Topology
noncomputable section
universe u v w
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem completedGroupAlgebraStageMapInClass_of
    (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C) (g : G) :
    completedGroupAlgebraStageMapInClass G C U (MonoidAlgebra.of ℤ _ g) =
      MonoidAlgebra.single (openNormalSubgroupInClassProj (C := C) (G := G) U g) 1
theorem

completedGroupAlgebraStageMapInClass_compatible

L145 ↗
FoxDifferential.completedGroupAlgebraStageMapInClass_compatible
Documentation

Compatibility lemma completedGroupAlgebraStageMapInClass_compatible.

Source context 9 commands

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

namespace FoxDifferential
open Set
open ProCGroups
open ProCGroups.InverseSystems
open ProCGroups.ProC
open scoped Topology
noncomputable section
universe u v w
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem completedGroupAlgebraStageMapInClass_compatible
    (C : ProCGroups.FiniteGroupClass.{u})
    {U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V) :
    (completedGroupAlgebraTransitionInClass G C hUV).comp
        (completedGroupAlgebraStageMapInClass G C V) =
      completedGroupAlgebraStageMapInClass G C U
def

CompletedGroupAlgebraCompatibleInClass

L171 ↗
FoxDifferential.CompletedGroupAlgebraCompatibleInClass
Documentation

Compatibility for a class-restricted completed group algebra family.

Source context 9 commands

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

namespace FoxDifferential
open Set
open ProCGroups
open ProCGroups.InverseSystems
open ProCGroups.ProC
open scoped Topology
noncomputable section
universe u v w
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
def CompletedGroupAlgebraCompatibleInClass
    (C : ProCGroups.FiniteGroupClass.{u})
    (x : ∀ U : CompletedGroupAlgebraIndexInClass G C,
      CompletedGroupAlgebraStageInClass G C U) : Prop
abbrev

CompletedGroupAlgebraInClass

L178 ↗
FoxDifferential.CompletedGroupAlgebraInClass
Documentation

The class-restricted completed group algebra as an inverse-limit subtype.

Source context 9 commands

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

namespace FoxDifferential
open Set
open ProCGroups
open ProCGroups.InverseSystems
open ProCGroups.ProC
open scoped Topology
noncomputable section
universe u v w
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
abbrev CompletedGroupAlgebraInClass (C : ProCGroups.FiniteGroupClass.{u}) : Type _
def

completedGroupAlgebraProjectionInClass

L184 ↗
FoxDifferential.completedGroupAlgebraProjectionInClass
Documentation

Projection from the class-restricted completed group algebra to one finite stage.

Source context 9 commands

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

namespace FoxDifferential
open Set
open ProCGroups
open ProCGroups.InverseSystems
open ProCGroups.ProC
open scoped Topology
noncomputable section
universe u v w
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
def completedGroupAlgebraProjectionInClass
    (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C) :
    CompletedGroupAlgebraInClass G C → CompletedGroupAlgebraStageInClass G C U
def

completedGroupAlgebraComapIndexInClass

L199 ↗
FoxDifferential.completedGroupAlgebraComapIndexInClass
Documentation

Pull back a class-restricted finite quotient along a continuous homomorphism.

The hereditary hypothesis is the precise extra closure property needed: the pulled-back quotient embeds into the target quotient, so membership in C follows from closure under subgroups.

Source context 13 commands

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

namespace FoxDifferential
open Set
open ProCGroups
open ProCGroups.InverseSystems
open ProCGroups.ProC
open scoped Topology
noncomputable section
universe u v w
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
section ComapInClass
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · statement
def completedGroupAlgebraComapIndexInClass
    (C : ProCGroups.FiniteGroupClass.{u}) (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (ψ : ContinuousMonoidHom G H) (U : CompletedGroupAlgebraIndexInClass H C) :
    CompletedGroupAlgebraIndexInClass G C
def

completedGroupAlgebraComapQuotientMapInClass

L221 ↗
FoxDifferential.completedGroupAlgebraComapQuotientMapInClass
Documentation

The finite quotient map induced by a continuous homomorphism after pulling back the stage.

Source context 13 commands

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

namespace FoxDifferential
open Set
open ProCGroups
open ProCGroups.InverseSystems
open ProCGroups.ProC
open scoped Topology
noncomputable section
universe u v w
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
section ComapInClass
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · statement
def completedGroupAlgebraComapQuotientMapInClass
    (C : ProCGroups.FiniteGroupClass.{u}) (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (ψ : ContinuousMonoidHom G H) (U : CompletedGroupAlgebraIndexInClass H C) :
    CompletedGroupAlgebraQuotientInClass G C
        (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC ψ U) →*
      CompletedGroupAlgebraQuotientInClass H C U
theorem

completedGroupAlgebraComapQuotientMapInClass_mk

L235 ↗
FoxDifferential.completedGroupAlgebraComapQuotientMapInClass_mk
Documentation

Evaluation formula for completedGroupAlgebraComapQuotientMapInClass_mk.

Source context 13 commands

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

namespace FoxDifferential
open Set
open ProCGroups
open ProCGroups.InverseSystems
open ProCGroups.ProC
open scoped Topology
noncomputable section
universe u v w
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
section ComapInClass
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · statement
theorem completedGroupAlgebraComapQuotientMapInClass_mk
    (C : ProCGroups.FiniteGroupClass.{u}) (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (ψ : ContinuousMonoidHom G H) (U : CompletedGroupAlgebraIndexInClass H C) (g : G) :
    completedGroupAlgebraComapQuotientMapInClass
        (G := G) (H := H) C hC ψ U
        (QuotientGroup.mk'
          ((((OrderDual.ofDual
            (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC ψ U)).1 :
              OpenNormalSubgroup G) : Subgroup G)) g) =
      QuotientGroup.mk' ((((OrderDual.ofDual U).1 : OpenNormalSubgroup H) : Subgroup H))
        (ψ g)
theorem

completedGroupAlgebraComapQuotientMapInClass_surjective_of_surjective

L248 ↗
FoxDifferential.completedGroupAlgebraComapQuotientMapInClass_surjective_of_surjective
Documentation

Surjectivity lemma completedGroupAlgebraComapQuotientMapInClass_surjective_of_surjective.

Source context 13 commands

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

namespace FoxDifferential
open Set
open ProCGroups
open ProCGroups.InverseSystems
open ProCGroups.ProC
open scoped Topology
noncomputable section
universe u v w
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
section ComapInClass
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · statement
theorem completedGroupAlgebraComapQuotientMapInClass_surjective_of_surjective
    (C : ProCGroups.FiniteGroupClass.{u}) (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (ψ : ContinuousMonoidHom G H) (hψ : Function.Surjective ψ)
    (U : CompletedGroupAlgebraIndexInClass H C) :
    Function.Surjective
      (completedGroupAlgebraComapQuotientMapInClass (G := G) (H := H) C hC ψ U)
theorem

completedGroupAlgebraComapIndexInClass_mono

L266 ↗
FoxDifferential.completedGroupAlgebraComapIndexInClass_mono
Documentation

有限群クラスを固定した 標準写像が対応する有限段階・係数段階・augmentation 構造と両立することを述べる。

Source context 14 commands

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

namespace FoxDifferential
open Set
open ProCGroups
open ProCGroups.InverseSystems
open ProCGroups.ProC
open scoped Topology
noncomputable section
universe u v w
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
section ComapInClass
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [IsTopologicalGroup G] in
Lean source · statement
theorem completedGroupAlgebraComapIndexInClass_mono
    (C : ProCGroups.FiniteGroupClass.{u}) (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (ψ : ContinuousMonoidHom G H) {U V : CompletedGroupAlgebraIndexInClass H C}
    (hUV : U ≤ V) :
    completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC ψ U ≤
      completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC ψ V
theorem

completedGroupAlgebraComapQuotientMapInClass_compatible

L281 ↗
FoxDifferential.completedGroupAlgebraComapQuotientMapInClass_compatible
Documentation

Compatibility lemma completedGroupAlgebraComapQuotientMapInClass_compatible.

Source context 13 commands

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

namespace FoxDifferential
open Set
open ProCGroups
open ProCGroups.InverseSystems
open ProCGroups.ProC
open scoped Topology
noncomputable section
universe u v w
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
section ComapInClass
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · statement
theorem completedGroupAlgebraComapQuotientMapInClass_compatible
    (C : ProCGroups.FiniteGroupClass.{u}) (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (ψ : ContinuousMonoidHom G H) {U V : CompletedGroupAlgebraIndexInClass H C}
    (hUV : U ≤ V) :
    (OpenNormalSubgroupInClass.map
        (C := C) (G := H)
        (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV).comp
        (completedGroupAlgebraComapQuotientMapInClass (G := G) (H := H) C hC ψ V) =
      (completedGroupAlgebraComapQuotientMapInClass (G := G) (H := H) C hC ψ U).comp
        (OpenNormalSubgroupInClass.map
          (C := C) (G := G)
          (U := OrderDual.ofDual
            (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC ψ U))
          (V := OrderDual.ofDual
            (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC ψ V))
          (completedGroupAlgebraComapIndexInClass_mono (G := G) (H := H) C hC ψ hUV))
theorem

completedGroupAlgebraComapIndexInClass_id

L308 ↗
FoxDifferential.completedGroupAlgebraComapIndexInClass_id
Documentation

Pulling a finite quotient back along the identity continuous homomorphism gives the same class-restricted index. This is intentionally an equality theorem, since dependent inverse-limit indices are often not definitionally equal after target naturality rewrites.

Source context 13 commands

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

namespace FoxDifferential
open Set
open ProCGroups
open ProCGroups.InverseSystems
open ProCGroups.ProC
open scoped Topology
noncomputable section
universe u v w
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
section ComapInClass
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · statement
theorem completedGroupAlgebraComapIndexInClass_id
    (C : ProCGroups.FiniteGroupClass.{u}) (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (U : CompletedGroupAlgebraIndexInClass G C) :
    completedGroupAlgebraComapIndexInClass (G := G) (H := G) C hC
        (ContinuousMonoidHom.id G) U = U
theorem

completedGroupAlgebraComapIndexInClass_comp

L326 ↗
FoxDifferential.completedGroupAlgebraComapIndexInClass_comp
Documentation

Pullback of class-restricted finite quotients is functorial for continuous target maps.

This is the index-level rewrite needed when the two inverse-limit stage indices produced by a composite target map are propositionally, but not definitionally, the same.

Source context 14 commands

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

namespace FoxDifferential
open Set
open ProCGroups
open ProCGroups.InverseSystems
open ProCGroups.ProC
open scoped Topology
noncomputable section
universe u v w
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
section ComapInClass
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [IsTopologicalGroup G] in
Lean source · statement
theorem completedGroupAlgebraComapIndexInClass_comp
    (C : ProCGroups.FiniteGroupClass.{u}) (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    {K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
    (φ : G →ₜ* H) (ψ : H →ₜ* K) (U : CompletedGroupAlgebraIndexInClass K C) :
    completedGroupAlgebraComapIndexInClass (G := G) (H := K) C hC (ψ.comp φ) U =
      completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC φ
        (completedGroupAlgebraComapIndexInClass (G := H) (H := K) C hC ψ U)
theorem

completedGroupAlgebraComapIndexInClass_top

L343 ↗
FoxDifferential.completedGroupAlgebraComapIndexInClass_top
Documentation

Pulling back the canonical trivial quotient gives the canonical trivial quotient.

Source context 14 commands

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

namespace FoxDifferential
open Set
open ProCGroups
open ProCGroups.InverseSystems
open ProCGroups.ProC
open scoped Topology
noncomputable section
universe u v w
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
section ComapInClass
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [IsTopologicalGroup G] in
Lean source · statement
theorem completedGroupAlgebraComapIndexInClass_top
    (C : ProCGroups.FiniteGroupClass.{u}) (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (ψ : G →ₜ* H) :
    completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hC ψ
        (OrderDual.toDual (OpenNormalSubgroupInClass.top (C := C) (G := H))) =
      OrderDual.toDual (OpenNormalSubgroupInClass.top (C := C) (G := G))

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