Module

InClassNaturality.lean

Nyll.ProCGroups.CompletedGroupAlgebra.AllFiniteFunctoriality.InClassNaturality

9 declarations indexed from sourceView source ↗

Module documentation

Completed Group Algebra / All Finite Functoriality / Within a Class Naturality

This module proves that the comparison between the all-finite and \(C\)-indexed completions is natural for continuous group homomorphisms, in ring-, algebra-, and equivalence-valued forms.

Imports3

Imported by2

theorem

completedGroupAlgebraRingHomToInClass_ext_of_comp_toCompleted

L37 ↗

CompletedGroupAlgebra.completedGroupAlgebraRingHomToInClass_ext_of_comp_toCompleted

Documentation

Continuous ring homomorphisms from the all-finite completed group algebra to a \(C\)-indexed completed group algebra are determined by their values on the dense abstract group algebra.

Source context 9 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
universe u v w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem completedGroupAlgebraRingHomToInClass_ext_of_comp_toCompleted
    (C : ProCGroups.FiniteGroupClass.{v})
    [CompactSpace R] [T2Space R] [TotallyDisconnectedSpace R]
    {f g : CompletedGroupAlgebraCarrier R G →+* CompletedGroupAlgebraInClass C R H}
    (hf : Continuous f) (hg : Continuous g)
    (hfg : f.comp (toCompletedGroupAlgebraRingHom R G) =
      g.comp (toCompletedGroupAlgebraRingHom R G)) :
    f = g

theorem

completedGroupAlgebraToInClassRingHom_naturality

L63 ↗

CompletedGroupAlgebra.completedGroupAlgebraToInClassRingHom_naturality

Documentation

Naturality of the comparison from the all-finite completed group algebra to the \(C\)-indexed completed group algebra in the group variable.

