Module

KernelBoundary.lean

Nyll.ProCGroups.CrowellExactSequence.Profinite.KernelBoundary

17 declarations indexed from sourceView source ↗

Module documentation

Boundary maps from the profinite kernel

This file constructs the completed and separated boundary maps on the kernel of a profinite presentation. It proves that these maps kill commutators and gives continuity criteria ensuring that they kill the closure of the commutator subgroup, hence factor through topological abelianization.

Imports3

Imported by2

def

completedKernelBoundaryProCInteger

L35 ↗

CrowellExactSequence.completedKernelBoundaryProCInteger

Documentation

Kernel elements map multiplicatively to the Fox completed differential module.

Source context 9 commands

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

namespace CrowellExactSequence
noncomputable section
open scoped BigOperators commutatorElement
open FoxDifferential
open ProCGroups.ProC
universe u
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · full declaration

def completedKernelBoundaryProCInteger
    (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H) :
    psi.toMonoidHom.ker →*
      Multiplicative (ZCCompletedDifferentialModule C psi.toMonoidHom) where
  toFun n := Multiplicative.ofAdd
    (zcUniversalDifferential C psi.toMonoidHom n.1)
  map_one' := by
    apply Multiplicative.toAdd.injective
    exact ScalarCrossedHom.map_one (zcUniversalDifferential C psi.toMonoidHom)
  map_mul' n₁ n₂ := by
    apply Multiplicative.toAdd.injective
    have hmul :=
      ScalarCrossedHom.map_mul (zcUniversalDifferential C psi.toMonoidHom) n₁.1 n₂.1
    have hpsi : psi.toMonoidHom n₁.1 = 1 := n₁.2
    have hadd :
        zcUniversalDifferential C psi.toMonoidHom ((n₁ * n₂ : psi.toMonoidHom.ker).1) =
          zcUniversalDifferential C psi.toMonoidHom n₁.1 +
            zcUniversalDifferential C psi.toMonoidHom n₂.1 := by
      change
        zcUniversalDifferential C psi.toMonoidHom (n₁.1 * n₂.1) =
          zcUniversalDifferential C psi.toMonoidHom n₁.1 +
            zcUniversalDifferential C psi.toMonoidHom n₂.1
      rw [hmul, zcCompletedGroupAlgebraScalar_apply, hpsi, map_one, one_smul]
    exact hadd

def

separatedCompletedKernelBoundaryProCInteger

L61 ↗

CrowellExactSequence.separatedCompletedKernelBoundaryProCInteger

Documentation

Kernel elements map multiplicatively to the separated completed differential module.

Source context 9 commands

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

namespace CrowellExactSequence
noncomputable section
open scoped BigOperators commutatorElement
open FoxDifferential
open ProCGroups.ProC
universe u
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · full declaration

def separatedCompletedKernelBoundaryProCInteger
    (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H) :
    psi.toMonoidHom.ker →*
      Multiplicative (ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom) where
  toFun n := Multiplicative.ofAdd
    (zcSeparatedUniversalDifferential C psi.toMonoidHom n.1)
  map_one' := by
    apply Multiplicative.toAdd.injective
    change zcSeparatedUniversalDifferential C psi.toMonoidHom 1 = 0
    rw [← zcCompletedDifferentialModuleToSeparated_universal
      (C := C) (ψ := psi.toMonoidHom) (g := 1),
      ScalarCrossedHom.map_one (zcUniversalDifferential C psi.toMonoidHom)]
    exact
      (zcCompletedDifferentialModuleToSeparated C psi.toMonoidHom).map_zero
  map_mul' n₁ n₂ := by
    apply Multiplicative.toAdd.injective
    have hmul :=
      ScalarCrossedHom.map_mul
        (zcSeparatedUniversalDifferential C psi.toMonoidHom) n₁.1 n₂.1
    have hpsi : psi.toMonoidHom n₁.1 = 1 := n₁.2
    have hadd :
        zcSeparatedUniversalDifferential C psi.toMonoidHom ((n₁ * n₂ : psi.toMonoidHom.ker).1) =
          zcSeparatedUniversalDifferential C psi.toMonoidHom n₁.1 +
            zcSeparatedUniversalDifferential C psi.toMonoidHom n₂.1 := by
      change
        zcSeparatedUniversalDifferential C psi.toMonoidHom (n₁.1 * n₂.1) =
          zcSeparatedUniversalDifferential C psi.toMonoidHom n₁.1 +
            zcSeparatedUniversalDifferential C psi.toMonoidHom n₂.1
      rw [hmul, zcCompletedGroupAlgebraScalar_apply, hpsi, map_one, one_smul]
    exact hadd

