Yamaguchi Lean 4 Library
ProCGroups.FoxDifferential.Completed.FreeProC.StageApproximation
ProCGroups/FoxDifferential/Completed/FreeProC/StageApproximation

ProCGroups.FoxDifferential.Completed.FreeProC.StageApproximation

6 Theorems

The principal declarations in this module are:

  • subset_closure_of_quotientKernel_stage_exact Quotient-kernel density from exact finite-stage images. For each quotient stage \(j\), let \(T_{\mathrm{stage}}(j)\) be the image condition satisfied by points of \(T\), and let \(S_{\mathrm{stage}}(j)\) be the finite-stage image of algebraic approximants from \(S\). If every \(T_{\mathrm{stage}}\) point is in \(S_{\mathrm{stage}}\), and every \(S_{\mathrm{stage}}\) point lifts to an actual point of \(S\), then \(T\) is contained in the closure of \(S\). - freeProCZCFoxBoundaryCycles_subset_closure_kernelCycleSet_of_stage_exact Completed Fox density under quotient-stage boundary inclusion, finite-stage exactness, and kernel-word lifting hypotheses. - freeProCZCFoxBoundaryCycles_subset_closure_kernelCycleSet_of_finiteStage_semi_exact Completed Fox density from finite semidirect Fox exactness at every quotient stage. Here the finite-stage \(T_{\mathrm{stage}}\) is the set of finite semidirect boundary cycles and the finite-stage \(S_{\mathrm{stage}}\) is the set of actual kernel-word derivative points. The hypotheses that remain are the actual comparison data between completed stages and finite Fox stages. - freeProCZCFoxBoundaryCycles_subset_closure_graphWordSet_of_finiteStage_semi_exact Completed Fox graph-word density from finite semidirect Fox exactness at every quotient stage. This is the finite-quotient form that does not assume that words in the finite relation subgroup \(N_{\mathrm{stage},j}\) to be actual kernel words for \(\varphi\). A word \(w \in N_{\mathrm{stage},j}\) only has to project to the trivial right coordinate at the \(j\)-th finite stage; the completed approximant remains the genuine graph point \((D w, \varphi(w))\).
imports
Imported by

Declarations

Theorem FoxDifferential.subset_closure_of_quotientKernel_stage_exact 
theorem subset_closure_of_quotientKernel_stage_exact
    {J : Type v} {Q : J → Type*} [∀ j, Group (Q j)]
    (π : ∀ j : J, Y →* Q j)
    (hbasis : HasLeftQuotientKernelNeighbourhoodBasis (Y := Y) π)
    (Sstage Tstage : ∀ j : J, Set (Q j))
    (hTstage : ∀ y : Y, y ∈ T → ∀ j : J, π j y ∈ Tstage j)
    (hstage_exact : ∀ j : J, Tstage j ⊆ Sstage j)
    (hlift_stage : ∀ j : J, ∀ q : Q j, q ∈ Sstage j →
      ∃ s : Y, s ∈ S ∧ π j s = q) :
    T ⊆ closure S

Quotient-kernel density from exact finite-stage images. For each quotient stage \(j\), let \(T_{\mathrm{stage}}(j)\) be the image condition satisfied by points of \(T\), and let \(S_{\mathrm{stage}}(j)\) be the finite-stage image of algebraic approximants from \(S\). If every \(T_{\mathrm{stage}}\) point is in \(S_{\mathrm{stage}}\), and every \(S_{\mathrm{stage}}\) point lifts to an actual point of \(S\), then \(T\) is contained in the closure of \(S\).

