Module

Density.lean

Nyll.ProCGroups.FoxDifferential.Completed.FreeProC.Density

22 declarations indexed from sourceView source ↗

Module documentation

Fox differential: completed — free pro-\(C\) — density

The principal declarations in this module are:

HasLeftOpenSubgroupNeighbourhoodBasis

Left open subgroup neighborhood basis, expressed as a proposition rather than a structure. For every neighborhood \(U\) of \(y\), one can find an open subgroup \(V\) such that the left coset \(yV\) is contained in \(U\). This is the topological input used to pass from finite or open-subgroup approximations to ordinary closure.

HasLeftOpenNormalSubgroupNeighbourhoodBasis

This is the normal-subgroup version of the left open-subgroup neighborhood basis: in a profinite group, every identity neighborhood can be refined by an open normal subgroup.

subset_closure_of_open_neighbourhood_approximation

A point belongs to the set-theoretic closure of \(S\) when every open neighborhood of it contains an algebraic point of \(S\).

HasLeftOpenNormalSubgroupNeighbourhoodBasis.to_subgroup_basis

The normal-subgroup basis implies the subgroup basis.

Imports1

Nyll.ProCGroups.FoxDifferential.Completed.FreeProC.SemidirectLift

Imported by2

theorem

subset_closure_of_open_neighbourhood_approximation

L44 ↗

FoxDifferential.subset_closure_of_open_neighbourhood_approximation

Documentation

A point belongs to the set-theoretic closure of \(S\) when every open neighborhood of it contains an algebraic point of \(S\).

Source context 6 commands

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

namespace FoxDifferential
noncomputable section
universe u v
section GenericClosureAPI
variable {Y : Type u} [TopologicalSpace Y]
variable {S T : Set Y}

Lean source · statement

theorem subset_closure_of_open_neighbourhood_approximation
    (happrox :
      ∀ y : Y, y ∈ T → ∀ U : Set Y, IsOpen U → y ∈ U →
        ∃ s : Y, s ∈ S ∧ s ∈ U) :
    T ⊆ closure S

def

HasLeftOpenSubgroupNeighbourhoodBasis

L68 ↗

FoxDifferential.HasLeftOpenSubgroupNeighbourhoodBasis

Documentation

Source context 6 commands

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

namespace FoxDifferential
noncomputable section
universe u v
section OpenSubgroupClosureAPI
variable {Y : Type u} [Group Y] [TopologicalSpace Y]
variable {S T : Set Y}

Lean source · statement

def HasLeftOpenSubgroupNeighbourhoodBasis (Y : Type u) [Group Y] [TopologicalSpace Y] : Prop

def

HasLeftOpenNormalSubgroupNeighbourhoodBasis

L77 ↗

FoxDifferential.HasLeftOpenNormalSubgroupNeighbourhoodBasis

Documentation

This is the normal-subgroup version of the left open-subgroup neighborhood basis: in a profinite group, every identity neighborhood can be refined by an open normal subgroup.

Source context 6 commands

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

namespace FoxDifferential
noncomputable section
universe u v
section OpenSubgroupClosureAPI
variable {Y : Type u} [Group Y] [TopologicalSpace Y]
variable {S T : Set Y}

Lean source · statement

def HasLeftOpenNormalSubgroupNeighbourhoodBasis
    (Y : Type u) [Group Y] [TopologicalSpace Y] : Prop

theorem

to_subgroup_basis

L84 ↗

FoxDifferential.HasLeftOpenNormalSubgroupNeighbourhoodBasis.to_subgroup_basis

Documentation

The normal-subgroup basis implies the subgroup basis.

Source context 6 commands

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

namespace FoxDifferential
noncomputable section
universe u v
section OpenSubgroupClosureAPI
variable {Y : Type u} [Group Y] [TopologicalSpace Y]
variable {S T : Set Y}

Lean source · statement