theorem

separatedCompletedKernelBoundaryProCInteger_mem_ker_iff

L97 ↗

CrowellExactSequence.separatedCompletedKernelBoundaryProCInteger_mem_ker_iff

Documentation

Membership in the separated completed kernel-boundary kernel is equivalent to vanishing of the corresponding finite-stage coordinate.

Source context 10 commands

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

namespace CrowellExactSequence
noncomputable section
open scoped BigOperators commutatorElement
open FoxDifferential
open ProCGroups.ProC
universe u
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 separatedCompletedKernelBoundaryProCInteger_mem_ker_iff
    {C : ProCGroups.FiniteGroupClass.{u}} {psi : ContinuousMonoidHom G H}
    {n : ProfiniteKernelSubgroup psi} :
    n ∈ (separatedCompletedKernelBoundaryProCInteger
        (G := G) (H := H) C psi).ker ↔
      ∀ i : ZCCompletedDifferentialModuleIndex C psi.toMonoidHom,
        zcCompletedDifferentialModuleStageDifferential C psi.toMonoidHom i n.1 = 0

theorem

isClosed_separatedCompletedKernelBoundaryProCInteger_ker

L161 ↗

CrowellExactSequence.isClosed_separatedCompletedKernelBoundaryProCInteger_ker

Documentation

The separated kernel boundary has closed kernel, because zero can be tested at every finite stage and each finite-stage boundary is continuous.

Source context 9 commands

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

namespace CrowellExactSequence
noncomputable section
open scoped BigOperators commutatorElement
open FoxDifferential
open ProCGroups.ProC
universe u
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem isClosed_separatedCompletedKernelBoundaryProCInteger_ker
    (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H) :
    IsClosed
      (((separatedCompletedKernelBoundaryProCInteger
          (G := G) (H := H) C psi).ker :
        Subgroup (ProfiniteKernelSubgroup psi)) :
          Set (ProfiniteKernelSubgroup psi))

theorem

separatedCompletedKernelBoundaryProCInteger_commutator_le_ker

L194 ↗

CrowellExactSequence.separatedCompletedKernelBoundaryProCInteger_commutator_le_ker

Documentation

Algebraic part of well-definedness for the separated boundary: ordinary commutators already map to zero.

Source context 10 commands

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

namespace CrowellExactSequence
noncomputable section
open scoped BigOperators commutatorElement
open FoxDifferential
open ProCGroups.ProC
universe u
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 separatedCompletedKernelBoundaryProCInteger_commutator_le_ker
    (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H) :
    commutator (ProfiniteKernelSubgroup psi) <=
      (separatedCompletedKernelBoundaryProCInteger (G := G) (H := H) C psi).ker

theorem

separatedBoundaryKillsTopologicalCommutatorProCInteger

L213 ↗

CrowellExactSequence.separatedBoundaryKillsTopologicalCommutatorProCInteger

Documentation

The separated kernel boundary kills \(\overline{[N,N]}\) without assuming algebraic closedness of the raw crossed-differential relation submodule.

Source context 9 commands

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

namespace CrowellExactSequence
noncomputable section
open scoped BigOperators commutatorElement
open FoxDifferential
open ProCGroups.ProC
universe u
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem separatedBoundaryKillsTopologicalCommutatorProCInteger
    (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H) :
    Subgroup.topologicalClosure (commutator (ProfiniteKernelSubgroup psi)) <=
      (separatedCompletedKernelBoundaryProCInteger (G := G) (H := H) C psi).ker

theorem

completedBoundaryKillsTopologicalCommutatorProCInteger_of_continuous

L229 ↗

CrowellExactSequence.completedBoundaryKillsTopologicalCommutatorProCInteger_of_continuous

Documentation

If the completed kernel boundary is continuous and its target is \(T_1\), then it vanishes on the topological closure of the kernel's commutator subgroup.

Source context 9 commands

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

