Module

Separation.lean

Nyll.ProCGroups.CompletedGroupAlgebra.Separation

19 declarations indexed from sourceView source ↗

Module documentation

Completed Group Algebra / Separation

This module contains separation lemmas for completed group algebras using finite quotients.

Imports2

Imported by3

theorem

exists_completedGroupAlgebraIndex_avoids_finset

L39 ↗

CompletedGroupAlgebra.exists_completedGroupAlgebraIndex_avoids_finset

Documentation

A finite set of nontrivial elements in a profinite group can be avoided by one open-normal finite quotient. This is the finite-support separation input in Lemma 5.3.5(a).

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 : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [T2Space G] in

Lean source · statement

theorem exists_completedGroupAlgebraIndex_avoids_finset
    (s : Finset G)
    (hs : ∀ x ∈ s, x ≠ 1) :
    ∃ U : CompletedGroupAlgebraIndex G,
      ∀ x ∈ s, x ∉ (((OrderDual.ofDual U).1 : OpenNormalSubgroup G) : Subgroup G)

theorem

exists_completedGroupAlgebraIndex_separating_support

L77 ↗

CompletedGroupAlgebra.exists_completedGroupAlgebraIndex_separating_support

Documentation

For a finite-support group-algebra element and a chosen basis element \(g\), one finite quotient separates the image of \(g\) from all other support points.

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 : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [TopologicalSpace R] [IsTopologicalRing R]
    [T2Space G]
    H [Group H] [TopologicalSpace H] [IsTopologicalGroup H] in

Lean source · statement