theorem HasLeftOpenNormalSubgroupNeighbourhoodBasis.to_subgroup_basis
    (hbasis : HasLeftOpenNormalSubgroupNeighbourhoodBasis Y) :
    HasLeftOpenSubgroupNeighbourhoodBasis Y

theorem

subset_closure_of_openSubgroup_approximation

L95 ↗

FoxDifferential.subset_closure_of_openSubgroup_approximation

Documentation

If for every \(y \in T\) and every open subgroup \(V\) there is \(s \in S\) with \(y^{-1}s \in V\), then \(T\) is contained in the closure of \(S\).

Source context 6 commands

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

namespace FoxDifferential
noncomputable section
universe u v
section OpenSubgroupClosureAPI
variable {Y : Type u} [Group Y] [TopologicalSpace Y]
variable {S T : Set Y}

Lean source · statement

theorem subset_closure_of_openSubgroup_approximation
    (hbasis : HasLeftOpenSubgroupNeighbourhoodBasis Y)
    (happrox :
      ∀ y : Y, y ∈ T → ∀ V : Subgroup Y,
        IsOpen ((V : Subgroup Y) : Set Y) →
          ∃ s : Y, s ∈ S ∧ y⁻¹ * s ∈ V) :
    T ⊆ closure S

theorem

subset_closure_of_openNormalSubgroup_approximation

L114 ↗

FoxDifferential.subset_closure_of_openNormalSubgroup_approximation

Documentation

The completed Fox graph or boundary-cycle set lies in the required closed generated submodule by finite-stage separation.

Source context 6 commands

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

namespace FoxDifferential
noncomputable section
universe u v
section OpenSubgroupClosureAPI
variable {Y : Type u} [Group Y] [TopologicalSpace Y]
variable {S T : Set Y}

Lean source · statement

theorem subset_closure_of_openNormalSubgroup_approximation
    (hbasis : HasLeftOpenNormalSubgroupNeighbourhoodBasis Y)
    (happrox :
      ∀ y : Y, y ∈ T → ∀ V : Subgroup Y,
        V.Normal → IsOpen ((V : Subgroup Y) : Set Y) →
          ∃ s : Y, s ∈ S ∧ y⁻¹ * s ∈ V) :
    T ⊆ closure S

theorem

mem_closure_of_openSubgroup_approximation

L130 ↗

FoxDifferential.mem_closure_of_openSubgroup_approximation

Documentation

Coset approximation gives a pointwise closure statement.

Source context 6 commands

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

namespace FoxDifferential
noncomputable section
universe u v
section OpenSubgroupClosureAPI
variable {Y : Type u} [Group Y] [TopologicalSpace Y]
variable {S T : Set Y}

Lean source · statement

theorem mem_closure_of_openSubgroup_approximation
    (hbasis : HasLeftOpenSubgroupNeighbourhoodBasis Y)
    {y : Y}
    (happrox :
      ∀ V : Subgroup Y, IsOpen ((V : Subgroup Y) : Set Y) →
        ∃ s : Y, s ∈ S ∧ y⁻¹ * s ∈ V) :
    y ∈ closure S

def

HasLeftQuotientKernelNeighbourhoodBasis

L157 ↗

FoxDifferential.HasLeftQuotientKernelNeighbourhoodBasis

Documentation

A left neighborhood basis expressed directly by kernels of quotient maps. This is the form produced by finite-stage maps: every open neighborhood of \(y\) contains a left coset \(y\ker(\pi_j)\).

Source context 6 commands

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

namespace FoxDifferential
noncomputable section
universe u v
section QuotientKernelClosureAPI
variable {Y : Type u} [Group Y] [TopologicalSpace Y]
variable {S T : Set Y}

Lean source · statement

def HasLeftQuotientKernelNeighbourhoodBasis
    {J : Type v} {Q : J → Type*} [∀ j, Group (Q j)]
    (π : ∀ j : J, Y →* Q j) : Prop

theorem

subset_closure_of_quotientKernel_approximation

