NYLL
Module

RelationSubmoduleApproximation.lean

Nyll.ProCGroups.FoxDifferential.Completed.FreeProC.RelationSubmoduleApproximation
6 declarations indexed from sourceView source ↗

Module documentation

Fox differential: completed — free pro-\(C\) — relation submodule approximation

The principal declarations in this module are:

  • boundaryCycles_subset_kernelClosure_of_relSubmoduleExact

Completed Fox density from finite-stage relation-submodule exactness.

  • freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_finiteStage_relSubmodule_exact

The same finite relation-submodule input places completed boundary cycles in the closed generated Fox graph target.

  • boundaryCycles_subset_kernelClosure_of_sourceBoundaryReduction

Completed Fox density holds when, at every finite stage, every source-coordinate lift whose source boundary lies in the explicit relation augmentation ideal projects to a relation-boundary vector.

  • boundaryCycles_subset_closedGenTarget_of_sourceBoundaryReduction

The source-boundary relation-ideal route also places completed boundary cycles inside the closed-generated Fox graph target.

Imports3
Imported by2

Declarations

theorem

boundaryCycles_subset_kernelClosure_of_relSubmoduleExact

L48 ↗
FoxDifferential.boundaryCycles_subset_kernelClosure_of_relSubmoduleExact
Documentation

Completed Fox density from finite-stage relation-submodule exactness.

Source context 12 commands

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

namespace FoxDifferential
noncomputable section
universe u v
section CompletedFoxRelationSubmoduleExact
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 boundaryCycles_subset_kernelClosure_of_relSubmoduleExact
    [Fintype X] (φ : X → H)
    {J : Type v}
    (Nstage : J → Subgroup (FreeGroup X))
    [∀ j, (Nstage j).Normal]
    (nstage : J → ℕ)
    (π : ∀ j : J,
      ZCCompletedFoxSemidirect C X H →*
        FoxAlgebraicStageSemidirect (X := X) (Nstage j) (nstage j))
    (hbasis :
      HasLeftQuotientKernelNeighbourhoodBasis
        (Y := ZCCompletedFoxSemidirect C X H) π)
    (hboundary_stage :
      ∀ y : ZCCompletedFoxSemidirect C X H,
        y ∈ freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ →
          ∀ j : J,
            π j y ∈ foxAlgebraicStageSemidirectBoundaryCycleSet
              (X := X) (Nstage j) (nstage j))
    (hstage_module_exact :
      ∀ j : J,
        foxAlgebraicStageRelationBoundaryModuleExact
          (X := X) (Nstage j) (nstage j))
    (hNstage_kernel :
      ∀ j : J, ∀ {w : FreeGroup X}, w ∈ Nstage j → FreeGroup.lift φ w = 1)
    (hkernel_word_projection :
      ∀ j : J, ∀ w : FreeGroup X, w ∈ Nstage j →
        π j (freeProCZCCompletedFoxSemidirectKernelWordPoint (C := C) φ w) =
          foxAlgebraicStageSemidirectKernelWordPoint (X := X) (Nstage j) (nstage j) w) :
    freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ ⊆
      closure (freeProCZCCompletedFoxSemidirectKernelCycleSet (C := C) φ)
theorem

freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_finiteStage_relSubmodule_exact

L90 ↗
FoxDifferential.freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_finiteStage_relSubmodule_exact
Documentation

The same finite relation-submodule input places completed boundary cycles in 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 CompletedFoxRelationSubmoduleExact
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_finiteStage_relSubmodule_exact
    [Fintype X] (φ : X → H)
    {J : Type v}
    (Nstage : J → Subgroup (FreeGroup X))
    [∀ j, (Nstage j).Normal]
    (nstage : J → ℕ)
    (π : ∀ j : J,
      ZCCompletedFoxSemidirect C X H →*
        FoxAlgebraicStageSemidirect (X := X) (Nstage j) (nstage j))
    (hbasis :
      HasLeftQuotientKernelNeighbourhoodBasis
        (Y := ZCCompletedFoxSemidirect C X H) π)
    (hboundary_stage :
      ∀ y : ZCCompletedFoxSemidirect C X H,
        y ∈ freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ →
          ∀ j : J,
            π j y ∈ foxAlgebraicStageSemidirectBoundaryCycleSet
              (X := X) (Nstage j) (nstage j))
    (hstage_module_exact :
      ∀ j : J,
        foxAlgebraicStageRelationBoundaryModuleExact
          (X := X) (Nstage j) (nstage j))
    (hNstage_kernel :
      ∀ j : J, ∀ {w : FreeGroup X}, w ∈ Nstage j → FreeGroup.lift φ w = 1)
    (hkernel_word_projection :
      ∀ j : J, ∀ w : FreeGroup X, w ∈ Nstage j →
        π j (freeProCZCCompletedFoxSemidirectKernelWordPoint (C := C) φ w) =
          foxAlgebraicStageSemidirectKernelWordPoint (X := X) (Nstage j) (nstage j) w) :
    freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ ⊆
      ((freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
          (ZCCompletedFoxSemidirect C X H)) : Set
          (ZCCompletedFoxSemidirect C X H))
