Yamaguchi Lean 4 Library
ProCGroups.FoxDifferential.Completed.ProCIntegerCoefficients.AugmentationIdeal.Basic
ProCGroups/FoxDifferential/Completed/ProCIntegerCoefficients/AugmentationIdeal/Basic

ProCGroups.FoxDifferential.Completed.ProCIntegerCoefficients.AugmentationIdeal.Basic

8 Theorems | 3 Definitions

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.
imports
Imported by

Declarations

Definition FoxDifferential.zcCompletedGroupAlgebraStandardAugmentationIdeal 
def zcCompletedGroupAlgebraStandardAugmentationIdeal :
    Ideal (ZCCompletedGroupAlgebra C H) :=
  Ideal.span (Set.range fun h : H => zcGroupLike C H h - 1)

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.

Theorem FoxDifferential.zcCompletedGroupAlgebraStandardAugmentationIdeal_eq_span 
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)

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

Show Lean proof
Theorem FoxDifferential.zcGroupLike_sub_one_mem_standardAugmentationIdeal 
theorem zcGroupLike_sub_one_mem_standardAugmentationIdeal (h : H) :
    zcGroupLike C H h - 1 ∈ zcCompletedGroupAlgebraStandardAugmentationIdeal C H

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

Show Lean proof
Theorem FoxDifferential.zcCompletedGroupAlgebraBoundary_mem_standardAugmentationIdeal 
theorem zcCompletedGroupAlgebraBoundary_mem_standardAugmentationIdeal
    (ψ : G →* H) (g : G) :
    zcCompletedGroupAlgebraBoundary C ψ g ∈
      zcCompletedGroupAlgebraStandardAugmentationIdeal C H

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

Show Lean proof
Definition FoxDifferential.zcCompletedGroupAlgebraBoundaryToStandardAugmentationIdeal 
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

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

Definition FoxDifferential.zcToStdAugIdeal 
def zcToStdAugIdeal
    (ψ : G →* H) :
    ZCCompletedDifferentialModule C ψ →ₗ[ZCCompletedGroupAlgebra C H]
      zcCompletedGroupAlgebraStandardAugmentationIdeal C H :=
  crossedHomModuleLift
    (A := zcCompletedGroupAlgebraStandardAugmentationIdeal C H)
    (zcCompletedGroupAlgebraScalar C ψ)
    (zcCompletedGroupAlgebraBoundaryToStandardAugmentationIdeal C H ψ)

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

Theorem FoxDifferential.zcToStdAugIdeal_val 
@[simp]
theorem zcToStdAugIdeal_val
    (ψ : G →* H) (x : ZCCompletedDifferentialModule C ψ) :
    ((zcToStdAugIdeal C H ψ x :
      ZCCompletedGroupAlgebra C H)) =
      zcToCompletedGroupAlgebra C ψ x

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

Show Lean proof
Theorem FoxDifferential.zcToCompletedGroupAlgebra_mem_standardAugmentationIdeal 
theorem zcToCompletedGroupAlgebra_mem_standardAugmentationIdeal
    (ψ : G →* H) (x : ZCCompletedDifferentialModule C ψ) :
    zcToCompletedGroupAlgebra C ψ x ∈
      zcCompletedGroupAlgebraStandardAugmentationIdeal C H

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

Show Lean proof
Theorem FoxDifferential.zcToCompletedGroupAlgebra_range_le_standardAugmentationIdeal 
theorem zcToCompletedGroupAlgebra_range_le_standardAugmentationIdeal
    (ψ : G →* H) :
    LinearMap.range (zcToCompletedGroupAlgebra C ψ) ≤
      (zcCompletedGroupAlgebraStandardAugmentationIdeal C H :
        Submodule (ZCCompletedGroupAlgebra C H) (ZCCompletedGroupAlgebra C H))

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

Show Lean proof
Theorem FoxDifferential.zcToCompletedGroupAlgebra_range_eq_standardAugmentationIdeal_of_surjective 
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))

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

Show Lean proof
Theorem FoxDifferential.zcToStdAugIdeal_surjective_of_surjective 
theorem zcToStdAugIdeal_surjective_of_surjective
    (ψ : G →* H) (hψ : Function.Surjective ψ) :
    Function.Surjective
      (zcToStdAugIdeal C H ψ)

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

Show Lean proof