L169 ↗

FoxDifferential.subset_closure_of_quotientKernel_approximation

Documentation

If quotient kernels form a left neighborhood basis, then equality at every quotient stage gives closure. This is the abstract topology step for the remaining Crowell density theorem: finite quotient exactness supplies \(s\in S\) with \(\pi_j s = \pi_j y\); the quotient-kernel basis turns this into ordinary topological approximation.

Source context 6 commands

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

namespace FoxDifferential
noncomputable section
universe u v
section QuotientKernelClosureAPI
variable {Y : Type u} [Group Y] [TopologicalSpace Y]
variable {S T : Set Y}

Lean source · statement

theorem subset_closure_of_quotientKernel_approximation
    {J : Type v} {Q : J → Type*} [∀ j, Group (Q j)]
    (π : ∀ j : J, Y →* Q j)
    (hbasis : HasLeftQuotientKernelNeighbourhoodBasis (Y := Y) π)
    (happrox :
      ∀ y : Y, y ∈ T → ∀ j : J,
        ∃ s : Y, s ∈ S ∧ π j s = π j y) :
    T ⊆ closure S

def

freeProCZCCompletedFoxSemidirectKernelWordPoint

L207 ↗

FoxDifferential.freeProCZCCompletedFoxSemidirectKernelWordPoint

Documentation

The semidirect point \((D w, 1)\) attached to an abstract free-group kernel-word candidate. The word may or may not actually lie in the kernel; kernel membership is recorded separately by the corresponding kernel-cycle-set lemma.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
universe u v
section CompletedFoxDensity
open scoped Topology
variable {C : ProCGroups.FiniteGroupClass}
variable {X H : Type u}
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [DecidableEq X]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]

Lean source · statement

def freeProCZCCompletedFoxSemidirectKernelWordPoint (φ : X → H) (w : FreeGroup X) :
    ZCCompletedFoxSemidirect C X H

theorem

freeProCZCCompletedFoxSemidirectKernelWordPoint_left

L220 ↗

FoxDifferential.freeProCZCCompletedFoxSemidirectKernelWordPoint_left

Documentation

The left coordinate of a completed Fox semidirect kernel-word point is its completed Fox derivative vector.

Source context 12 commands

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

namespace FoxDifferential
noncomputable section
universe u v
section CompletedFoxDensity
open scoped Topology
variable {C : ProCGroups.FiniteGroupClass}
variable {X H : Type u}
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [DecidableEq X]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
omit [TopologicalSpace (ZCCompletedFoxSemidirect C X H)] [IsTopologicalGroup
    (ZCCompletedFoxSemidirect C X H)] in

Lean source · statement

theorem freeProCZCCompletedFoxSemidirectKernelWordPoint_left
    (φ : X → H) (w : FreeGroup X) :
    (freeProCZCCompletedFoxSemidirectKernelWordPoint (C := C) φ w).left =
      zcFreeGroupFoxDerivativeVector C (FreeGroup.lift φ) w

theorem

freeProCZCCompletedFoxSemidirectKernelWordPoint_right

L230 ↗

FoxDifferential.freeProCZCCompletedFoxSemidirectKernelWordPoint_right

Documentation

The right coordinate of a completed Fox semidirect kernel-word point is the identity element.

Source context 12 commands

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

namespace FoxDifferential
noncomputable section
universe u v
section CompletedFoxDensity
open scoped Topology
variable {C : ProCGroups.FiniteGroupClass}
variable {X H : Type u}
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [DecidableEq X]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
omit [TopologicalSpace (ZCCompletedFoxSemidirect C X H)] [IsTopologicalGroup
    (ZCCompletedFoxSemidirect C X H)] in

Lean source · statement

theorem freeProCZCCompletedFoxSemidirectKernelWordPoint_right
    (φ : X → H) (w : FreeGroup X) :
    (freeProCZCCompletedFoxSemidirectKernelWordPoint (C := C) φ w).right = 1