Source context 9 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
universe u v w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem completedGroupAlgebraToInClassRingHom_naturality
    (C : ProCGroups.FiniteGroupClass.{v})
    (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
    [CompactSpace R] [T2Space R] [TotallyDisconnectedSpace R]
    (φ : G →* H) (hφ : Continuous φ) :
    (completedGroupAlgebraMapInClass (G := G) (H := H) C hHer R φ hφ).comp
        (completedGroupAlgebraToInClassRingHom (R := R) (G := G) C ) =
      (completedGroupAlgebraToInClassRingHom (R := R) (G := H) C ).comp
        (completedGroupAlgebraMap (G := G) (H := H) R φ hφ)

theorem

completedGroupAlgebraToInClassAlgHom_naturality

L149 ↗

CompletedGroupAlgebra.completedGroupAlgebraToInClassAlgHom_naturality

Documentation

Algebra-homomorphism form of the naturality of the comparison from the all-finite completed group algebra to the \(C\)-indexed completed group algebra.

Source context 9 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
universe u v w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem completedGroupAlgebraToInClassAlgHom_naturality
    (C : ProCGroups.FiniteGroupClass.{v})
    (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
    [CompactSpace R] [T2Space R] [TotallyDisconnectedSpace R]
    (φ : G →* H) (hφ : Continuous φ) :
    (completedGroupAlgebraMapAlgHomInClass (G := G) (H := H) C hHer R φ hφ).comp
        (completedGroupAlgebraToInClassAlgHom (R := R) (G := G) C ) =
      (completedGroupAlgebraToInClassAlgHom (R := R) (G := H) C ).comp
        (completedGroupAlgebraMapAlgHom (G := G) (H := H) R φ hφ)

theorem

completedGroupAlgebraFromInClassRingHom_naturality

L171 ↗

CompletedGroupAlgebra.completedGroupAlgebraFromInClassRingHom_naturality

Documentation

Naturality of the inverse comparison from the \(C\)-indexed completed group algebra back to the all-finite completed group algebra, for pro-\(C\) groups.

Source context 9 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
universe u v w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem completedGroupAlgebraFromInClassRingHom_naturality
    (C : ProCGroups.FiniteGroupClass.{v})
    (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    [CompactSpace R] [T2Space R] [TotallyDisconnectedSpace R]
    (hG : HasOpenNormalBasisInClass C G) (hH : HasOpenNormalBasisInClass C H)
    (φ : G →* H) (hφ : Continuous φ) :
    (completedGroupAlgebraMap (G := G) (H := H) R φ hφ).comp
        (completedGroupAlgebraFromInClassRingHom (R := R) (G := G) C hForm hG) =
      (completedGroupAlgebraFromInClassRingHom (R := R) (G := H) C hForm hH).comp
        (completedGroupAlgebraMapInClass (G := G) (H := H) C hHer R φ hφ)

theorem

completedGroupAlgebraFromInClassAlgHom_naturality

L222 ↗

CompletedGroupAlgebra.completedGroupAlgebraFromInClassAlgHom_naturality

Documentation

Algebra-homomorphism form of the naturality of the inverse comparison from the \(C\)-indexed completed group algebra back to the all-finite completed group algebra.

Source context 9 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
universe u v w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem completedGroupAlgebraFromInClassAlgHom_naturality
    (C : ProCGroups.FiniteGroupClass.{v})
    (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    [CompactSpace R] [T2Space R] [TotallyDisconnectedSpace R]
    (hG : HasOpenNormalBasisInClass C G) (hH : HasOpenNormalBasisInClass C H)
    (φ : G →* H) (hφ : Continuous φ) :
    (completedGroupAlgebraMapAlgHom (G := G) (H := H) R φ hφ).comp
        (completedGroupAlgebraFromInClassAlgHom (R := R) (G := G) C hForm hG) =
      (completedGroupAlgebraFromInClassAlgHom (R := R) (G := H) C hForm hH).comp
        (completedGroupAlgebraMapAlgHomInClass (G := G) (H := H) C hHer R φ hφ)

theorem

completedGroupAlgebraInClassRingEquiv_naturality

L244 ↗

CompletedGroupAlgebra.completedGroupAlgebraInClassRingEquiv_naturality

Documentation

The ring equivalence from all-finite to in-class completions is natural in the group.

Source context 9 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
universe u v w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem completedGroupAlgebraInClassRingEquiv_naturality
    (C : ProCGroups.FiniteGroupClass.{v})
    (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    [CompactSpace R] [T2Space R] [TotallyDisconnectedSpace R]
    (hG : HasOpenNormalBasisInClass C G) (hH : HasOpenNormalBasisInClass C H)
    (φ : G →* H) (hφ : Continuous φ) (x : CompletedGroupAlgebraCarrier R G) :
    completedGroupAlgebraMapInClass (G := G) (H := H) C hHer R φ hφ
        (completedGroupAlgebraInClassRingEquiv (R := R) (G := G) C hForm hG x) =
      completedGroupAlgebraInClassRingEquiv (R := R) (G := H) C hForm hH
        (completedGroupAlgebraMap (G := G) (H := H) R φ hφ x)

theorem

completedGroupAlgebraInClassRingEquiv_symm_naturality

L264 ↗

CompletedGroupAlgebra.completedGroupAlgebraInClassRingEquiv_symm_naturality

Documentation

The inverse ring equivalence from in-class to all-finite completions is natural in the group.

Source context 9 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
universe u v w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem completedGroupAlgebraInClassRingEquiv_symm_naturality
    (C : ProCGroups.FiniteGroupClass.{v})
    (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    [CompactSpace R] [T2Space R] [TotallyDisconnectedSpace R]
    (hG : HasOpenNormalBasisInClass C G) (hH : HasOpenNormalBasisInClass C H)
    (φ : G →* H) (hφ : Continuous φ) (x : CompletedGroupAlgebraInClass C R G) :
    completedGroupAlgebraMap (G := G) (H := H) R φ hφ
        ((completedGroupAlgebraInClassRingEquiv (R := R) (G := G) C hForm hG).symm x) =
      (completedGroupAlgebraInClassRingEquiv (R := R) (G := H) C hForm hH).symm
        (completedGroupAlgebraMapInClass (G := G) (H := H) C hHer R φ hφ x)

theorem

completedGroupAlgebraInClassAlgEquiv_naturality

L284 ↗

CompletedGroupAlgebra.completedGroupAlgebraInClassAlgEquiv_naturality

Documentation

The algebra equivalence from all-finite to in-class completions is natural in the group.

Source context 9 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
universe u v w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem completedGroupAlgebraInClassAlgEquiv_naturality
    (C : ProCGroups.FiniteGroupClass.{v})
    (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    [CompactSpace R] [T2Space R] [TotallyDisconnectedSpace R]
    (hG : HasOpenNormalBasisInClass C G) (hH : HasOpenNormalBasisInClass C H)
    (φ : G →* H) (hφ : Continuous φ) (x : CompletedGroupAlgebraCarrier R G) :
    completedGroupAlgebraMapAlgHomInClass (G := G) (H := H) C hHer R φ hφ
        (completedGroupAlgebraInClassAlgEquiv (R := R) (G := G) C hForm hG x) =
      completedGroupAlgebraInClassAlgEquiv (R := R) (G := H) C hForm hH
        (completedGroupAlgebraMapAlgHom (G := G) (H := H) R φ hφ x)

theorem

completedGroupAlgebraInClassAlgEquiv_symm_naturality

L306 ↗

CompletedGroupAlgebra.completedGroupAlgebraInClassAlgEquiv_symm_naturality

Documentation

The inverse algebra equivalence from in-class to all-finite completions is natural in the group.

Source context 9 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
universe u v w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem completedGroupAlgebraInClassAlgEquiv_symm_naturality
    (C : ProCGroups.FiniteGroupClass.{v})
    (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    [CompactSpace R] [T2Space R] [TotallyDisconnectedSpace R]
    (hG : HasOpenNormalBasisInClass C G) (hH : HasOpenNormalBasisInClass C H)
    (φ : G →* H) (hφ : Continuous φ) (x : CompletedGroupAlgebraInClass C R G) :
    completedGroupAlgebraMapAlgHom (G := G) (H := H) R φ hφ
        ((completedGroupAlgebraInClassAlgEquiv (R := R) (G := G) C hForm hG).symm x) =
      (completedGroupAlgebraInClassAlgEquiv (R := R) (G := H) C hForm hH).symm
        (completedGroupAlgebraMapAlgHomInClass (G := G) (H := H) C hHer R φ hφ x)

Module documentation

Completed Group Algebra / All Finite Functoriality / Within a Class Naturality

Declarations