NYLL
Module

RelationReflection.lean

Nyll.ProCGroups.FoxDifferential.Completed.FreeProC.RelationReflection
18 declarations indexed from sourceView source ↗

Module documentation

Relation reflection for free pro-\(C\) presentations

This module supplies the finite free-basis family used to reflect completed Fox relations through finite quotient stages, and relates stagewise vanishing to equality in the completed differential module.

Imports4
Imported by3

Declarations

abbrev

freeProCReflectionFamily

L39 ↗
CrowellExactSequence.freeProCReflectionFamily
Documentation

The universe-lifted finite free basis supplies the relation-reflection family.

Source context 12 commands

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

namespace CrowellExactSequence
noncomputable section
open scoped Topology
open ProCGroups.InverseSystems
open ProCGroups.ProC
open FoxDifferential
universe u v
section FreeRelationReflection
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {H : Type u}
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [T2Space H]
Lean source · statement
abbrev freeProCReflectionFamily
    (sourceData :
      ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
    {r : Nat}
    (hbasis : Cardinal.mk sourceData.basis = r) : ULift.{u} (Fin r) → sourceData.carrier
theorem

freeProCReflectionFamily_target_generates

L48 ↗
CrowellExactSequence.freeProCReflectionFamily_target_generates
Documentation

The target images of the chosen basis topologically generate a surjective target.

Source context 13 commands

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

namespace CrowellExactSequence
noncomputable section
open scoped Topology
open ProCGroups.InverseSystems
open ProCGroups.ProC
open FoxDifferential
universe u v
section FreeRelationReflection
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {H : Type u}
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [T2Space H]
omit [T2Space H] in
Lean source · full declaration
theorem freeProCReflectionFamily_target_generates
    (sourceData :
      ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
    {r : Nat}
    (hbasis : Cardinal.mk sourceData.basis = r)
    (psi : ContinuousMonoidHom sourceData.carrier H)
    (hpsi : Function.Surjective psi) :
    ProCGroups.Generation.TopologicallyGenerates
      (G := H)
      (Set.range (fun i : ULift.{u} (Fin r) =>
        psi (freeProCReflectionFamily (C := C) sourceData hbasis i))) := by
  simpa [freeProCReflectionFamily] using
    freeProCChosenULiftFamilyOfBasisCard_image_generates_of_surjective
      (C := C) sourceData hbasis psi hpsi
def

freeProCRelationReflectionStageSourceHom

L64 ↗
CrowellExactSequence.freeProCRelationReflectionStageSourceHom
Documentation

The free-group map onto the source quotient used by a differential-module finite stage.

Source context 12 commands

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

namespace CrowellExactSequence
noncomputable section
open scoped Topology
open ProCGroups.InverseSystems
open ProCGroups.ProC
open FoxDifferential
universe u v
section FreeRelationReflection
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {H : Type u}
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [T2Space H]
Lean source · statement
def freeProCRelationReflectionStageSourceHom
    (sourceData :
      ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
    {r : Nat}
    (hbasis : Cardinal.mk sourceData.basis = r)
    (psi : ContinuousMonoidHom sourceData.carrier H)
    (i : ZCCompletedDifferentialModuleIndex
      C psi.toMonoidHom) :
    FreeGroup (ULift.{u} (Fin r)) →*
      zcCompletedDifferentialModuleStageSource
        C psi.toMonoidHom i
def

freeProCRelationReflectionStageKernel

L83 ↗
CrowellExactSequence.freeProCRelationReflectionStageKernel
Documentation

The source kernel used by a differential-module stage, pulled back to the abstract free group on the chosen basis.

Source context 12 commands

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

namespace CrowellExactSequence
noncomputable section
open scoped Topology
open ProCGroups.InverseSystems
open ProCGroups.ProC
open FoxDifferential
universe u v
section FreeRelationReflection
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {H : Type u}
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [T2Space H]
Lean source · statement
def freeProCRelationReflectionStageKernel
    (sourceData :
      ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
    {r : Nat}
    (hbasis : Cardinal.mk sourceData.basis = r)
    (psi : ContinuousMonoidHom sourceData.carrier H)
    (i : ZCCompletedDifferentialModuleIndex
      C psi.toMonoidHom) :
    Subgroup (FreeGroup (ULift.{u} (Fin r)))
instance

freeProCRelationReflectionStageKernel_normal

L99 ↗
CrowellExactSequence.freeProCRelationReflectionStageKernel_normal
Documentation

The relation-reflection stage kernel is a normal subgroup of the free group on the lifted finite basis.

Source context 12 commands

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

namespace CrowellExactSequence
noncomputable section
open scoped Topology
open ProCGroups.InverseSystems
open ProCGroups.ProC
open FoxDifferential
universe u v
section FreeRelationReflection
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {H : Type u}
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [T2Space H]
Lean source · statement
instance freeProCRelationReflectionStageKernel_normal
    (sourceData :
      ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
    {r : Nat}
    (hbasis : Cardinal.mk sourceData.basis = r)
    (psi : ContinuousMonoidHom sourceData.carrier H)
    (i : ZCCompletedDifferentialModuleIndex
      C psi.toMonoidHom) :
    (freeProCRelationReflectionStageKernel (C := C) sourceData hbasis psi i).Normal
theorem

freeProCRelationReflectionStageSourceHom_surjective

L113 ↗
CrowellExactSequence.freeProCRelationReflectionStageSourceHom_surjective
Documentation

The chosen free basis surjects onto every finite source quotient stage.

Source context 13 commands

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

namespace CrowellExactSequence
noncomputable section
open scoped Topology
open ProCGroups.InverseSystems
open ProCGroups.ProC
open FoxDifferential
universe u v
section FreeRelationReflection
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {H : Type u}
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [T2Space H]
omit [IsTopologicalGroup H] [T2Space H] in
Lean source · statement
theorem freeProCRelationReflectionStageSourceHom_surjective
    (sourceData :
      ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
    {r : Nat}
    (hbasis : Cardinal.mk sourceData.basis = r)
    (psi : ContinuousMonoidHom sourceData.carrier H)
    (i : ZCCompletedDifferentialModuleIndex
      C psi.toMonoidHom) :
    Function.Surjective
      (freeProCRelationReflectionStageSourceHom (C := C) sourceData hbasis psi i)
def

freeProCRelationReflectionStageSourceEquiv

L179 ↗
CrowellExactSequence.freeProCRelationReflectionStageSourceEquiv
Documentation

Identification of the source quotient stage with the corresponding free-group quotient.

Source context 12 commands

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

namespace CrowellExactSequence
noncomputable section
open scoped Topology
open ProCGroups.InverseSystems
open ProCGroups.ProC
open FoxDifferential
universe u v
section FreeRelationReflection
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {H : Type u}
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [T2Space H]
Lean source · statement
def freeProCRelationReflectionStageSourceEquiv
    (sourceData :
      ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
    {r : Nat}
    (hbasis : Cardinal.mk sourceData.basis = r)
    (psi : ContinuousMonoidHom sourceData.carrier H)
    (i : ZCCompletedDifferentialModuleIndex
      C psi.toMonoidHom) :
    foxAlgebraicStageTargetQuotient
        (X := ULift.{u} (Fin r))
        (freeProCRelationReflectionStageKernel (C := C) sourceData hbasis psi i) ≃*
      zcCompletedDifferentialModuleStageSource
        C psi.toMonoidHom i
theorem

freeProCRelationReflectionStageSourceEquiv_mk

L203 ↗
CrowellExactSequence.freeProCRelationReflectionStageSourceEquiv_mk
Documentation

The relation-reflection source-stage equivalence sends the quotient class of a free word to its image under the corresponding source-stage homomorphism.

Source context 13 commands

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

namespace CrowellExactSequence
noncomputable section
open scoped Topology
open ProCGroups.InverseSystems
open ProCGroups.ProC
open FoxDifferential
universe u v
section FreeRelationReflection
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {H : Type u}
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [T2Space H]
omit [IsTopologicalGroup H] [T2Space H] in
Lean source · statement
theorem freeProCRelationReflectionStageSourceEquiv_mk
    (sourceData :
      ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
    {r : Nat}
    (hbasis : Cardinal.mk sourceData.basis = r)
    (psi : ContinuousMonoidHom sourceData.carrier H)
    (i : ZCCompletedDifferentialModuleIndex
      C psi.toMonoidHom)
    (w : FreeGroup (ULift.{u} (Fin r))) :
    freeProCRelationReflectionStageSourceEquiv (C := C) sourceData hbasis psi i
        (QuotientGroup.mk'
          (freeProCRelationReflectionStageKernel (C := C) sourceData hbasis psi i) w) =
      freeProCRelationReflectionStageSourceHom (C := C) sourceData hbasis psi i w
abbrev

freeProCRelationReflectionTargetStageKernel

L222 ↗
CrowellExactSequence.freeProCRelationReflectionTargetStageKernel
Documentation

The target finite Fox relation kernel attached to the target quotient of a \(\mathbb{Z}_C\)-completed differential-module index.

Source context 12 commands

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

namespace CrowellExactSequence
noncomputable section
open scoped Topology
open ProCGroups.InverseSystems
open ProCGroups.ProC
open FoxDifferential
universe u v
section FreeRelationReflection
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {H : Type u}
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [T2Space H]
Lean source · statement
abbrev freeProCRelationReflectionTargetStageKernel
    (sourceData :
      ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
    {r : Nat}
    (hbasis : Cardinal.mk sourceData.basis = r)
    (psi : ContinuousMonoidHom sourceData.carrier H)
    (i : ZCCompletedDifferentialModuleIndex
      C psi.toMonoidHom) :
    Subgroup (FreeGroup (ULift.{u} (Fin r)))
instance

freeProCRelationReflectionTargetStageKernel_normal

L238 ↗
CrowellExactSequence.freeProCRelationReflectionTargetStageKernel_normal
Documentation

The target finite Fox relation kernel is normal.

Source context 12 commands

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

namespace CrowellExactSequence
noncomputable section
open scoped Topology
open ProCGroups.InverseSystems
open ProCGroups.ProC
open FoxDifferential
universe u v
section FreeRelationReflection
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {H : Type u}
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [T2Space H]
Lean source · statement
instance freeProCRelationReflectionTargetStageKernel_normal
    (sourceData :
      ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
    {r : Nat}
    (hbasis : Cardinal.mk sourceData.basis = r)
    (psi : ContinuousMonoidHom sourceData.carrier H)
    (i : ZCCompletedDifferentialModuleIndex
      C psi.toMonoidHom) :
    (freeProCRelationReflectionTargetStageKernel (C := C) sourceData hbasis psi i).Normal
theorem

freeProCRelationReflectionTargetStageKernel_antitone

L251 ↗
CrowellExactSequence.freeProCRelationReflectionTargetStageKernel_antitone
Documentation

Target finite Fox kernels are antitone along differential-module stage refinement.

Source context 13 commands

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

namespace CrowellExactSequence
noncomputable section
open scoped Topology
open ProCGroups.InverseSystems
open ProCGroups.ProC
open FoxDifferential
universe u v
section FreeRelationReflection
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {H : Type u}
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [T2Space H]
omit [T2Space H] in
Lean source · statement
theorem freeProCRelationReflectionTargetStageKernel_antitone
    (sourceData :
      ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
    {r : Nat}
    (hbasis : Cardinal.mk sourceData.basis = r)
    (psi : ContinuousMonoidHom sourceData.carrier H)
    {i j : ZCCompletedDifferentialModuleIndex
      C psi.toMonoidHom} (hij : i ≤ j) :
    freeProCRelationReflectionTargetStageKernel (C := C) sourceData hbasis psi j ≤
      freeProCRelationReflectionTargetStageKernel (C := C) sourceData hbasis psi i
def

freeProCRelationReflectionTargetStageQMap

L268 ↗
CrowellExactSequence.freeProCRelationReflectionTargetStageQMap
Documentation

The canonical target quotient comparison map \(H/U_i \to F_X/N_i\).

Source context 12 commands

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

namespace CrowellExactSequence
noncomputable section
open scoped Topology
open ProCGroups.InverseSystems
open ProCGroups.ProC
open FoxDifferential
universe u v
section FreeRelationReflection
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {H : Type u}
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [T2Space H]
Lean source · statement
def freeProCRelationReflectionTargetStageQMap
    (sourceData :
      ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
    {r : Nat}
    (hbasis : Cardinal.mk sourceData.basis = r)
    (psi : ContinuousMonoidHom sourceData.carrier H)
    (hpsi : Function.Surjective psi)
    (i : ZCCompletedDifferentialModuleIndex
      C psi.toMonoidHom) :
    CompletedGroupAlgebraQuotientInClass H C i.target.2 →*
      foxAlgebraicStageTargetQuotient
        (X := ULift.{u} (Fin r))
        (freeProCRelationReflectionTargetStageKernel (C := C) sourceData hbasis psi i)
theorem

freeProCRelationReflectionTargetStageQMap_generator

L303 ↗
CrowellExactSequence.freeProCRelationReflectionTargetStageQMap_generator
Documentation

The generator formula for the free pro-\(C\) relation-reflection target finite-stage quotient map identifies the specified Crowell boundary or coordinate map.

Source context 13 commands

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

namespace CrowellExactSequence
noncomputable section
open scoped Topology
open ProCGroups.InverseSystems
open ProCGroups.ProC
open FoxDifferential
universe u v
section FreeRelationReflection
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {H : Type u}
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [T2Space H]
omit [T2Space H] in
Lean source · statement
theorem freeProCRelationReflectionTargetStageQMap_generator
    (sourceData :
      ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
    {r : Nat}
    (hbasis : Cardinal.mk sourceData.basis = r)
    (psi : ContinuousMonoidHom sourceData.carrier H)
    (hpsi : Function.Surjective psi)
    (i : ZCCompletedDifferentialModuleIndex
      C psi.toMonoidHom)
    (x : ULift.{u} (Fin r)) :
    freeProCRelationReflectionTargetStageQMap (C := C) sourceData hbasis psi hpsi i
        (QuotientGroup.mk
          (psi (freeProCReflectionFamily (C := C) sourceData hbasis x))) =
      QuotientGroup.mk'
        (freeProCRelationReflectionTargetStageKernel (C := C) sourceData hbasis psi i)
        (FreeGroup.of x)
theorem

freeProCRelationReflectionTargetStageQMap_transition

L334 ↗
CrowellExactSequence.freeProCRelationReflectionTargetStageQMap_transition
Documentation

Target quotient comparison maps commute with differential-module stage refinement.

Source context 13 commands

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

namespace CrowellExactSequence
noncomputable section
open scoped Topology
open ProCGroups.InverseSystems
open ProCGroups.ProC
open FoxDifferential
universe u v
section FreeRelationReflection
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {H : Type u}
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [T2Space H]
omit [T2Space H] in
Lean source · statement
theorem freeProCRelationReflectionTargetStageQMap_transition
    (sourceData :
      ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
    {r : Nat}
    (hbasis : Cardinal.mk sourceData.basis = r)
    (psi : ContinuousMonoidHom sourceData.carrier H)
    (hpsi : Function.Surjective psi)
    {i j : ZCCompletedDifferentialModuleIndex
      C psi.toMonoidHom} (hij : i ≤ j)
    (q : CompletedGroupAlgebraQuotientInClass H C j.target.2) :
    freeProCRelationReflectionTargetStageQMap (C := C) sourceData hbasis psi hpsi i
        ((OpenNormalSubgroupInClass.map
          (C := C) (G := H)
          (U := OrderDual.ofDual i.target.2)
          (V := OrderDual.ofDual j.target.2) hij.2.2) q) =
      foxAlgebraicStageTargetQuotientMap
        (X := ULift.{u} (Fin r))
        (freeProCRelationReflectionTargetStageKernel_antitone
          (C := C) sourceData hbasis psi hij)
        (freeProCRelationReflectionTargetStageQMap
          (C := C) sourceData hbasis psi hpsi j q)
def

freeProCRelationReflectionTargetStageRight

L381 ↗
CrowellExactSequence.freeProCRelationReflectionTargetStageRight
Documentation

The target component map used by finite Fox semidirect stages.

Source context 12 commands

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

namespace CrowellExactSequence
noncomputable section
open scoped Topology
open ProCGroups.InverseSystems
open ProCGroups.ProC
open FoxDifferential
universe u v
section FreeRelationReflection
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {H : Type u}
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [T2Space H]
Lean source · statement
def freeProCRelationReflectionTargetStageRight
    (sourceData :
      ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
    {r : Nat}
    (hbasis : Cardinal.mk sourceData.basis = r)
    (psi : ContinuousMonoidHom sourceData.carrier H)
    (hpsi : Function.Surjective psi)
    (i : ZCCompletedDifferentialModuleIndex
      C psi.toMonoidHom) :
    H →* foxAlgebraicStageTargetQuotient
        (X := ULift.{u} (Fin r))
        (freeProCRelationReflectionTargetStageKernel (C := C) sourceData hbasis psi i)
theorem

freeProCRelationReflectionTargetStageRight_generator

L404 ↗
CrowellExactSequence.freeProCRelationReflectionTargetStageRight_generator
Documentation

The target-stage right map sends the chosen generator to its quotient class in the relation-reflection target stage.

Source context 13 commands

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

namespace CrowellExactSequence
noncomputable section
open scoped Topology
open ProCGroups.InverseSystems
open ProCGroups.ProC
open FoxDifferential
universe u v
section FreeRelationReflection
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {H : Type u}
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [T2Space H]
omit [T2Space H] in
Lean source · statement
theorem freeProCRelationReflectionTargetStageRight_generator
    (sourceData :
      ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
    {r : Nat}
    (hbasis : Cardinal.mk sourceData.basis = r)
    (psi : ContinuousMonoidHom sourceData.carrier H)
    (hpsi : Function.Surjective psi)
    (i : ZCCompletedDifferentialModuleIndex
      C psi.toMonoidHom)
    (x : ULift.{u} (Fin r)) :
    freeProCRelationReflectionTargetStageRight (C := C) sourceData hbasis psi hpsi i
        (psi (freeProCReflectionFamily (C := C) sourceData hbasis x)) =
      QuotientGroup.mk'
        (freeProCRelationReflectionTargetStageKernel (C := C) sourceData hbasis psi i)
        (FreeGroup.of x)
def

freeProCRelationReflectionTargetStageMap

L431 ↗
CrowellExactSequence.freeProCRelationReflectionTargetStageMap
Documentation

The finite Fox semidirect projection attached to one target quotient stage.

Source context 12 commands

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

namespace CrowellExactSequence
noncomputable section
open scoped Topology
open ProCGroups.InverseSystems
open ProCGroups.ProC
open FoxDifferential
universe u v
section FreeRelationReflection
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {H : Type u}
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [T2Space H]
Lean source · statement
def freeProCRelationReflectionTargetStageMap
    (sourceData :
      ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
    {r : Nat}
    (hbasis : Cardinal.mk sourceData.basis = r)
    (psi : ContinuousMonoidHom sourceData.carrier H)
    (hpsi : Function.Surjective psi)
    (i : ZCCompletedDifferentialModuleIndex
      C psi.toMonoidHom) :
    ZCCompletedFoxSemidirect C (ULift.{u} (Fin r)) H →*
      FoxAlgebraicStageSemidirect
        (X := ULift.{u} (Fin r))
        (freeProCRelationReflectionTargetStageKernel (C := C) sourceData hbasis psi i)
        i.target.1.modulus
theorem

freeProCRelationReflection_finiteStage_relationBoundaryModuleExact

L467 ↗
CrowellExactSequence.freeProCRelationReflection_finiteStage_relationBoundaryModuleExact
Documentation

Each target finite stage attached to the chosen free pro-\(C\) basis satisfies the finite Fox relation-boundary module exactness needed by the approximation theorem.

Source context 13 commands

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

namespace CrowellExactSequence
noncomputable section
open scoped Topology
open ProCGroups.InverseSystems
open ProCGroups.ProC
open FoxDifferential
universe u v
section FreeRelationReflection
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable {H : Type u}
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [T2Space H]
omit [T2Space H] in
Lean source · statement
theorem freeProCRelationReflection_finiteStage_relationBoundaryModuleExact
    (sourceData :
      ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
    {r : Nat}
    (hbasis : Cardinal.mk sourceData.basis = r)
    (psi : ContinuousMonoidHom sourceData.carrier H)
    (i : ZCCompletedDifferentialModuleIndex
      C psi.toMonoidHom) :
    foxAlgebraicStageRelationBoundaryModuleExact
      (X := ULift.{u} (Fin r))
      (freeProCRelationReflectionTargetStageKernel (C := C) sourceData hbasis psi i)
      i.target.1.modulus

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