theorem

freeProCZCCompletedFoxSemidirectKernelWordPoint_mem_kernelCycleSet

L238 ↗

FoxDifferential.freeProCZCCompletedFoxSemidirectKernelWordPoint_mem_kernelCycleSet

Documentation

A genuine kernel word gives an element of the algebraic kernel-word cycle set.

Source context 12 commands

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

namespace FoxDifferential
noncomputable section
universe u v
section CompletedFoxDensity
open scoped Topology
variable {C : ProCGroups.FiniteGroupClass}
variable {X H : Type u}
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [DecidableEq X]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
omit [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
  [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)] in

Lean source · statement

theorem freeProCZCCompletedFoxSemidirectKernelWordPoint_mem_kernelCycleSet
    (φ : X → H) {w : FreeGroup X} (hw : FreeGroup.lift φ w = 1) :
    freeProCZCCompletedFoxSemidirectKernelWordPoint (C := C) φ w ∈
      freeProCZCCompletedFoxSemidirectKernelCycleSet (C := C) φ

theorem

mem_freeProCZCCompletedFoxSemidirectKernelCycleSet_iff

L250 ↗

FoxDifferential.mem_freeProCZCCompletedFoxSemidirectKernelCycleSet_iff

Documentation

Membership in the completed Fox semidirect kernel-cycle set is equivalent to vanishing of the corresponding finite-stage coordinate.

Source context 12 commands

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

namespace FoxDifferential
noncomputable section
universe u v
section CompletedFoxDensity
open scoped Topology
variable {C : ProCGroups.FiniteGroupClass}
variable {X H : Type u}
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [DecidableEq X]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
omit [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
  [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)] in

Lean source · statement

theorem mem_freeProCZCCompletedFoxSemidirectKernelCycleSet_iff
    {φ : X → H}
    {y : ZCCompletedFoxSemidirect C X H} :
    y ∈ freeProCZCCompletedFoxSemidirectKernelCycleSet (C := C) φ ↔
      ∃ w : FreeGroup X, FreeGroup.lift φ w = 1 ∧
        y = freeProCZCCompletedFoxSemidirectKernelWordPoint (C := C) φ w

theorem

freeProCZCCompletedFoxSemidirectBoundaryCycleSet_mk_iff

L269 ↗

FoxDifferential.freeProCZCCompletedFoxSemidirectBoundaryCycleSet_mk_iff

Documentation

Boundary-cycle membership for a point of the form \((v,1)\).

Source context 13 commands

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

namespace FoxDifferential
noncomputable section
universe u v
section CompletedFoxDensity
open scoped Topology
variable {C : ProCGroups.FiniteGroupClass}
variable {X H : Type u}
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [DecidableEq X]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
omit [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
  [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)] in
omit [DecidableEq X] in

Lean source · statement

theorem freeProCZCCompletedFoxSemidirectBoundaryCycleSet_mk_iff
    [Fintype X] {φ : X → H}
    {v : ZCFreeFoxCoordinates C (X := X) (H := H)} :
    ({ left := v, right := (1 : H) } :
        ZCCompletedFoxSemidirect C X H) ∈
      freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ ↔
        zcFreeGroupFoxBoundary C (FreeGroup.lift φ) v = 0

theorem

freeProCZCFoxBoundaryCycles_subset_closure_kernelCycleSet_of_quotKernel_approx

L289 ↗

FoxDifferential.freeProCZCFoxBoundaryCycles_subset_closure_kernelCycleSet_of_quotKernel_approx

Documentation

Quotient-kernel approximation form of the completed Fox density statement. This is the finite-stage attack surface for the remaining density theorem: once finite quotient exactness produces, for every finite quotient stage j, a kernel word whose semidirect point has the same j-th quotient image as the boundary cycle, the completed density statement follows.

Source context 12 commands

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