namespace CrowellExactSequence
noncomputable section
open scoped BigOperators commutatorElement
open FoxDifferential
open ProCGroups.ProC
universe u
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem completedBoundaryKillsTopologicalCommutatorProCInteger_of_continuous
    (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H)
    [TopologicalSpace (ZCCompletedDifferentialModule C psi.toMonoidHom)]
    [T1Space (ZCCompletedDifferentialModule C psi.toMonoidHom)]
    (hcont :
      Continuous (completedKernelBoundaryProCInteger (G := G) (H := H) C psi)) :
    Subgroup.topologicalClosure (commutator (ProfiniteKernelSubgroup psi)) <=
      (completedKernelBoundaryProCInteger (G := G) (H := H) C psi).ker

abbrev

CompletedBoundaryKillsTopologicalCommutatorProCInteger

L259 ↗

CrowellExactSequence.CompletedBoundaryKillsTopologicalCommutatorProCInteger

Documentation

Correct topological boundary factorization condition for the genuine \(N^{\mathrm{ab}}(C)\) map.

Source context 9 commands

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

namespace CrowellExactSequence
noncomputable section
open scoped BigOperators commutatorElement
open FoxDifferential
open ProCGroups.ProC
universe u
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

abbrev CompletedBoundaryKillsTopologicalCommutatorProCInteger
    (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H) : Prop

theorem

completedBoundaryKillsTopologicalCommutatorProCInteger_of_continuousBoundary

L268 ↗

CrowellExactSequence.completedBoundaryKillsTopologicalCommutatorProCInteger_of_continuousBoundary

Documentation

Continuity of the completed kernel boundary supplies the condition required for it to factor through the profinite kernel's topological abelianization.

Source context 9 commands

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

namespace CrowellExactSequence
noncomputable section
open scoped BigOperators commutatorElement
open FoxDifferential
open ProCGroups.ProC
universe u
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem completedBoundaryKillsTopologicalCommutatorProCInteger_of_continuousBoundary
    (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H)
    [TopologicalSpace (ZCCompletedDifferentialModule C psi.toMonoidHom)]
    [T1Space (ZCCompletedDifferentialModule C psi.toMonoidHom)]
    (hcont :
      Continuous (completedKernelBoundaryProCInteger (G := G) (H := H) C psi)) :
    CompletedBoundaryKillsTopologicalCommutatorProCInteger (G := G) (H := H) C psi

theorem

completedKernelBoundaryProCInteger_commutator_le_ker

L284 ↗

CrowellExactSequence.completedKernelBoundaryProCInteger_commutator_le_ker

Documentation

Algebraic part of well-definedness: the kernel boundary kills the ordinary commutator subgroup of the profinite kernel. The remaining topological step is to pass from the commutator subgroup to its closure.

Source context 10 commands

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

namespace CrowellExactSequence
noncomputable section
open scoped BigOperators commutatorElement
open FoxDifferential
open ProCGroups.ProC
universe u
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 completedKernelBoundaryProCInteger_commutator_le_ker
    (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H) :
    commutator (ProfiniteKernelSubgroup psi) <=
      (completedKernelBoundaryProCInteger (G := G) (H := H) C psi).ker

theorem

completedBoundaryKillsTopologicalCommutatorProCInteger_of_closed_ker

L300 ↗

CrowellExactSequence.completedBoundaryKillsTopologicalCommutatorProCInteger_of_closed_ker

Documentation

Topological form of well-definedness from closedness of the kernel of the boundary map.

Source context 9 commands

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

namespace CrowellExactSequence
noncomputable section
open scoped BigOperators commutatorElement
open FoxDifferential
open ProCGroups.ProC
universe u
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem completedBoundaryKillsTopologicalCommutatorProCInteger_of_closed_ker
    (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H)
    (hclosed :
      IsClosed
        (((completedKernelBoundaryProCInteger (G := G) (H := H) C psi).ker :
          Subgroup (ProfiniteKernelSubgroup psi)) : Set (ProfiniteKernelSubgroup psi))) :
    CompletedBoundaryKillsTopologicalCommutatorProCInteger (G := G) (H := H) C psi

theorem

continuous_completedKernelBoundaryZC_of_continuous_zcUnivDiff

L319 ↗

CrowellExactSequence.continuous_completedKernelBoundaryZC_of_continuous_zcUnivDiff

Documentation

Continuity of the universal completed differential on the ambient group implies continuity of the kernel boundary.

Source context 10 commands

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