theorem exists_completedGroupAlgebraIndex_separating_support
    (x : MonoidAlgebra R G) (g : G) :
    ∃ U : CompletedGroupAlgebraIndex G,
      ∀ h ∈ x.coeff.support, h ≠ g →
        openNormalSubgroupInClassProj (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U h ≠
          openNormalSubgroupInClassProj (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U
              g

theorem

completedGroupAlgebraStageMap_coeff_of_support_separated

L115 ↗

CompletedGroupAlgebra.completedGroupAlgebraStageMap_coeff_of_support_separated

Documentation

If a finite quotient separates \(g\) from the other support points of \(x\), then the coefficient of the image of \(g\) in the quotient group algebra is exactly the original coefficient of \(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 : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [TopologicalSpace R] [IsTopologicalRing R]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    H [Group H] [TopologicalSpace H] [IsTopologicalGroup H] in

Lean source · statement

theorem completedGroupAlgebraStageMap_coeff_of_support_separated
    (U : CompletedGroupAlgebraIndex G) (x : MonoidAlgebra R G) (g : G)
    (hsep : ∀ h ∈ x.coeff.support, h ≠ g →
      openNormalSubgroupInClassProj (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U h ≠
        openNormalSubgroupInClassProj (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U g) :
    (completedGroupAlgebraStageMap R G U x).coeff
        (openNormalSubgroupInClassProj
          (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U g) =
      x.coeff g

theorem

exists_completedGroupAlgebraIndexInClass_avoids_finset

L146 ↗

CompletedGroupAlgebra.exists_completedGroupAlgebraIndexInClass_avoids_finset

Documentation

A finite set of nontrivial elements in a pro-\(C\) group can be avoided by one open normal \(C\)-quotient. This is the \(C\)-indexed finite-support separation input in Lemma 5.3.5(a).

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 : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit R [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
    [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G]
    H [Group H] [TopologicalSpace H] [IsTopologicalGroup H] in

Lean source · statement

theorem exists_completedGroupAlgebraIndexInClass_avoids_finset
    (C : ProCGroups.FiniteGroupClass.{v}) (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (hG : HasOpenNormalBasisInClass C G) (s : Finset G) (hs : ∀ x ∈ s, x ≠ 1) :
    ∃ U : CompletedGroupAlgebraIndexInClass G C,
      ∀ x ∈ s, x ∉ (((OrderDual.ofDual U).1 : OpenNormalSubgroup G) : Subgroup G)

theorem

exists_completedGroupAlgebraIndexInClass_separating_finsupp_support

L184 ↗

CompletedGroupAlgebra.exists_completedGroupAlgebraIndexInClass_separating_finsupp_support

Documentation

For any finitely supported family on a pro-\(C\) group and a chosen basis point \(g\), one \(C\)-quotient separates the image of \(g\) from all other support points.

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 : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit R [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
    [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G]
    H [Group H] [TopologicalSpace H] [IsTopologicalGroup H] in

Lean source · statement

theorem exists_completedGroupAlgebraIndexInClass_separating_finsupp_support
    {M : Type w} [Zero M]
    (C : ProCGroups.FiniteGroupClass.{v}) (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (hG : HasOpenNormalBasisInClass C G) (x : G →₀ M) (g : G) :
    ∃ U : CompletedGroupAlgebraIndexInClass G C,
      ∀ h ∈ x.support, h ≠ g →
        openNormalSubgroupInClassProj (C := C) (G := G) U h ≠
          openNormalSubgroupInClassProj (C := C) (G := G) U g

theorem

exists_completedGroupAlgebraIndexInClass_separating_support

L223 ↗

CompletedGroupAlgebra.exists_completedGroupAlgebraIndexInClass_separating_support

Documentation

For a finite-support group-algebra element and a chosen basis element \(g\), one \(C\)-quotient separates the image of \(g\) from all other support points.

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 : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [TopologicalSpace R] [IsTopologicalRing R]
    [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G]
    H [Group H] [TopologicalSpace H] [IsTopologicalGroup H] in

Lean source · statement

theorem exists_completedGroupAlgebraIndexInClass_separating_support
    (C : ProCGroups.FiniteGroupClass.{v}) (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (hG : HasOpenNormalBasisInClass C G) (x : MonoidAlgebra R G) (g : G) :
    ∃ U : CompletedGroupAlgebraIndexInClass G C,
      ∀ h ∈ x.coeff.support, h ≠ g →
        openNormalSubgroupInClassProj (C := C) (G := G) U h ≠
          openNormalSubgroupInClassProj (C := C) (G := G) U g

theorem

completedGroupAlgebraStageMapInClass_coeff_of_support_separated

L241 ↗

CompletedGroupAlgebra.completedGroupAlgebraStageMapInClass_coeff_of_support_separated

Documentation

If a \(C\)-quotient separates \(g\) from the other support points of \(x\), then the coefficient of the image of \(g\) in the quotient group algebra is exactly the original coefficient of \(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 : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [TopologicalSpace R] [IsTopologicalRing R]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    H [Group H] [TopologicalSpace H] [IsTopologicalGroup H] in

Lean source · statement

theorem completedGroupAlgebraStageMapInClass_coeff_of_support_separated
    (C : ProCGroups.FiniteGroupClass.{v}) (U : CompletedGroupAlgebraIndexInClass G C)
    (x : MonoidAlgebra R G) (g : G)
    (hsep : ∀ h ∈ x.coeff.support, h ≠ g →
      openNormalSubgroupInClassProj (C := C) (G := G) U h ≠
        openNormalSubgroupInClassProj (C := C) (G := G) U g) :
    (completedGroupAlgebraStageMapInClass C R G U x).coeff
        (openNormalSubgroupInClassProj (C := C) (G := G) U g) =
      x.coeff g

theorem

injective_toCompletedGroupAlgebraRingHom

L270 ↗

CompletedGroupAlgebra.injective_toCompletedGroupAlgebraRingHom

Documentation

In Lemma 5.3.5(a), fixed-coefficient form, the canonical map from the abstract group algebra to the completed group algebra is injective for profinite G. Equivalently, the kernels of the finite group-quotient maps have trivial intersection.

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 : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [T2Space G] in

Lean source · statement

theorem injective_toCompletedGroupAlgebraRingHom
    : Function.Injective (toCompletedGroupAlgebraRingHom R G)

theorem

toCompletedGroupAlgebraRingHom_ker_eq_bot

L312 ↗

CompletedGroupAlgebra.toCompletedGroupAlgebraRingHom_ker_eq_bot

Documentation

The dense map from the ordinary group algebra into the completed group algebra has trivial kernel after separation by all finite quotient stages.

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 : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [T2Space G] in

Lean source · statement

theorem toCompletedGroupAlgebraRingHom_ker_eq_bot
    : RingHom.ker (toCompletedGroupAlgebraRingHom R G) = ⊥

theorem

toCompletedGroupAlgebraRingHom_ker_eq_iInf_stageMap_ker

L319 ↗

CompletedGroupAlgebra.toCompletedGroupAlgebraRingHom_ker_eq_iInf_stageMap_ker

Documentation

The kernel of the map to \(\widehat{R[G]}\) is the intersection of the finite-stage kernels.

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 : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] in

Lean source · statement

theorem toCompletedGroupAlgebraRingHom_ker_eq_iInf_stageMap_ker :
    RingHom.ker (toCompletedGroupAlgebraRingHom R G) =
      ⨅ U : CompletedGroupAlgebraIndex G, RingHom.ker (completedGroupAlgebraStageMap R G U)

theorem

iInf_completedGroupAlgebraStageMap_ker_eq_bot

L345 ↗

CompletedGroupAlgebra.iInf_completedGroupAlgebraStageMap_ker_eq_bot

Documentation

Fixed-coefficient finite-stage kernel-family form of Lemma 5.3.5(a).

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 : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [T2Space G] in

Lean source · statement

theorem iInf_completedGroupAlgebraStageMap_ker_eq_bot
    : (⨅ U : CompletedGroupAlgebraIndex G,
        RingHom.ker (completedGroupAlgebraStageMap R G U)) = ⊥

theorem

injective_toCompletedGroupAlgebraInClassRingHom

L356 ↗

CompletedGroupAlgebra.injective_toCompletedGroupAlgebraInClassRingHom

Documentation

\(C\)-indexed form of Lemma 5.3.5(a): for a pro-\(C\) group, the canonical map from the abstract group algebra to \(\widehat{R[G]}_{C}\) is injective.

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 : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [CompactSpace G] [TotallyDisconnectedSpace G] in

Lean source · statement

theorem injective_toCompletedGroupAlgebraInClassRingHom
    (C : ProCGroups.FiniteGroupClass.{v})
    (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) :
    Function.Injective (toCompletedGroupAlgebraInClassRingHom C R G)

theorem

toCompletedGroupAlgebraInClassRingHom_ker_eq_bot

L397 ↗

CompletedGroupAlgebra.toCompletedGroupAlgebraInClassRingHom_ker_eq_bot

Documentation

Kernel form of the \(C\)-indexed injectivity statement.

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 : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [CompactSpace G] [TotallyDisconnectedSpace G] in

Lean source · statement

theorem toCompletedGroupAlgebraInClassRingHom_ker_eq_bot
    (C : ProCGroups.FiniteGroupClass.{v})
    (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) :
    RingHom.ker (toCompletedGroupAlgebraInClassRingHom C R G) = ⊥

theorem

toCompletedGroupAlgebraInClassRingHom_ker_eq_iInf_stageMapInClass_ker

L409 ↗

CompletedGroupAlgebra.toCompletedGroupAlgebraInClassRingHom_ker_eq_iInf_stageMapInClass_ker

Documentation

The kernel of the map to \(\widehat{R[G]}_{C}\) is the intersection of the \(C\)-indexed finite-stage kernels.

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 : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] in

Lean source · statement

theorem toCompletedGroupAlgebraInClassRingHom_ker_eq_iInf_stageMapInClass_ker
    (C : ProCGroups.FiniteGroupClass.{v}) :
    RingHom.ker (toCompletedGroupAlgebraInClassRingHom C R G) =
      ⨅ U : CompletedGroupAlgebraIndexInClass G C,
        RingHom.ker (completedGroupAlgebraStageMapInClass C R G U)

theorem

iInf_completedGroupAlgebraStageMapInClass_ker_eq_bot

L439 ↗

CompletedGroupAlgebra.iInf_completedGroupAlgebraStageMapInClass_ker_eq_bot

Documentation

\(C\)-indexed finite-stage kernel-family form of Lemma 5.3.5(a).

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 : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [CompactSpace G] [TotallyDisconnectedSpace G] in

Lean source · statement

theorem iInf_completedGroupAlgebraStageMapInClass_ker_eq_bot
    (C : ProCGroups.FiniteGroupClass.{v})
    (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) :
    (⨅ U : CompletedGroupAlgebraIndexInClass G C,
        RingHom.ker (completedGroupAlgebraStageMapInClass C R G U)) = ⊥

theorem

iInf_groupAlgebraOpenFiniteQuotientKernel_eq_bot

L453 ↗

CompletedGroupAlgebra.iInf_groupAlgebraOpenFiniteQuotientKernel_eq_bot

Documentation

In Lemma 5.3.5(a), book kernel-family form, the intersection of the kernels of \(R[G] \to (R/I)[G/U]\), over open coefficient ideals and finite group quotients, is zero.

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 : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [T2Space G] in

Lean source · statement

theorem iInf_groupAlgebraOpenFiniteQuotientKernel_eq_bot
    [CompactSpace R] [T2Space R] [TotallyDisconnectedSpace R] :
    (⨅ K : CompletedGroupAlgebraOpenQuotientIndex R G,
        groupAlgebraOpenFiniteQuotientKernel R G K) = ⊥

theorem

completedGroupAlgebraRingHom_ext_of_comp_toCompleted

L502 ↗

CompletedGroupAlgebra.completedGroupAlgebraRingHom_ext_of_comp_toCompleted

Documentation

Continuous ring homomorphisms out of \(\widehat{R[G]}\) into another completed group algebra are determined by their values on the dense abstract 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 : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] in

Lean source · statement

theorem completedGroupAlgebraRingHom_ext_of_comp_toCompleted
    [T2Space R]
    {f g : CompletedGroupAlgebraCarrier R G →+* CompletedGroupAlgebraCarrier R H}
    (hf : Continuous f) (hg : Continuous g)
    (hfg : f.comp (toCompletedGroupAlgebraRingHom R G) =
      g.comp (toCompletedGroupAlgebraRingHom R G)) :
    f = g

theorem

completedGroupAlgebraMap_id

L525 ↗

CompletedGroupAlgebra.completedGroupAlgebraMap_id

Documentation

Lemma 5.3.5(e), identity law for the completed-group-algebra functor.

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 : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] in

Lean source · statement

theorem completedGroupAlgebraMap_id
    [T2Space R] :
    completedGroupAlgebraMap (G := G) (H := G) R (MonoidHom.id G) continuous_id =
      RingHom.id (CompletedGroupAlgebraCarrier R G)

theorem

completedGroupAlgebraMapAlgHom_id

L542 ↗

CompletedGroupAlgebra.completedGroupAlgebraMapAlgHom_id

Documentation

Lemma 5.3.5(e), identity law for the completed-group-algebra functor, as an \(R\)-algebra homomorphism.

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 : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] in

Lean source · statement

theorem completedGroupAlgebraMapAlgHom_id
    [T2Space R] :
    completedGroupAlgebraMapAlgHom (G := G) (H := G) R (MonoidHom.id G) continuous_id =
      AlgHom.id R (CompletedGroupAlgebraCarrier R G)

Module documentation

Completed Group Algebra / Separation

Declarations