namespace FoxDifferential
noncomputable section
universe u v
section CompletedFoxDensity
open scoped Topology
variable {C : ProCGroups.FiniteGroupClass}
variable {X H : Type u}
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [DecidableEq X]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
omit [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)] in

Lean source · statement

theorem freeProCZCFoxBoundaryCycles_subset_closure_kernelCycleSet_of_quotKernel_approx
    [Fintype X] (φ : X → H)
    {J : Type v} {Q : J → Type*} [∀ j, Group (Q j)]
    (π : ∀ j : J,
      ZCCompletedFoxSemidirect C X H →* Q j)
    (hbasis :
      HasLeftQuotientKernelNeighbourhoodBasis
        (Y := ZCCompletedFoxSemidirect C X H) π)
    (happrox :
      ∀ y : ZCCompletedFoxSemidirect C X H,
        y ∈ freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ →
          ∀ j : J,
            ∃ w : FreeGroup X,
              FreeGroup.lift φ w = 1 ∧
                π j (freeProCZCCompletedFoxSemidirectKernelWordPoint
                    (C := C) φ w) = π j y) :
    freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ ⊆
      closure (freeProCZCCompletedFoxSemidirectKernelCycleSet (C := C) φ)

theorem

freeProCZCFoxBoundaryCycles_subset_closure_kernelCycleSet_of_open_neighbourhood_approx

L326 ↗

FoxDifferential.freeProCZCFoxBoundaryCycles_subset_closure_kernelCycleSet_of_open_neighbourhood_approx

Documentation

For every boundary cycle and every open neighborhood in the completed semidirect product, there is a genuine kernel word whose point \((D w, 1)\) lies in that neighborhood; this is the density statement used by Crowell middle exactness.

Source context 12 commands

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

namespace FoxDifferential
noncomputable section
universe u v
section CompletedFoxDensity
open scoped Topology
variable {C : ProCGroups.FiniteGroupClass}
variable {X H : Type u}
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [DecidableEq X]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
omit [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)] in

Lean source · statement

theorem freeProCZCFoxBoundaryCycles_subset_closure_kernelCycleSet_of_open_neighbourhood_approx
    [Fintype X] (φ : X → H)
    (happrox :
      ∀ y : ZCCompletedFoxSemidirect C X H,
        y ∈ freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ →
          ∀ U : Set (ZCCompletedFoxSemidirect C X H),
            IsOpen U → y ∈ U →
              ∃ w : FreeGroup X,
                FreeGroup.lift φ w = 1 ∧
                freeProCZCCompletedFoxSemidirectKernelWordPoint (C := C) φ w ∈ U) :
    freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ ⊆
      closure (freeProCZCCompletedFoxSemidirectKernelCycleSet (C := C) φ)

theorem

freeProCZCFoxBoundaryCycles_subset_closure_kernelCycleSet_of_openSubgroup_approx

L350 ↗

FoxDifferential.freeProCZCFoxBoundaryCycles_subset_closure_kernelCycleSet_of_openSubgroup_approx

Documentation

For every open subgroup \(V\) of the completed Fox semidirect group, a boundary cycle \(y\) is approximated by a kernel-word cycle point modulo the left coset \(yV\).

Source context 12 commands

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

namespace FoxDifferential
noncomputable section
universe u v
section CompletedFoxDensity
open scoped Topology
variable {C : ProCGroups.FiniteGroupClass}
variable {X H : Type u}
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [DecidableEq X]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
omit [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)] in

Lean source · statement

