Module

SourceCycleReduction.lean

Nyll.ProCGroups.FoxDifferential.Completed.FiniteStage.SourceCycleReduction

9 declarations indexed from sourceView source ↗

Module documentation

Fox differential: completed — finite stage — source cycle reduction

The principal declarations in this module are:

foxAlgebraicStageSourceBoundaryCycleSubmodule

Source boundary cycles in the source coordinate module.

foxAlgebraicStageSourceCycleProjectionExact

Source-cycle projection exactness: every source Fox cycle maps to the target relation-boundary submodule. This is the source-quotient analogue of exactness before the relation-ideal correction.

mem_foxAlgebraicStageSourceBoundaryCycleSubmodule

Membership in the finite-stage boundary-cycle object is characterized by the corresponding boundary-vanishing condition.

foxAlgebraicStageSourceBoundaryLeftRelationReduction_of_sourceCycleProjectionExact

Source-cycle projection exactness implies the reduction for the left relation-augmentation submodule, because elements of the left relation-augmentation submodule have explicit relation-compatible primitives.

Imports1

Nyll.ProCGroups.FoxDifferential.Completed.FiniteStage.RelationIdealPrimitive

Imported by1

Nyll.ProCGroups.FoxDifferential.Completed.FiniteStage.All

def

foxAlgebraicStageSourceBoundaryCycleSubmodule

L41 ↗

FoxDifferential.foxAlgebraicStageSourceBoundaryCycleSubmodule

Documentation

Source boundary cycles in the source coordinate module.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

Lean source · statement

def foxAlgebraicStageSourceBoundaryCycleSubmodule [Fintype X] :
    Submodule (foxAlgebraicStageSourceGroupAlgebra (X := X) N n)
      (foxAlgebraicStageSourceCoordinateVector (X := X) N n)

theorem

mem_foxAlgebraicStageSourceBoundaryCycleSubmodule

L52 ↗

FoxDifferential.mem_foxAlgebraicStageSourceBoundaryCycleSubmodule

Documentation

Membership in the finite-stage boundary-cycle object is characterized by the corresponding boundary-vanishing condition.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
omit [DecidableEq X] [N.Normal] in

Lean source · statement

theorem mem_foxAlgebraicStageSourceBoundaryCycleSubmodule
    (N : Subgroup (FreeGroup X)) (n : ℕ) [Fintype X]
    {p : foxAlgebraicStageSourceCoordinateVector (X := X) N n} :
    p ∈ foxAlgebraicStageSourceBoundaryCycleSubmodule (X := X) N n ↔
      foxAlgebraicStageSourceFoxBoundary (X := X) N n p = 0

def

foxAlgebraicStageSourceCycleProjectionExact

L64 ↗

FoxDifferential.foxAlgebraicStageSourceCycleProjectionExact

Documentation

Source-cycle projection exactness: every source Fox cycle maps to the target relation-boundary submodule. This is the source-quotient analogue of exactness before the relation-ideal correction.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

Lean source · statement

def foxAlgebraicStageSourceCycleProjectionExact [Fintype X] : Prop

def

foxAlgebraicStageSourceBoundaryLeftRelationReduction

L71 ↗

FoxDifferential.foxAlgebraicStageSourceBoundaryLeftRelationReduction

Documentation

Left-submodule version of the source-boundary reduction.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

Lean source · statement

def foxAlgebraicStageSourceBoundaryLeftRelationReduction [Fintype X] : Prop

theorem

foxAlgebraicStageSourceBoundaryLeftRelationReduction_of_sourceCycleProjectionExact

L83 ↗

FoxDifferential.foxAlgebraicStageSourceBoundaryLeftRelationReduction_of_sourceCycleProjectionExact

Documentation

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

Lean source · statement

theorem foxAlgebraicStageSourceBoundaryLeftRelationReduction_of_sourceCycleProjectionExact
    [Fintype X]
    (hcycle : foxAlgebraicStageSourceCycleProjectionExact (X := X) N n) :
    foxAlgebraicStageSourceBoundaryLeftRelationReduction (X := X) N n

theorem

foxAlgebraicStageSourceBoundaryRelationIdealReduction_of_relationIdeal_le_leftSubmodule

L118 ↗