theorem

boundaryCycles_subset_kernelClosure_of_sourceBoundaryReduction

L134 ↗
FoxDifferential.boundaryCycles_subset_kernelClosure_of_sourceBoundaryReduction
Documentation

Completed Fox density holds when, at every finite stage, every source-coordinate lift whose source boundary lies in the explicit relation augmentation ideal projects to a relation-boundary vector.

Source context 12 commands

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

namespace FoxDifferential
noncomputable section
universe u v
section CompletedFoxRelationSubmoduleExact
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 boundaryCycles_subset_kernelClosure_of_sourceBoundaryReduction
    [Fintype X] (φ : X → H)
    {J : Type v}
    (Nstage : J → Subgroup (FreeGroup X))
    [∀ j, (Nstage j).Normal]
    (nstage : J → ℕ)
    (π : ∀ j : J,
      ZCCompletedFoxSemidirect C X H →*
        FoxAlgebraicStageSemidirect (X := X) (Nstage j) (nstage j))
    (hbasis :
      HasLeftQuotientKernelNeighbourhoodBasis
        (Y := ZCCompletedFoxSemidirect C X H) π)
    (hboundary_stage :
      ∀ y : ZCCompletedFoxSemidirect C X H,
        y ∈ freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ →
          ∀ j : J,
            π j y ∈ foxAlgebraicStageSemidirectBoundaryCycleSet
              (X := X) (Nstage j) (nstage j))
    (hstage_reduce :
      ∀ j : J,
        foxAlgebraicStageSourceBoundaryRelationIdealReduction
          (X := X) (Nstage j) (nstage j))
    (hNstage_kernel :
      ∀ j : J, ∀ {w : FreeGroup X}, w ∈ Nstage j → FreeGroup.lift φ w = 1)
    (hkernel_word_projection :
      ∀ j : J, ∀ w : FreeGroup X, w ∈ Nstage j →
        π j (freeProCZCCompletedFoxSemidirectKernelWordPoint (C := C) φ w) =
          foxAlgebraicStageSemidirectKernelWordPoint (X := X) (Nstage j) (nstage j) w) :
    freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ ⊆
      closure (freeProCZCCompletedFoxSemidirectKernelCycleSet (C := C) φ)
theorem

boundaryCycles_subset_closedGenTarget_of_sourceBoundaryReduction

L176 ↗
FoxDifferential.boundaryCycles_subset_closedGenTarget_of_sourceBoundaryReduction
Documentation

The source-boundary relation-ideal route also places completed boundary cycles 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 CompletedFoxRelationSubmoduleExact
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 boundaryCycles_subset_closedGenTarget_of_sourceBoundaryReduction
    [Fintype X] (φ : X → H)
    {J : Type v}
    (Nstage : J → Subgroup (FreeGroup X))
    [∀ j, (Nstage j).Normal]
    (nstage : J → ℕ)
    (π : ∀ j : J,
      ZCCompletedFoxSemidirect C X H →*
        FoxAlgebraicStageSemidirect (X := X) (Nstage j) (nstage j))
    (hbasis :
      HasLeftQuotientKernelNeighbourhoodBasis
        (Y := ZCCompletedFoxSemidirect C X H) π)
    (hboundary_stage :
      ∀ y : ZCCompletedFoxSemidirect C X H,
        y ∈ freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ →
          ∀ j : J,
            π j y ∈ foxAlgebraicStageSemidirectBoundaryCycleSet
              (X := X) (Nstage j) (nstage j))
    (hstage_reduce :
      ∀ j : J,
        foxAlgebraicStageSourceBoundaryRelationIdealReduction
          (X := X) (Nstage j) (nstage j))
    (hNstage_kernel :
      ∀ j : J, ∀ {w : FreeGroup X}, w ∈ Nstage j → FreeGroup.lift φ w = 1)
    (hkernel_word_projection :
      ∀ j : J, ∀ w : FreeGroup X, w ∈ Nstage j →
        π j (freeProCZCCompletedFoxSemidirectKernelWordPoint (C := C) φ w) =
          foxAlgebraicStageSemidirectKernelWordPoint (X := X) (Nstage j) (nstage j) w) :
    freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ ⊆
      ((freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
          (ZCCompletedFoxSemidirect C X H)) : Set
          (ZCCompletedFoxSemidirect C X H))