namespace CrowellExactSequence
noncomputable section
open scoped BigOperators commutatorElement
open FoxDifferential
open ProCGroups.ProC
universe u
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 · full declaration

theorem continuous_completedKernelBoundaryZC_of_continuous_zcUnivDiff
    (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H)
    [TopologicalSpace (ZCCompletedDifferentialModule C psi.toMonoidHom)]
    (hD : Continuous (fun g : G => zcUniversalDifferential C psi.toMonoidHom g)) :
    Continuous (completedKernelBoundaryProCInteger (G := G) (H := H) C psi) := by
  change Continuous fun n : ProfiniteKernelSubgroup psi =>
    Multiplicative.ofAdd (zcUniversalDifferential C psi.toMonoidHom n.1)
  exact continuous_ofAdd.comp (hD.comp continuous_subtype_val)

theorem

completedBoundaryKillsTopCommZC_of_continuous_zcUnivDiff

L332 ↗

CrowellExactSequence.completedBoundaryKillsTopCommZC_of_continuous_zcUnivDiff

Documentation

Well-definedness of \(d_N\) from continuity of the universal completed differential on the ambient group.

Source context 9 commands

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

namespace CrowellExactSequence
noncomputable section
open scoped BigOperators commutatorElement
open FoxDifferential
open ProCGroups.ProC
universe u
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · full declaration

theorem completedBoundaryKillsTopCommZC_of_continuous_zcUnivDiff
    (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H)
    [TopologicalSpace (ZCCompletedDifferentialModule C psi.toMonoidHom)]
    [T1Space (ZCCompletedDifferentialModule C psi.toMonoidHom)]
    (hD : Continuous (fun g : G => zcUniversalDifferential C psi.toMonoidHom g)) :
    CompletedBoundaryKillsTopologicalCommutatorProCInteger (G := G) (H := H) C psi :=
  completedBoundaryKillsTopologicalCommutatorProCInteger_of_continuousBoundary
    (G := G) (H := H) C psi
    (continuous_completedKernelBoundaryZC_of_continuous_zcUnivDiff
      (G := G) (H := H) C psi hD)

theorem

completedBoundaryKillsTopCommZC_of_continuous_kernel_familyCoords_fintype

L350 ↗

CrowellExactSequence.completedBoundaryKillsTopCommZC_of_continuous_kernel_familyCoords_fintype

Documentation

Finite-coordinate form of the topological well-definedness step for \(d_N\). If a finite coordinate system on \(A_{\psi}(C)\) identifies the universal differential on the kernel with a continuous coordinate-valued map, then the ordinary commutator-killing identity extends to \(\overline{[N,N]}\). In paper language, this is the passage from a continuous coordinate formula for \(D|_N\) to the well-defined map \(N^{\mathrm{ab}}(C) \to A_{\psi}(C)\).

Source context 9 commands

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

namespace CrowellExactSequence
noncomputable section
open scoped BigOperators commutatorElement
open FoxDifferential
open ProCGroups.ProC
universe u
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem completedBoundaryKillsTopCommZC_of_continuous_kernel_familyCoords_fintype
    (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H)
    {X : Type u} [Fintype X] (family : X → G)
    (hbasis_A :
      IsPresentedCompletedDifferentialFamilyBasisProCInteger
        (G := G) (H := H) C psi family)
    [T1Space (ZCFreeFoxCoordinates C (X := X) (H := H))]
    (Dcoords : ProfiniteKernelSubgroup psi →
      ZCFreeFoxCoordinates C (X := X) (H := H))
    (hDcoords_continuous : Continuous Dcoords)
    (hDcoords :
      ∀ n : ProfiniteKernelSubgroup psi,
        Dcoords n =
          presentedCompletedDifferentialFamilyCoordinatesProCInteger
            (G := G) (H := H) C psi family hbasis_A
            (zcUniversalDifferential C psi.toMonoidHom n.1)) :
    CompletedBoundaryKillsTopologicalCommutatorProCInteger (G := G) (H := H) C psi

theorem

completedBoundaryKillsTopCommZC_of_continuous_kernel_familyCoords

L429 ↗

CrowellExactSequence.completedBoundaryKillsTopCommZC_of_continuous_kernel_familyCoords

Documentation

Fin-indexed finite-coordinate form of the topological well-definedness step for \(d_N\).