Show Lean proof
Theorem FoxDifferential.freeProCZCFoxBoundaryCycles_subset_closure_kernelCycleSet_of_stage_exact 
omit [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)] in
theorem freeProCZCFoxBoundaryCycles_subset_closure_kernelCycleSet_of_stage_exact
    [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) π)
    (Sstage Tstage : ∀ j : J, Set (Q j))
    (hboundary_stage :
      ∀ y : ZCCompletedFoxSemidirect C X H,
        y ∈ freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ →
          ∀ j : J, π j y ∈ Tstage j)
    (hstage_exact : ∀ j : J, Tstage j ⊆ Sstage j)
    (hlift_stage :
      ∀ j : J, ∀ q : Q j, q ∈ Sstage j →
        ∃ w : FreeGroup X,
          FreeGroup.lift φ w = 1 ∧
            π j (freeProCZCCompletedFoxSemidirectKernelWordPoint (C := C) φ w) = q) :
    freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ ⊆
      closure (freeProCZCCompletedFoxSemidirectKernelCycleSet (C := C) φ)

Completed Fox density under quotient-stage boundary inclusion, finite-stage exactness, and kernel-word lifting hypotheses.

Show Lean proof
Theorem FoxDifferential.freeProCZCFoxBoundaryCycles_subset_closure_kernelCycleSet_of_finiteStage_semi_exact 
omit [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)] in
theorem freeProCZCFoxBoundaryCycles_subset_closure_kernelCycleSet_of_finiteStage_semi_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_exact :
      ∀ j : J,
        foxAlgebraicStageBoundaryCyclesCoveredBySourceKernel
          (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) φ)

Completed Fox density from finite semidirect Fox exactness at every quotient stage. Here the finite-stage \(T_{\mathrm{stage}}\) is the set of finite semidirect boundary cycles and the finite-stage \(S_{\mathrm{stage}}\) is the set of actual kernel-word derivative points. The hypotheses that remain are the actual comparison data between completed stages and finite Fox stages.

Show Lean proof
Theorem FoxDifferential.freeProCZCFoxBoundaryCycles_subset_closure_graphWordSet_of_finiteStage_semi_exact 
omit [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)] in
theorem freeProCZCFoxBoundaryCycles_subset_closure_graphWordSet_of_finiteStage_semi_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_exact :
      ∀ j : J,
        foxAlgebraicStageBoundaryCyclesCoveredBySourceKernel
          (X := X) (Nstage j) (nstage j))
    (hgraph_word_projection :
      ∀ j : J, ∀ w : FreeGroup X, w ∈ Nstage j →
        π j (freeProCZCCompletedFoxSemidirectGraphWordPoint (C := C) φ w) =
          foxAlgebraicStageSemidirectKernelWordPoint (X := X) (Nstage j) (nstage j) w) :
    freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ ⊆
      closure (freeProCZCCompletedFoxSemidirectGraphWordSet (C := C) φ)

Completed Fox graph-word density from finite semidirect Fox exactness at every quotient stage. This is the finite-quotient form that does not assume that words in the finite relation subgroup \(N_{\mathrm{stage},j}\) to be actual kernel words for \(\varphi\). A word \(w \in N_{\mathrm{stage},j}\) only has to project to the trivial right coordinate at the \(j\)-th finite stage; the completed approximant remains the genuine graph point \((D w, \varphi(w))\).

Show Lean proof
Theorem FoxDifferential.freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_finiteStage_graphWord_semi_exact 
theorem freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_finiteStage_graphWord_semi_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_exact :
      ∀ j : J,
        foxAlgebraicStageBoundaryCyclesCoveredBySourceKernel
          (X := X) (Nstage j) (nstage j))
    (hgraph_word_projection :
      ∀ j : J, ∀ w : FreeGroup X, w ∈ Nstage j →
        π j (freeProCZCCompletedFoxSemidirectGraphWordPoint (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))

Finite-stage semidirect exactness places every completed boundary cycle in the closed generated Fox graph target without assuming that finite relation words are actual kernel words.

Show Lean proof
Theorem FoxDifferential.freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_finiteStage_semi_exact 
theorem freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_finiteStage_semi_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_exact :
      ∀ j : J,
        foxAlgebraicStageBoundaryCyclesCoveredBySourceKernel
          (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))

The finite-stage semidirect exactness route also places every completed boundary cycle in the closed generated Fox graph target.

Show Lean proof