NYLL
Module

KernelIdeal.lean

Nyll.ProCGroups.FoxDifferential.Completed.FiniteStage.Stage.KernelIdeal
2 declarations indexed from sourceView source ↗

Module documentation

Fox differential: completed — finite stage — stage — kernel ideal

The principal declarations in this module are:

  • foxAlgebraicStageSourceGeneratorSubOne_mem_sourceAugmentationIdeal

The finite-stage source generator \([x_i]-1\) belongs to the source augmentation ideal.

  • foxAlgebraicStageGroupAlgebraMapKernel_mem_mulAugmentation_of_derivatives_eq_zero

Finite-stage Fox kernel input: the target derivative equations place the source coefficients in K_j, while the source generator boundaries lie in I_j.

Imports1
Imported by1

Declarations

theorem

foxAlgebraicStageSourceGeneratorSubOne_mem_sourceAugmentationIdeal

L40 ↗
FoxDifferential.foxAlgebraicStageSourceGeneratorSubOne_mem_sourceAugmentationIdeal
Documentation

The finite-stage source generator \([x_i]-1\) belongs to the source augmentation ideal.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
omit [DecidableEq X] [N.Normal] in
Lean source · statement
theorem foxAlgebraicStageSourceGeneratorSubOne_mem_sourceAugmentationIdeal
    (i : X) :
    MonoidAlgebra.of (ModNCompletedCoeff n)
        (FreeGroup X ⧸ foxCommutatorPowerSubgroup (F := FreeGroup X) N n)
        (QuotientGroup.mk'
          (foxCommutatorPowerSubgroup (F := FreeGroup X) N n)
          (FreeGroup.of i)) - 1 ∈
      foxAlgebraicStageSourceAugmentationIdeal (X := X) N n
theorem

foxAlgebraicStageGroupAlgebraMapKernel_mem_mulAugmentation_of_derivatives_eq_zero

L57 ↗
FoxDifferential.foxAlgebraicStageGroupAlgebraMapKernel_mem_mulAugmentation_of_derivatives_eq_zero
Documentation

Finite-stage Fox kernel input: the target derivative equations place the source coefficients in K_j, while the source generator boundaries lie in I_j.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u v
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
Lean source · statement
theorem foxAlgebraicStageGroupAlgebraMapKernel_mem_mulAugmentation_of_derivatives_eq_zero
    [Finite X]
    {x : foxAlgebraicStageSourceGroupAlgebra (X := X) N n}
    (hderivative :
      ∀ i : X, foxAlgebraicStageGroupAlgebraDerivative (X := X) N n i x = 0)
    (haugmentation :
      foxCommutatorPowerSourceGroupAlgebraAugmentation
        (F := FreeGroup X) N n x = 0) :
    x ∈ foxAlgebraicStageGroupAlgebraMapKernelMulAugmentationIdeal (X := X) N n

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