Source context 9 commands

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

namespace CrowellExactSequence
noncomputable section
open scoped BigOperators commutatorElement
open FoxDifferential
open ProCGroups.ProC
universe u
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem completedBoundaryKillsTopCommZC_of_continuous_kernel_familyCoords
    (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H)
    {r : Nat} (family : Fin r → G)
    (hbasis_A :
      IsPresentedCompletedDifferentialFamilyBasisProCInteger
        (G := G) (H := H) C psi family)
    [T1Space (Fin r → ZCCompletedGroupAlgebra C H)]
    (Dcoords : ProfiniteKernelSubgroup psi → Fin r → ZCCompletedGroupAlgebra C H)
    (hDcoords_continuous : Continuous Dcoords)
    (hDcoords :
      ∀ n : ProfiniteKernelSubgroup psi,
        Dcoords n =
          presentedCompletedDifferentialFamilyCoordinatesProCInteger
            (G := G) (H := H) C psi family hbasis_A
            (zcUniversalDifferential C psi.toMonoidHom n.1)) :
    CompletedBoundaryKillsTopologicalCommutatorProCInteger (G := G) (H := H) C psi

theorem

completedBoundaryKillsTopCommZC_of_continuous_ambient_familyCoords_fintype

L510 ↗

CrowellExactSequence.completedBoundaryKillsTopCommZC_of_continuous_ambient_familyCoords_fintype

Documentation

Finite-coordinate ambient version of the completed-boundary theorem killing the top commutator subgroup. This is the form used when a continuous Fox-coordinate formula is constructed on the whole source and then restricted to \(\ker \psi\).

Source context 9 commands

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

namespace CrowellExactSequence
noncomputable section
open scoped BigOperators commutatorElement
open FoxDifferential
open ProCGroups.ProC
universe u
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem completedBoundaryKillsTopCommZC_of_continuous_ambient_familyCoords_fintype
    (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H)
    {X : Type u} [Fintype X] (family : X → G)
    (hbasis_A :
      IsPresentedCompletedDifferentialFamilyBasisProCInteger
        (G := G) (H := H) C psi family)
    [T1Space (ZCFreeFoxCoordinates C (X := X) (H := H))]
    (Dcoords : G → ZCFreeFoxCoordinates C (X := X) (H := H))
    (hDcoords_continuous : Continuous Dcoords)
    (hDcoords :
      ∀ n : ProfiniteKernelSubgroup psi,
        Dcoords n.1 =
          presentedCompletedDifferentialFamilyCoordinatesProCInteger
            (G := G) (H := H) C psi family hbasis_A
            (zcUniversalDifferential C psi.toMonoidHom n.1)) :
    CompletedBoundaryKillsTopologicalCommutatorProCInteger (G := G) (H := H) C psi

theorem

completedBoundaryKillsTopCommZC_of_continuous_ambient_familyCoords

L537 ↗

CrowellExactSequence.completedBoundaryKillsTopCommZC_of_continuous_ambient_familyCoords

Documentation

\(\operatorname{Fin}\)-indexed ambient-coordinate version of the completed-boundary theorem killing the top commutator subgroup for continuous kernel-family coordinates.

Source context 9 commands

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

namespace CrowellExactSequence
noncomputable section
open scoped BigOperators commutatorElement
open FoxDifferential
open ProCGroups.ProC
universe u
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem completedBoundaryKillsTopCommZC_of_continuous_ambient_familyCoords
    (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H)
    {r : Nat} (family : Fin r → G)
    (hbasis_A :
      IsPresentedCompletedDifferentialFamilyBasisProCInteger
        (G := G) (H := H) C psi family)
    [T1Space (Fin r → ZCCompletedGroupAlgebra C H)]
    (Dcoords : G → Fin r → ZCCompletedGroupAlgebra C H)
    (hDcoords_continuous : Continuous Dcoords)
    (hDcoords :
      ∀ n : ProfiniteKernelSubgroup psi,
        Dcoords n.1 =
          presentedCompletedDifferentialFamilyCoordinatesProCInteger
            (G := G) (H := H) C psi family hbasis_A
            (zcUniversalDifferential C psi.toMonoidHom n.1)) :
    CompletedBoundaryKillsTopologicalCommutatorProCInteger (G := G) (H := H) C psi

Module documentation

Boundary maps from the profinite kernel

Declarations