NYLL
Module

Target.lean

Nyll.ProCGroups.FoxDifferential.Completed.FiniteStage.CoeffMap.Target
8 declarations indexed from sourceView source ↗

Module documentation

Fox differential: completed — finite stage — coeff map — target

The principal declarations in this module are:

  • foxAlgebraicStageTargetGroupAlgebraCoeffMap

Coefficient-reduction map on finite-stage target group algebras for a divisor \(n \mid m\).

  • foxAlgebraicStageTargetGroupAlgebraCoeffMap_of

Evaluation of target coefficient reduction on a represented quotient word.

  • foxAlgebraicStageTargetGroupAlgebraCoeffMap_of_quotient

Evaluation of target coefficient reduction on a quotient basis element.

  • foxAlgebraicStageTargetGroupAlgebraCoeffMap_single_apply

The finite-stage target coefficient map sends a singleton to the singleton with reduced coefficient and unchanged support.

Imports1
Imported by3

Declarations

def

foxAlgebraicStageTargetGroupAlgebraCoeffMap

L45 ↗
FoxDifferential.foxAlgebraicStageTargetGroupAlgebraCoeffMap
Documentation

Coefficient-reduction map on finite-stage target group algebras for a divisor \(n \mid m\).

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 : ℕ)
variable {n₀ m₀ : ℕ} [Fact (0 < n₀)] [Fact (0 < m₀)]
Lean source · statement
def foxAlgebraicStageTargetGroupAlgebraCoeffMap
    (N : Subgroup (FreeGroup X)) [N.Normal] (hnm : n₀ ∣ m₀) :
    foxAlgebraicStageTargetGroupAlgebra (X := X) N m₀ →+*
      foxAlgebraicStageTargetGroupAlgebra (X := X) N n₀
theorem

foxAlgebraicStageTargetGroupAlgebraCoeffMap_of

L55 ↗
FoxDifferential.foxAlgebraicStageTargetGroupAlgebraCoeffMap_of
Documentation

Evaluation of target coefficient reduction on a represented quotient word.

Source context 12 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 : ℕ)
variable {n₀ m₀ : ℕ} [Fact (0 < n₀)] [Fact (0 < m₀)]
omit [DecidableEq X] [Fact (0 < n₀)] [Fact (0 < m₀)] in
Lean source · statement
theorem foxAlgebraicStageTargetGroupAlgebraCoeffMap_of
    (N : Subgroup (FreeGroup X)) [N.Normal] (hnm : n₀ ∣ m₀) (w : FreeGroup X) :
    foxAlgebraicStageTargetGroupAlgebraCoeffMap (X := X) N hnm
        (MonoidAlgebra.of (ModNCompletedCoeff m₀)
          (foxAlgebraicStageTargetQuotient (X := X) N) (QuotientGroup.mk' N w)) =
      MonoidAlgebra.of (ModNCompletedCoeff n₀)
        (foxAlgebraicStageTargetQuotient (X := X) N) (QuotientGroup.mk' N w)
theorem

foxAlgebraicStageTargetGroupAlgebraCoeffMap_of_quotient

L70 ↗
FoxDifferential.foxAlgebraicStageTargetGroupAlgebraCoeffMap_of_quotient
Documentation

Evaluation of target coefficient reduction on a quotient basis element.

Source context 12 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 : ℕ)
variable {n₀ m₀ : ℕ} [Fact (0 < n₀)] [Fact (0 < m₀)]
omit [DecidableEq X] [Fact (0 < n₀)] [Fact (0 < m₀)] in
Lean source · statement
theorem foxAlgebraicStageTargetGroupAlgebraCoeffMap_of_quotient
    (N : Subgroup (FreeGroup X)) [N.Normal] (hnm : n₀ ∣ m₀)
    (q : foxAlgebraicStageTargetQuotient (X := X) N) :
    foxAlgebraicStageTargetGroupAlgebraCoeffMap (X := X) N hnm
        (MonoidAlgebra.of (ModNCompletedCoeff m₀)
          (foxAlgebraicStageTargetQuotient (X := X) N) q) =
      MonoidAlgebra.of (ModNCompletedCoeff n₀)
        (foxAlgebraicStageTargetQuotient (X := X) N) q
theorem

foxAlgebraicStageTargetGroupAlgebraCoeffMap_single_apply

L87 ↗
FoxDifferential.foxAlgebraicStageTargetGroupAlgebraCoeffMap_single_apply
Documentation

The finite-stage target coefficient map sends a singleton to the singleton with reduced coefficient and unchanged support.

Source context 12 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 : ℕ)
variable {n₀ m₀ : ℕ} [Fact (0 < n₀)] [Fact (0 < m₀)]
omit [DecidableEq X] [Fact (0 < n₀)] [Fact (0 < m₀)] in
Lean source · statement
theorem foxAlgebraicStageTargetGroupAlgebraCoeffMap_single_apply
    (N : Subgroup (FreeGroup X)) [N.Normal] (hnm : n₀ ∣ m₀)
    (q : foxAlgebraicStageTargetQuotient (X := X) N)
    (a : ModNCompletedCoeff m₀) :
    foxAlgebraicStageTargetGroupAlgebraCoeffMap (X := X) N hnm
        (MonoidAlgebra.single q a) =
      MonoidAlgebra.single q (modNCompletedCoeffMap (n := n₀) (m := m₀) hnm a)
theorem

foxAlgebraicStageTargetGroupAlgebraCoeffMap_eq_mapRange

L121 ↗
FoxDifferential.foxAlgebraicStageTargetGroupAlgebraCoeffMap_eq_mapRange
Documentation

Target coefficient reduction is the native monoid-algebra coefficient map.

Source context 12 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 : ℕ)
variable {n₀ m₀ : ℕ} [Fact (0 < n₀)] [Fact (0 < m₀)]
omit [DecidableEq X] [Fact (0 < n₀)] [Fact (0 < m₀)] in
Lean source · statement
theorem foxAlgebraicStageTargetGroupAlgebraCoeffMap_eq_mapRange
    (N : Subgroup (FreeGroup X)) [N.Normal] (hnm : n₀ ∣ m₀) :
    foxAlgebraicStageTargetGroupAlgebraCoeffMap (X := X) N hnm =
      MonoidAlgebra.mapRingHom
        (foxAlgebraicStageTargetQuotient (X := X) N)
        (modNCompletedCoeffMap (n := n₀) (m := m₀) hnm)