theorem

freeProCZCFoxBoundaryCycles_subset_closure_kernelCycleSet_of_finiteStage_relDeriv

L222 ↗
FoxDifferential.freeProCZCFoxBoundaryCycles_subset_closure_kernelCycleSet_of_finiteStage_relDeriv
Documentation

The finite-stage relation-ideal derivative theorem, quotient-kernel neighborhood basis, and projection compatibility imply completed Fox density.

Source context 13 commands

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

namespace FoxDifferential
noncomputable section
universe u v
section CompletedFoxRelationSubmoduleExact
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)]
section
omit [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
Lean source · statement
theorem freeProCZCFoxBoundaryCycles_subset_closure_kernelCycleSet_of_finiteStage_relDeriv
    [Fintype X] (φ : X → H)
    {J : Type v}
    (Nstage : J → Subgroup (FreeGroup X))
    [∀ j, (Nstage j).Normal]
    (nstage : J → ℕ)
    (π : ∀ j : J,
      ZCCompletedFoxSemidirect C X H →*
        FoxAlgebraicStageSemidirect (X := X) (Nstage j) (nstage j))
    (hbasis :
      HasLeftQuotientKernelNeighbourhoodBasis
        (Y := ZCCompletedFoxSemidirect C X H) π)
    (hboundary_stage :
      ∀ y : ZCCompletedFoxSemidirect C X H,
        y ∈ freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ →
          ∀ j : J,
            π j y ∈ foxAlgebraicStageSemidirectBoundaryCycleSet
              (X := X) (Nstage j) (nstage j))
    (hNstage_kernel :
      ∀ j : J, ∀ {w : FreeGroup X}, w ∈ Nstage j → FreeGroup.lift φ w = 1)
    (hkernel_word_projection :
      ∀ j : J, ∀ w : FreeGroup X, w ∈ Nstage j →
        π j (freeProCZCCompletedFoxSemidirectKernelWordPoint (C := C) φ w) =
          foxAlgebraicStageSemidirectKernelWordPoint (X := X) (Nstage j) (nstage j) w) :
    freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ ⊆
      closure (freeProCZCCompletedFoxSemidirectKernelCycleSet (C := C) φ)
theorem

freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_finiteStage_relDeriv

L262 ↗
FoxDifferential.freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_finiteStage_relDeriv
Documentation

Completed boundary cycles lie in the closed-generated Fox graph target using the finite-stage relation-ideal derivative theorem.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
universe u v
section CompletedFoxRelationSubmoduleExact
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_finiteStage_relDeriv
    [Fintype X] (φ : X → H)
    {J : Type v}
    (Nstage : J → Subgroup (FreeGroup X))
    [∀ j, (Nstage j).Normal]
    (nstage : J → ℕ)
    (π : ∀ j : J,
      ZCCompletedFoxSemidirect C X H →*
        FoxAlgebraicStageSemidirect (X := X) (Nstage j) (nstage j))
    (hbasis :
      HasLeftQuotientKernelNeighbourhoodBasis
        (Y := ZCCompletedFoxSemidirect C X H) π)
    (hboundary_stage :
      ∀ y : ZCCompletedFoxSemidirect C X H,
        y ∈ freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ →
          ∀ j : J,
            π j y ∈ foxAlgebraicStageSemidirectBoundaryCycleSet
              (X := X) (Nstage j) (nstage j))
    (hNstage_kernel :
      ∀ j : J, ∀ {w : FreeGroup X}, w ∈ Nstage j → FreeGroup.lift φ w = 1)
    (hkernel_word_projection :
      ∀ j : J, ∀ w : FreeGroup X, w ∈ Nstage j →
        π j (freeProCZCCompletedFoxSemidirectKernelWordPoint (C := C) φ w) =
          foxAlgebraicStageSemidirectKernelWordPoint (X := X) (Nstage j) (nstage j) w) :
    freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ ⊆
      ((freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
          (ZCCompletedFoxSemidirect C X H)) : Set
          (ZCCompletedFoxSemidirect C X H))

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