NYLL
Module

StageCoeffMap.lean

Nyll.ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.InClass.StageCoeffMap
7 declarations indexed from sourceView source ↗

Module documentation

Fox differential: coefficient rings — mod-\(n\) completed group algebra — in class — stage

coeff map

The principal declarations in this module are:

  • modNCompletedGroupAlgebraStageCoeffMapInClass

The coefficient reduction map on one class-restricted finite quotient stage \(G/U\).

  • modNCompletedGroupAlgebraStageCoeffMapInClass_of

The class-indexed stage coefficient map sends a group-like basis element to the same support with its coefficient reduced modulo the target modulus.

  • modNCompletedGroupAlgebraStageCoeffMapInClass_single_apply

The class-indexed stage coefficient map sends a singleton to the same support with its coefficient reduced modulo the target modulus.

  • modNCompletedGroupAlgebraStageCoeffMapInClass_rfl

The class-indexed stage coefficient map for reflexive divisibility is the identity ring homomorphism.

Imports1
Imported by3

Declarations

abbrev

modNCompletedGroupAlgebraStageCoeffMapInClass

L44 ↗
FoxDifferential.modNCompletedGroupAlgebraStageCoeffMapInClass
Documentation

The coefficient reduction map on one class-restricted finite quotient stage \(G/U\).

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable {n m k : ℕ}
variable [Fact (0 < n)] [Fact (0 < m)] [Fact (0 < k)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < n)] [Fact (0 < m)] in
Lean source · statement
abbrev modNCompletedGroupAlgebraStageCoeffMapInClass
    (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C) (hnm : n ∣
        m) :
    ModNCompletedGroupAlgebraStageInClass m G C U →+*
      ModNCompletedGroupAlgebraStageInClass n G C U
theorem

modNCompletedGroupAlgebraStageCoeffMapInClass_of

L58 ↗
FoxDifferential.modNCompletedGroupAlgebraStageCoeffMapInClass_of
Documentation

The class-indexed stage coefficient map sends a group-like basis element to the same support with its coefficient reduced modulo the target modulus.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable {n m k : ℕ}
variable [Fact (0 < n)] [Fact (0 < m)] [Fact (0 < k)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < n)] [Fact (0 < m)] in
Lean source · statement
theorem modNCompletedGroupAlgebraStageCoeffMapInClass_of
    (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C) (hnm : n ∣ m)
    (q : CompletedGroupAlgebraQuotientInClass G C U) :
    modNCompletedGroupAlgebraStageCoeffMapInClass
        (n := n) (m := m) (G := G) C U hnm
        (MonoidAlgebra.of (ModNCompletedCoeff m) _ q) =
      MonoidAlgebra.of (ModNCompletedCoeff n) _ q
theorem

modNCompletedGroupAlgebraStageCoeffMapInClass_single_apply

L74 ↗
FoxDifferential.modNCompletedGroupAlgebraStageCoeffMapInClass_single_apply
Documentation

The class-indexed stage coefficient map sends a singleton to the same support with its coefficient reduced modulo the target modulus.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable {n m k : ℕ}
variable [Fact (0 < n)] [Fact (0 < m)] [Fact (0 < k)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < n)] [Fact (0 < m)] in
Lean source · statement
theorem modNCompletedGroupAlgebraStageCoeffMapInClass_single_apply
    (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C) (hnm : n ∣ m)
    (q : CompletedGroupAlgebraQuotientInClass G C U)
    (a : ModNCompletedCoeff m) :
    modNCompletedGroupAlgebraStageCoeffMapInClass
        (n := n) (m := m) (G := G) C U hnm
        (MonoidAlgebra.single q a) =
      MonoidAlgebra.single q (modNCompletedCoeffMap (n := n) (m := m) hnm a)
theorem

modNCompletedGroupAlgebraStageCoeffMapInClass_rfl

L112 ↗
FoxDifferential.modNCompletedGroupAlgebraStageCoeffMapInClass_rfl
Documentation

The class-indexed stage coefficient map for reflexive divisibility is the identity ring homomorphism.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable {n m k : ℕ}
variable [Fact (0 < n)] [Fact (0 < m)] [Fact (0 < k)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < n)] in
Lean source · statement
theorem modNCompletedGroupAlgebraStageCoeffMapInClass_rfl
    (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C) :
    modNCompletedGroupAlgebraStageCoeffMapInClass
        (n := n) (m := n) (G := G) C U dvd_rfl =
      RingHom.id _
theorem

modNCompletedGroupAlgebraStageCoeffMapInClass_comp

L139 ↗
FoxDifferential.modNCompletedGroupAlgebraStageCoeffMapInClass_comp
Documentation

Class-indexed stage coefficient maps compose according to transitivity of modulus divisibility.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable {n m k : ℕ}
variable [Fact (0 < n)] [Fact (0 < m)] [Fact (0 < k)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < n)] [Fact (0 < m)] [Fact (0 < k)] in
Lean source · statement
theorem modNCompletedGroupAlgebraStageCoeffMapInClass_comp
    (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C)
    (hnm : n ∣ m) (hmk : m ∣ k) :
    (modNCompletedGroupAlgebraStageCoeffMapInClass
          (n := n) (m := m) (G := G) C U hnm).comp
        (modNCompletedGroupAlgebraStageCoeffMapInClass
          (n := m) (m := k) (G := G) C U hmk) =
      modNCompletedGroupAlgebraStageCoeffMapInClass
        (n := n) (m := k) (G := G) C U (dvd_trans hnm hmk)
theorem

modNCompletedGroupAlgebraStageCoeffMapInClass_compatible

L174 ↗
FoxDifferential.modNCompletedGroupAlgebraStageCoeffMapInClass_compatible
Documentation

Class-indexed stage coefficient maps commute with finite-quotient transition maps.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable {n m k : ℕ}
variable [Fact (0 < n)] [Fact (0 < m)] [Fact (0 < k)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < n)] [Fact (0 < m)] in
Lean source · statement
theorem modNCompletedGroupAlgebraStageCoeffMapInClass_compatible
    (C : ProCGroups.FiniteGroupClass.{u})
    {U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V) (hnm : n ∣ m) :
    (modNCompletedGroupAlgebraStageCoeffMapInClass
          (n := n) (m := m) (G := G) C U hnm).comp
        (modNCompletedGroupAlgebraTransitionInClass m G C hUV) =
      (modNCompletedGroupAlgebraTransitionInClass n G C hUV).comp
        (modNCompletedGroupAlgebraStageCoeffMapInClass
          (n := n) (m := m) (G := G) C V hnm)
theorem

modNCompletedGroupAlgebraStageCoeffMapInClass_surjective

L246 ↗
FoxDifferential.modNCompletedGroupAlgebraStageCoeffMapInClass_surjective
Documentation

A class-indexed stage coefficient map is surjective when the target modulus divides the source modulus.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable {n m k : ℕ}
variable [Fact (0 < n)] [Fact (0 < m)] [Fact (0 < k)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < n)] [Fact (0 < m)] in
Lean source · statement
theorem modNCompletedGroupAlgebraStageCoeffMapInClass_surjective
    (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C) (hnm : n ∣
        m) :
    Function.Surjective
      (modNCompletedGroupAlgebraStageCoeffMapInClass
        (n := n) (m := m) (G := G) C U hnm)

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