Module

Basic.lean

Nyll.ProCGroups.FoxDifferential.Completed.ProCIntegerCoefficients.AugmentationIdeal.Basic

11 declarations indexed from sourceView source ↗

Module documentation

Fox differential: completed — \(\mathbb{Z}_C\) coefficients — augmentation ideal — basic

The principal declarations in this module are:

zcCompletedGroupAlgebraStandardAugmentationIdeal

The algebraic ideal generated by the standard completed augmentation generators \([h]-1\). The completed augmentation ideal itself is the kernel of the completed augmentation map, defined in the completed augmentation construction with \(\mathbb{Z}_C\)-coefficients.

zcCompletedGroupAlgebraBoundaryToStandardAugmentationIdeal

The completed Fox boundary, with codomain restricted to the algebraic standard augmentation-generator ideal.

zcCompletedGroupAlgebraStandardAugmentationIdeal_eq_span

The standard completed augmentation-generator ideal, viewed as a submodule, is the submodule span of the standard generators.

zcGroupLike_sub_one_mem_standardAugmentationIdeal

Each completed group-like generator \([h]-1\) lies in the algebraic standard augmentation-generator ideal.

Imports2

Nyll.ProCGroups.FoxDifferential.Completed.ProCIntegerCoefficients.Core
Mathlib.RingTheory.Ideal.Basic

Imported by2

def

zcCompletedGroupAlgebraStandardAugmentationIdeal

L46 ↗

FoxDifferential.zcCompletedGroupAlgebraStandardAugmentationIdeal

Documentation

Source context 6 commands

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

namespace FoxDifferential
noncomputable section
universe u
section AugmentationIdeal
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

def zcCompletedGroupAlgebraStandardAugmentationIdeal :
    Ideal (ZCCompletedGroupAlgebra C H)

theorem

zcCompletedGroupAlgebraStandardAugmentationIdeal_eq_span

L54 ↗

FoxDifferential.zcCompletedGroupAlgebraStandardAugmentationIdeal_eq_span

Documentation

The standard completed augmentation-generator ideal, viewed as a submodule, is the submodule span of the standard generators.

Source context 6 commands

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

namespace FoxDifferential
noncomputable section
universe u
section AugmentationIdeal
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · full declaration

theorem zcCompletedGroupAlgebraStandardAugmentationIdeal_eq_span :
    ((zcCompletedGroupAlgebraStandardAugmentationIdeal C H :
      Ideal (ZCCompletedGroupAlgebra C H)) :
      Submodule (ZCCompletedGroupAlgebra C H) (ZCCompletedGroupAlgebra C H)) =
      Submodule.span (ZCCompletedGroupAlgebra C H)
        (Set.range fun h : H => zcGroupLike C H h - 1) :=
  rfl

theorem

zcGroupLike_sub_one_mem_standardAugmentationIdeal

L66 ↗

FoxDifferential.zcGroupLike_sub_one_mem_standardAugmentationIdeal

Documentation

Each completed group-like generator \([h]-1\) lies in the algebraic standard augmentation-generator ideal.

Source context 6 commands

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

namespace FoxDifferential
noncomputable section
universe u
section AugmentationIdeal
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem zcGroupLike_sub_one_mem_standardAugmentationIdeal (h : H) :
    zcGroupLike C H h - 1 ∈ zcCompletedGroupAlgebraStandardAugmentationIdeal C H

theorem

zcCompletedGroupAlgebraBoundary_mem_standardAugmentationIdeal

L73 ↗

FoxDifferential.zcCompletedGroupAlgebraBoundary_mem_standardAugmentationIdeal

Documentation

The completed Fox boundary lies in the algebraic standard augmentation-generator ideal.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
universe u
section AugmentationIdeal
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {G : Type u} [Group G]

Lean source · statement

theorem zcCompletedGroupAlgebraBoundary_mem_standardAugmentationIdeal
    (ψ : G →* H) (g : G) :
    zcCompletedGroupAlgebraBoundary C ψ g ∈
      zcCompletedGroupAlgebraStandardAugmentationIdeal C H

def

zcCompletedGroupAlgebraBoundaryToStandardAugmentationIdeal

L85 ↗

FoxDifferential.zcCompletedGroupAlgebraBoundaryToStandardAugmentationIdeal

Documentation

The completed Fox boundary, with codomain restricted to the algebraic standard augmentation-generator ideal.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
universe u
section AugmentationIdeal
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {G : Type u} [Group G]

Lean source · full declaration