FoxDifferential.foxAlgebraicStageSourceBoundaryRelationIdealReduction_of_relationIdeal_le_leftSubmodule

Documentation

If the two-sided relation augmentation ideal is already generated by the same relation augmentation elements as a left source-submodule, source-cycle projection exactness implies the source-boundary relation-ideal reduction used in the finite-stage exactness file.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

Lean source · statement

theorem foxAlgebraicStageSourceBoundaryRelationIdealReduction_of_relationIdeal_le_leftSubmodule
    [Fintype X]
    (hideal_left :
      ∀ x : foxAlgebraicStageSourceGroupAlgebra (X := X) N n,
        x ∈ foxAlgebraicStageRelationAugmentationIdeal (X := X) N n →
          x ∈ foxAlgebraicStageRelationAugmentationLeftSubmodule (X := X) N n)
    (hcycle : foxAlgebraicStageSourceCycleProjectionExact (X := X) N n) :
    foxAlgebraicStageSourceBoundaryRelationIdealReduction (X := X) N n

theorem

foxAlgebraicStageRelationBoundaryModuleExact_of_relIdealLeftGen_and_sourceCycleProjExact

L131 ↗

FoxDifferential.foxAlgebraicStageRelationBoundaryModuleExact_of_relIdealLeftGen_and_sourceCycleProjExact

Documentation

Finite-stage source-cycle projection exactness gives relation-boundary module exactness.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

Lean source · statement

theorem foxAlgebraicStageRelationBoundaryModuleExact_of_relIdealLeftGen_and_sourceCycleProjExact
    [Fintype X]
    (hideal_left :
      ∀ x : foxAlgebraicStageSourceGroupAlgebra (X := X) N n,
        x ∈ foxAlgebraicStageRelationAugmentationIdeal (X := X) N n →
          x ∈ foxAlgebraicStageRelationAugmentationLeftSubmodule (X := X) N n)
    (hcycle : foxAlgebraicStageSourceCycleProjectionExact (X := X) N n) :
    foxAlgebraicStageRelationBoundaryModuleExact (X := X) N n

theorem

foxAlgebraicStageBoundaryCyclesCovered_of_relIdealLeftGen_and_sourceCycleProjExact

L145 ↗

FoxDifferential.foxAlgebraicStageBoundaryCyclesCovered_of_relIdealLeftGen_and_sourceCycleProjExact

Documentation

The same inputs give finite coordinate coverage.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

Lean source · statement

theorem foxAlgebraicStageBoundaryCyclesCovered_of_relIdealLeftGen_and_sourceCycleProjExact
    [Fintype X]
    (hideal_left :
      ∀ x : foxAlgebraicStageSourceGroupAlgebra (X := X) N n,
        x ∈ foxAlgebraicStageRelationAugmentationIdeal (X := X) N n →
          x ∈ foxAlgebraicStageRelationAugmentationLeftSubmodule (X := X) N n)
    (hcycle : foxAlgebraicStageSourceCycleProjectionExact (X := X) N n) :
    foxAlgebraicStageBoundaryCyclesCoveredBySourceKernel (X := X) N n

theorem

foxAlgebraicStageSemiBoundaryCyclesCovered_of_relIdealLeftGen_and_sourceCycleProjExact

L162 ↗

FoxDifferential.foxAlgebraicStageSemiBoundaryCyclesCovered_of_relIdealLeftGen_and_sourceCycleProjExact

Documentation

Relation-ideal left generation together with exactness of the source-cycle projection covers the finite semidirect boundary cycles.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

Lean source · statement

theorem foxAlgebraicStageSemiBoundaryCyclesCovered_of_relIdealLeftGen_and_sourceCycleProjExact
    [Fintype X]
    (hideal_left :
      ∀ x : foxAlgebraicStageSourceGroupAlgebra (X := X) N n,
        x ∈ foxAlgebraicStageRelationAugmentationIdeal (X := X) N n →
          x ∈ foxAlgebraicStageRelationAugmentationLeftSubmodule (X := X) N n)
    (hcycle : foxAlgebraicStageSourceCycleProjectionExact (X := X) N n) :
    foxAlgebraicStageSemidirectBoundaryCyclesCoveredBySourceKernel (X := X) N n

Module documentation

Fox differential: completed — finite stage — source cycle reduction

Declarations