theorem freeProCZCFoxBoundaryCycles_subset_closure_kernelCycleSet_of_openSubgroup_approx
    [Fintype X] (φ : X → H)
    (hbasis :
      HasLeftOpenSubgroupNeighbourhoodBasis
        (ZCCompletedFoxSemidirect C X H))
    (happrox :
      ∀ y : ZCCompletedFoxSemidirect C X H,
        y ∈ freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ →
          ∀ V : Subgroup (ZCCompletedFoxSemidirect C X H),
            IsOpen ((V : Subgroup
              (ZCCompletedFoxSemidirect C X H)) : Set
              (ZCCompletedFoxSemidirect C X H)) →
              ∃ w : FreeGroup X,
                FreeGroup.lift φ w = 1 ∧
                y⁻¹ * freeProCZCCompletedFoxSemidirectKernelWordPoint
                    (C := C) φ w ∈ V) :
    freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ ⊆
      closure (freeProCZCCompletedFoxSemidirectKernelCycleSet (C := C) φ)

theorem

freeProCZCFoxBoundaryCycles_subset_closure_kernelCycleSet_of_openNormalSubgroup_approx

L383 ↗

FoxDifferential.freeProCZCFoxBoundaryCycles_subset_closure_kernelCycleSet_of_openNormalSubgroup_approx

Documentation

Open-normal-subgroup approximation form of the completed Fox density statement.

Source context 12 commands

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

namespace FoxDifferential
noncomputable section
universe u v
section CompletedFoxDensity
open scoped Topology
variable {C : ProCGroups.FiniteGroupClass}
variable {X H : Type u}
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [DecidableEq X]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
omit [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)] in

Lean source · statement

theorem freeProCZCFoxBoundaryCycles_subset_closure_kernelCycleSet_of_openNormalSubgroup_approx
    [Fintype X] (φ : X → H)
    (hbasis :
      HasLeftOpenNormalSubgroupNeighbourhoodBasis
        (ZCCompletedFoxSemidirect C X H))
    (happrox :
      ∀ y : ZCCompletedFoxSemidirect C X H,
        y ∈ freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ →
          ∀ V : Subgroup (ZCCompletedFoxSemidirect C X H),
            V.Normal →
            IsOpen ((V : Subgroup
              (ZCCompletedFoxSemidirect C X H)) : Set
              (ZCCompletedFoxSemidirect C X H)) →
              ∃ w : FreeGroup X,
                FreeGroup.lift φ w = 1 ∧
                y⁻¹ * freeProCZCCompletedFoxSemidirectKernelWordPoint
                    (C := C) φ w ∈ V) :
    freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ ⊆
      closure (freeProCZCCompletedFoxSemidirectKernelCycleSet (C := C) φ)

theorem

freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_openSubgroup_approx

L419 ↗

FoxDifferential.freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_openSubgroup_approx

Documentation

Open-subgroup approximation places every completed boundary cycle inside the closed generated Fox graph target.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
universe u v
section CompletedFoxDensity
open scoped Topology
variable {C : ProCGroups.FiniteGroupClass}
variable {X H : Type u}
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [DecidableEq X]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]

Lean source · statement

theorem freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_openSubgroup_approx
    [Fintype X] (φ : X → H)
    (hbasis :
      HasLeftOpenSubgroupNeighbourhoodBasis
        (ZCCompletedFoxSemidirect C X H))
    (happrox :
      ∀ y : ZCCompletedFoxSemidirect C X H,
        y ∈ freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ →
          ∀ V : Subgroup (ZCCompletedFoxSemidirect C X H),
            IsOpen ((V : Subgroup
              (ZCCompletedFoxSemidirect C X H)) : Set
              (ZCCompletedFoxSemidirect C X H)) →
              ∃ w : FreeGroup X,
                FreeGroup.lift φ w = 1 ∧
                y⁻¹ * freeProCZCCompletedFoxSemidirectKernelWordPoint
                    (C := C) φ w ∈ V) :
    freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ ⊆
      ((freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
          (ZCCompletedFoxSemidirect C X H)) : Set
          (ZCCompletedFoxSemidirect C X H))

theorem

freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_openNormalSubgroup_approx

L448 ↗

FoxDifferential.freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_openNormalSubgroup_approx

Documentation

