NYLL
Module

AllFinite.lean

Nyll.ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Basic.StageCoeffMap.AllFinite
7 declarations indexed from sourceView source ↗

Module documentation

Fox differential: prime-power completed group algebra — basic — stage coeff map — all finite

The principal declarations in this module are:

  • modNCompletedGroupAlgebraStageCoeffMap

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

  • modNCompletedGroupAlgebraStageCoeffMap_of

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

  • modNCompletedGroupAlgebraStageCoeffMap_rfl

The all-finite stage coefficient map for reflexive divisibility is the identity ring homomorphism.

  • modNCompletedGroupAlgebraStageCoeffMap_comp

All-finite stage coefficient maps compose according to transitivity of modulus divisibility.

Imports1
Imported by2

Declarations

abbrev

modNCompletedGroupAlgebraStageCoeffMap

L41 ↗
FoxDifferential.modNCompletedGroupAlgebraStageCoeffMap
Documentation

The coefficient reduction map on one 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 modNCompletedGroupAlgebraStageCoeffMap
    (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) (hnm : n ∣ m) :
    ModNCompletedGroupAlgebraStage m G U →+* ModNCompletedGroupAlgebraStage n G U
theorem

modNCompletedGroupAlgebraStageCoeffMap_of

L53 ↗
FoxDifferential.modNCompletedGroupAlgebraStageCoeffMap_of
Documentation

The all-finite 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 modNCompletedGroupAlgebraStageCoeffMap_of
    (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) (hnm : n ∣ m)
    (q : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G U) :
    modNCompletedGroupAlgebraStageCoeffMap (n := n) (m := m) (G := G) U hnm
        (MonoidAlgebra.of (ModNCompletedCoeff m) _ q) =
      MonoidAlgebra.of (ModNCompletedCoeff n) _ q
theorem

modNCompletedGroupAlgebraStageCoeffMap_rfl

L68 ↗
FoxDifferential.modNCompletedGroupAlgebraStageCoeffMap_rfl
Documentation

The all-finite 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 modNCompletedGroupAlgebraStageCoeffMap_rfl
    (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) :
    modNCompletedGroupAlgebraStageCoeffMap (n := n) (m := n) (G := G) U dvd_rfl =
      RingHom.id _
theorem

modNCompletedGroupAlgebraStageCoeffMap_comp

L92 ↗
FoxDifferential.modNCompletedGroupAlgebraStageCoeffMap_comp
Documentation

All-finite 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 modNCompletedGroupAlgebraStageCoeffMap_comp
    (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) (hnm : n ∣ m) (hmk : m ∣ k) :
    (modNCompletedGroupAlgebraStageCoeffMap (n := n) (m := m) (G := G) U hnm).comp
        (modNCompletedGroupAlgebraStageCoeffMap (n := m) (m := k) (G := G) U hmk) =
      modNCompletedGroupAlgebraStageCoeffMap (n := n) (m := k) (G := G) U
        (dvd_trans hnm hmk)
theorem

modNCompletedGroupAlgebraStageCoeffMap_compatible

L122 ↗
FoxDifferential.modNCompletedGroupAlgebraStageCoeffMap_compatible
Documentation

All-finite 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 modNCompletedGroupAlgebraStageCoeffMap_compatible
    {U V : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G} (hUV : U ≤ V) (hnm : n ∣ m) :
    (modNCompletedGroupAlgebraStageCoeffMap (n := n) (m := m) (G := G) U hnm).comp
        (modNCompletedGroupAlgebraTransition m G hUV) =
      (modNCompletedGroupAlgebraTransition n G hUV).comp
        (modNCompletedGroupAlgebraStageCoeffMap (n := n) (m := m) (G := G) V hnm)
theorem

modNCompletedGroupAlgebraStageCoeffMap_single_apply

L163 ↗
FoxDifferential.modNCompletedGroupAlgebraStageCoeffMap_single_apply
Documentation

The all-finite 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 modNCompletedGroupAlgebraStageCoeffMap_single_apply
    (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) (hnm : n ∣ m)
    (q : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G U)
    (a : ModNCompletedCoeff m) :
    modNCompletedGroupAlgebraStageCoeffMap (n := n) (m := m) (G := G) U hnm
        (MonoidAlgebra.single q a) =
      MonoidAlgebra.single q (modNCompletedCoeffMap (n := n) (m := m) hnm a)
theorem

modNCompletedGroupAlgebraStageCoeffMap_surjective

L197 ↗
FoxDifferential.modNCompletedGroupAlgebraStageCoeffMap_surjective
Documentation

An all-finite 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 modNCompletedGroupAlgebraStageCoeffMap_surjective
    (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) (hnm : n ∣ m) :
    Function.Surjective
      (modNCompletedGroupAlgebraStageCoeffMap (n := n) (m := m) (G := G) U hnm)

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