def zcCompletedGroupAlgebraBoundaryToStandardAugmentationIdeal
    (ψ : G →* H) :
    ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ)
      (zcCompletedGroupAlgebraStandardAugmentationIdeal C H) where
  toFun g :=
    ⟨zcCompletedGroupAlgebraBoundary C ψ g,
      zcCompletedGroupAlgebraBoundary_mem_standardAugmentationIdeal C H ψ g⟩
  map_mul' g h := by
    apply Subtype.ext
    exact (zcCompletedGroupAlgebraBoundary C ψ).map_mul g h

def

zcToStdAugIdeal

L100 ↗

FoxDifferential.zcToStdAugIdeal

Documentation

The completed Fox tail is restricted to the algebraic standard augmentation ideal as its codomain.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
universe u
section AugmentationIdeal
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {G : Type u} [Group G]

Lean source · statement

def zcToStdAugIdeal
    (ψ : G →* H) :
    ZCCompletedDifferentialModule C ψ →ₗ[ZCCompletedGroupAlgebra C H]
      zcCompletedGroupAlgebraStandardAugmentationIdeal C H

theorem

zcToStdAugIdeal_val

L114 ↗

FoxDifferential.zcToStdAugIdeal_val

Documentation

The value of the standard-augmentation-ideal-valued completed Fox tail is the underlying completed group-algebra tail.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
universe u
section AugmentationIdeal
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {G : Type u} [Group G]

Lean source · statement

theorem zcToStdAugIdeal_val
    (ψ : G →* H) (x : ZCCompletedDifferentialModule C ψ) :
    ((zcToStdAugIdeal C H ψ x :
      ZCCompletedGroupAlgebra C H)) =
      zcToCompletedGroupAlgebra C ψ x

theorem

zcToCompletedGroupAlgebra_mem_standardAugmentationIdeal

L134 ↗

FoxDifferential.zcToCompletedGroupAlgebra_mem_standardAugmentationIdeal

Documentation

The completed Fox tail lands in the algebraic standard augmentation-generator ideal.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
universe u
section AugmentationIdeal
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {G : Type u} [Group G]

Lean source · statement

theorem zcToCompletedGroupAlgebra_mem_standardAugmentationIdeal
    (ψ : G →* H) (x : ZCCompletedDifferentialModule C ψ) :
    zcToCompletedGroupAlgebra C ψ x ∈
      zcCompletedGroupAlgebraStandardAugmentationIdeal C H

theorem

zcToCompletedGroupAlgebra_range_le_standardAugmentationIdeal

L145 ↗

FoxDifferential.zcToCompletedGroupAlgebra_range_le_standardAugmentationIdeal

Documentation

The range of the completed Fox tail is contained in the algebraic standard augmentation-generator ideal.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
universe u
section AugmentationIdeal
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {G : Type u} [Group G]

Lean source · statement

theorem zcToCompletedGroupAlgebra_range_le_standardAugmentationIdeal
    (ψ : G →* H) :
    LinearMap.range (zcToCompletedGroupAlgebra C ψ) ≤
      (zcCompletedGroupAlgebraStandardAugmentationIdeal C H :
        Submodule (ZCCompletedGroupAlgebra C H) (ZCCompletedGroupAlgebra C H))

theorem

zcToCompletedGroupAlgebra_range_eq_standardAugmentationIdeal_of_surjective

L157 ↗

FoxDifferential.zcToCompletedGroupAlgebra_range_eq_standardAugmentationIdeal_of_surjective

Documentation

If \(\psi\) is surjective, the completed Fox tail has range exactly the algebraic standard augmentation-generator ideal.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
universe u
section AugmentationIdeal
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {G : Type u} [Group G]

Lean source · statement

theorem zcToCompletedGroupAlgebra_range_eq_standardAugmentationIdeal_of_surjective
    (ψ : G →* H) (hψ : Function.Surjective ψ) :
    LinearMap.range (zcToCompletedGroupAlgebra C ψ) =
      (zcCompletedGroupAlgebraStandardAugmentationIdeal C H :
        Submodule (ZCCompletedGroupAlgebra C H) (ZCCompletedGroupAlgebra C H))

theorem

zcToStdAugIdeal_surjective_of_surjective

L176 ↗

FoxDifferential.zcToStdAugIdeal_surjective_of_surjective

Documentation

If \(\psi\) is surjective, the standard-augmentation-ideal-valued completed Fox tail is surjective.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
universe u
section AugmentationIdeal
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {G : Type u} [Group G]

Lean source · statement

theorem zcToStdAugIdeal_surjective_of_surjective
    (ψ : G →* H) (hψ : Function.Surjective ψ) :
    Function.Surjective
      (zcToStdAugIdeal C H ψ)

Module documentation

Fox differential: completed — \(\mathbb{Z}_C\) coefficients — augmentation ideal — basic

Declarations