theorem

foxAlgebraicStageTargetGroupAlgebraCoeffMap_apply

L152 ↗
FoxDifferential.foxAlgebraicStageTargetGroupAlgebraCoeffMap_apply
Documentation

The finite-stage target coefficient map changes each coefficient while retaining its target-quotient support.

Source context 12 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 : ℕ)
variable {n₀ m₀ : ℕ} [Fact (0 < n₀)] [Fact (0 < m₀)]
omit [DecidableEq X] [Fact (0 < n₀)] [Fact (0 < m₀)] in
Lean source · statement
theorem foxAlgebraicStageTargetGroupAlgebraCoeffMap_apply
    (N : Subgroup (FreeGroup X)) [N.Normal] (hnm : n₀ ∣ m₀)
    (x : foxAlgebraicStageTargetGroupAlgebra (X := X) N m₀)
    (q : foxAlgebraicStageTargetQuotient (X := X) N) :
    (foxAlgebraicStageTargetGroupAlgebraCoeffMap (X := X) N hnm x).coeff q =
      modNCompletedCoeffMap (n := n₀) (m := m₀) hnm (x.coeff q)
theorem

foxAlgebraicStageTargetGroupAlgebraCoeffMap_rfl

L165 ↗
FoxDifferential.foxAlgebraicStageTargetGroupAlgebraCoeffMap_rfl
Documentation

Target coefficient reduction is the identity map when the modulus is unchanged.

Source context 12 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 : ℕ)
variable {n₀ m₀ : ℕ} [Fact (0 < n₀)] [Fact (0 < m₀)]
omit [DecidableEq X] [Fact (0 < n₀)] in
Lean source · statement
theorem foxAlgebraicStageTargetGroupAlgebraCoeffMap_rfl
    (N : Subgroup (FreeGroup X)) [N.Normal] :
    foxAlgebraicStageTargetGroupAlgebraCoeffMap (X := X) (n₀ := n₀) (m₀ := n₀) N dvd_rfl =
      RingHom.id _
theorem

foxAlgebraicStageTargetGroupAlgebraCoeffMap_comp

L191 ↗
FoxDifferential.foxAlgebraicStageTargetGroupAlgebraCoeffMap_comp
Documentation

Target coefficient reductions compose along divisibility.

Source context 12 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 : ℕ)
variable {n₀ m₀ : ℕ} [Fact (0 < n₀)] [Fact (0 < m₀)]
omit [DecidableEq X] [Fact (0 < n₀)] [Fact (0 < m₀)] in
Lean source · statement
theorem foxAlgebraicStageTargetGroupAlgebraCoeffMap_comp
    {k₀ : ℕ}
    (N : Subgroup (FreeGroup X)) [N.Normal] (hnm : n₀ ∣ m₀) (hmk : m₀ ∣ k₀) :
    (foxAlgebraicStageTargetGroupAlgebraCoeffMap (X := X) N hnm).comp
        (foxAlgebraicStageTargetGroupAlgebraCoeffMap (X := X) N hmk) =
      foxAlgebraicStageTargetGroupAlgebraCoeffMap (X := X) N (dvd_trans hnm hmk)

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