Open-normal-subgroup approximation places every completed boundary cycle inside the closed generated Fox graph target.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
universe u v
section CompletedFoxDensity
open scoped Topology
variable {C : ProCGroups.FiniteGroupClass}
variable {X H : Type u}
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [DecidableEq X]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]

Lean source · statement

theorem freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_openNormalSubgroup_approx
    [Fintype X] (φ : X → H)
    (hbasis :
      HasLeftOpenNormalSubgroupNeighbourhoodBasis
        (ZCCompletedFoxSemidirect C X H))
    (happrox :
      ∀ y : ZCCompletedFoxSemidirect C X H,
        y ∈ freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ →
          ∀ V : Subgroup (ZCCompletedFoxSemidirect C X H),
            V.Normal →
            IsOpen ((V : Subgroup
              (ZCCompletedFoxSemidirect C X H)) : Set
              (ZCCompletedFoxSemidirect C X H)) →
              ∃ w : FreeGroup X,
                FreeGroup.lift φ w = 1 ∧
                y⁻¹ * freeProCZCCompletedFoxSemidirectKernelWordPoint
                    (C := C) φ w ∈ V) :
    freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ ⊆
      ((freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
          (ZCCompletedFoxSemidirect C X H)) : Set
          (ZCCompletedFoxSemidirect C X H))

theorem

closure_freeProCZCFoxSemiKernelCycleSet_eq_boundaryCycleSet_of_openSubgroup_approx

L479 ↗

FoxDifferential.closure_freeProCZCFoxSemiKernelCycleSet_eq_boundaryCycleSet_of_openSubgroup_approx

Documentation

Under the standard continuity inputs, open-subgroup approximation upgrades the one-sided closure statement to the equality between boundary cycles and the closure of kernel-word cycles.

Source context 12 commands

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

namespace FoxDifferential
noncomputable section
universe u v
section CompletedFoxDensity
open scoped Topology
variable {C : ProCGroups.FiniteGroupClass}
variable {X H : Type u}
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [DecidableEq X]
variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
omit [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)] in

Lean source · full declaration

theorem closure_freeProCZCFoxSemiKernelCycleSet_eq_boundaryCycleSet_of_openSubgroup_approx
    [Fintype X] [T1Space H]
    [TopologicalSpace (ZCCompletedGroupAlgebra C H)]
    [T1Space (ZCCompletedGroupAlgebra C H)]
    (φ : X → H)
    (hleft :
      Continuous
        (fun y : ZCCompletedFoxSemidirect C X H => y.left))
    (hright :
      Continuous
        (fun y : ZCCompletedFoxSemidirect C X H => y.right))
    (hboundary :
      Continuous
        (zcFreeGroupFoxBoundary C (FreeGroup.lift φ)))
    (hbasis :
      HasLeftOpenSubgroupNeighbourhoodBasis
        (ZCCompletedFoxSemidirect C X H))
    (happrox :
      ∀ y : ZCCompletedFoxSemidirect C X H,
        y ∈ freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ →
          ∀ V : Subgroup (ZCCompletedFoxSemidirect C X H),
            IsOpen ((V : Subgroup
              (ZCCompletedFoxSemidirect C X H)) : Set
              (ZCCompletedFoxSemidirect C X H)) →
              ∃ w : FreeGroup X,
                FreeGroup.lift φ w = 1 ∧
                y⁻¹ * freeProCZCCompletedFoxSemidirectKernelWordPoint
                    (C := C) φ w ∈ V) :
    closure (freeProCZCCompletedFoxSemidirectKernelCycleSet (C := C) φ) =
      freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ := by
  exact
    (closure_freeProCZCFoxSemiKernelCycleSet_eq_boundaryCycleSet_iff_density (C := C) (φ := φ)
        hleft hright hboundary).2
      (freeProCZCFoxBoundaryCycles_subset_closure_kernelCycleSet_of_openSubgroup_approx
        (C := C) φ hbasis happrox)

Module documentation

Fox differential: completed — free pro-\(C\) — density

Declarations