ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.InClass.AddCommGroup

12 Theorems | 8 Instances

The principal declarations in this module are:

coe_zero_modNCompletedGroupAlgebraInClass The inclusion of the \(C\)-indexed mod-\(n\) completed group algebra into the ambient completed group algebra preserves zero. - coe_add_modNCompletedGroupAlgebraInClass The inclusion of the \(C\)-indexed mod-\(n\) completed group algebra into the ambient completed group algebra preserves addition. - coe_neg_modNCompletedGroupAlgebraInClass The inclusion of the \(C\)-indexed mod-\(n\) completed group algebra into the ambient completed group algebra preserves negation. - coe_sub_modNCompletedGroupAlgebraInClass The inclusion of the \(C\)-indexed mod-\(n\) completed group algebra into the ambient completed group algebra preserves subtraction.

import

ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.InClass.Basic

Imported by

ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.InClass

Instance FoxDifferential.instZeroModNCompletedGroupAlgebraInClass

instance instZeroModNCompletedGroupAlgebraInClass
    (C : ProCGroups.FiniteGroupClass.{u}) :
    Zero (ModNCompletedGroupAlgebraInClass n G C) where
  zero := ⟨fun U => (0 : ModNCompletedGroupAlgebraStageInClass n G C U), by
    intro U V hUV
    change modNCompletedGroupAlgebraTransitionInClass n G C hUV
      (0 : ModNCompletedGroupAlgebraStageInClass n G C V) = 0
    exact map_zero _⟩

The zero element is defined coordinatewise as the compatible family of zero elements at all finite stages.

Instance FoxDifferential.instAddModNCompletedGroupAlgebraInClass

instance instAddModNCompletedGroupAlgebraInClass
    (C : ProCGroups.FiniteGroupClass.{u}) :
    Add (ModNCompletedGroupAlgebraInClass n G C) where
  add x y := ⟨fun U =>
      (show ModNCompletedGroupAlgebraStageInClass n G C U from x.1 U) +
        (show ModNCompletedGroupAlgebraStageInClass n G C U from y.1 U), by
    intro U V hUV
    calc
      modNCompletedGroupAlgebraTransitionInClass n G C hUV
          ((show ModNCompletedGroupAlgebraStageInClass n G C V from x.1 V) +
            (show ModNCompletedGroupAlgebraStageInClass n G C V from y.1 V))
        =
          modNCompletedGroupAlgebraTransitionInClass n G C hUV
            (show ModNCompletedGroupAlgebraStageInClass n G C V from x.1 V) +
          modNCompletedGroupAlgebraTransitionInClass n G C hUV
            (show ModNCompletedGroupAlgebraStageInClass n G C V from y.1 V) := by
            rw [map_add]
      _ =
          (show ModNCompletedGroupAlgebraStageInClass n G C U from x.1 U) +
            (show ModNCompletedGroupAlgebraStageInClass n G C U from y.1 U) := by
            exact congrArg₂ HAdd.hAdd (x.2 U V hUV) (y.2 U V hUV)⟩

Addition in the mod-\(n\) completed group algebra is defined coordinatewise through finite-stage group-algebra additions.

Instance FoxDifferential.instAddZeroClassModNCompletedGroupAlgebraInClass

instance instAddZeroClassModNCompletedGroupAlgebraInClass
    (C : ProCGroups.FiniteGroupClass.{u}) :
    AddZeroClass (ModNCompletedGroupAlgebraInClass n G C) where
  zero := 0
  add := (· + ·)
  zero_add x := by
    apply Subtype.ext
    funext U
    change (0 : ModNCompletedGroupAlgebraStageInClass n G C U) +
      (show ModNCompletedGroupAlgebraStageInClass n G C U from x.1 U) =
        (show ModNCompletedGroupAlgebraStageInClass n G C U from x.1 U)
    simp only [zero_add]
  add_zero x := by
    apply Subtype.ext
    funext U
    change (show ModNCompletedGroupAlgebraStageInClass n G C U from x.1 U) +
      (0 : ModNCompletedGroupAlgebraStageInClass n G C U) =
        (show ModNCompletedGroupAlgebraStageInClass n G C U from x.1 U)
    simp only [add_zero]

Coordinatewise zero and addition on the class-indexed mod-\(n\) completed group algebra satisfy the left and right zero laws.

Instance FoxDifferential.instNegModNCompletedGroupAlgebraInClass

instance instNegModNCompletedGroupAlgebraInClass
    (C : ProCGroups.FiniteGroupClass.{u}) :
    Neg (ModNCompletedGroupAlgebraInClass n G C) where
  neg x := ⟨fun U => -(show ModNCompletedGroupAlgebraStageInClass n G C U from x.1 U), by
    intro U V hUV
    change modNCompletedGroupAlgebraTransitionInClass n G C hUV
        (-(show ModNCompletedGroupAlgebraStageInClass n G C V from x.1 V)) =
      -(show ModNCompletedGroupAlgebraStageInClass n G C U from x.1 U)
    rw [map_neg]
    exact congrArg Neg.neg (x.2 U V hUV)⟩

Negation on the \(C\)-indexed mod-\(n\) completed group algebra is defined coordinatewise through finite-stage group-algebra negations.

Instance FoxDifferential.instSubModNCompletedGroupAlgebraInClass

instance instSubModNCompletedGroupAlgebraInClass
    (C : ProCGroups.FiniteGroupClass.{u}) :
    Sub (ModNCompletedGroupAlgebraInClass n G C) where
  sub x y := ⟨fun U =>
      (show ModNCompletedGroupAlgebraStageInClass n G C U from x.1 U) -
        (show ModNCompletedGroupAlgebraStageInClass n G C U from y.1 U), by
    intro U V hUV
    change modNCompletedGroupAlgebraTransitionInClass n G C hUV
        ((show ModNCompletedGroupAlgebraStageInClass n G C V from x.1 V) -
          (show ModNCompletedGroupAlgebraStageInClass n G C V from y.1 V)) =
      (show ModNCompletedGroupAlgebraStageInClass n G C U from x.1 U) -
        (show ModNCompletedGroupAlgebraStageInClass n G C U from y.1 U)
    rw [map_sub]
    exact congrArg₂ HSub.hSub (x.2 U V hUV) (y.2 U V hUV)⟩

Subtraction on the completed group algebra is defined coordinatewise through the finite-stage group-algebra subtractions.

Instance FoxDifferential.instSMulNatModNCompletedGroupAlgebraInClass

instance instSMulNatModNCompletedGroupAlgebraInClass
    (C : ProCGroups.FiniteGroupClass.{u}) :
    SMul ℕ (ModNCompletedGroupAlgebraInClass n G C) where
  smul m x := ⟨fun U =>
      m • (show ModNCompletedGroupAlgebraStageInClass n G C U from x.1 U), by
    intro U V hUV
    change modNCompletedGroupAlgebraTransitionInClass n G C hUV
        (m • (show ModNCompletedGroupAlgebraStageInClass n G C V from x.1 V)) =
      m • (show ModNCompletedGroupAlgebraStageInClass n G C U from x.1 U)
    rw [map_nsmul]
    exact congrArg (m • ·) (x.2 U V hUV)⟩

The completed group algebra carries coefficient-ring scalar multiplication by applying the scalar action at every finite quotient stage.

Instance FoxDifferential.instSMulIntModNCompletedGroupAlgebraInClass

instance instSMulIntModNCompletedGroupAlgebraInClass
    (C : ProCGroups.FiniteGroupClass.{u}) :
    SMul ℤ (ModNCompletedGroupAlgebraInClass n G C) where
  smul m x := ⟨fun U =>
      m • (show ModNCompletedGroupAlgebraStageInClass n G C U from x.1 U), by
    intro U V hUV
    change modNCompletedGroupAlgebraTransitionInClass n G C hUV
        (m • (show ModNCompletedGroupAlgebraStageInClass n G C V from x.1 V)) =
      m • (show ModNCompletedGroupAlgebraStageInClass n G C U from x.1 U)
    rw [map_zsmul]
    exact congrArg (m • ·) (x.2 U V hUV)⟩

The completed group algebra carries coefficient-ring scalar multiplication by applying the scalar action at every finite quotient stage.

Theorem FoxDifferential.coe_zero_modNCompletedGroupAlgebraInClass

omit [Fact (0 < n)] in
@[simp]
theorem coe_zero_modNCompletedGroupAlgebraInClass
    (C : ProCGroups.FiniteGroupClass.{u}) :
    ((0 : ModNCompletedGroupAlgebraInClass n G C) :
      (U : CompletedGroupAlgebraIndexInClass G C) →
        ModNCompletedGroupAlgebraStageInClass n G C U) = 0

The inclusion of the \(C\)-indexed mod-\(n\) completed group algebra into the ambient completed group algebra preserves zero.

Show Lean proof

Theorem FoxDifferential.coe_add_modNCompletedGroupAlgebraInClass

omit [Fact (0 < n)] in
@[simp]
theorem coe_add_modNCompletedGroupAlgebraInClass
    (C : ProCGroups.FiniteGroupClass.{u})
    (x y : ModNCompletedGroupAlgebraInClass n G C) :
    ((x + y : ModNCompletedGroupAlgebraInClass n G C) :
      (U : CompletedGroupAlgebraIndexInClass G C) →
        ModNCompletedGroupAlgebraStageInClass n G C U) = x + y

The inclusion of the \(C\)-indexed mod-\(n\) completed group algebra into the ambient completed group algebra preserves addition.

Show Lean proof

Theorem FoxDifferential.coe_neg_modNCompletedGroupAlgebraInClass

omit [Fact (0 < n)] in
@[simp]
theorem coe_neg_modNCompletedGroupAlgebraInClass
    (C : ProCGroups.FiniteGroupClass.{u})
    (x : ModNCompletedGroupAlgebraInClass n G C) :
    ((-x : ModNCompletedGroupAlgebraInClass n G C) :
      (U : CompletedGroupAlgebraIndexInClass G C) →
        ModNCompletedGroupAlgebraStageInClass n G C U) = -x

The inclusion of the \(C\)-indexed mod-\(n\) completed group algebra into the ambient completed group algebra preserves negation.

Show Lean proof

Theorem FoxDifferential.coe_sub_modNCompletedGroupAlgebraInClass

omit [Fact (0 < n)] in
@[simp]
theorem coe_sub_modNCompletedGroupAlgebraInClass
    (C : ProCGroups.FiniteGroupClass.{u})
    (x y : ModNCompletedGroupAlgebraInClass n G C) :
    ((x - y : ModNCompletedGroupAlgebraInClass n G C) :
      (U : CompletedGroupAlgebraIndexInClass G C) →
        ModNCompletedGroupAlgebraStageInClass n G C U) = x - y

The inclusion of the \(C\)-indexed mod-\(n\) completed group algebra into the ambient completed group algebra preserves subtraction.

Show Lean proof

Theorem FoxDifferential.coe_nsmul_modNCompletedGroupAlgebraInClass

omit [Fact (0 < n)] in
@[simp]
theorem coe_nsmul_modNCompletedGroupAlgebraInClass
    (C : ProCGroups.FiniteGroupClass.{u})
    (m : ℕ) (x : ModNCompletedGroupAlgebraInClass n G C) :
    ((m • x : ModNCompletedGroupAlgebraInClass n G C) :
      (U : CompletedGroupAlgebraIndexInClass G C) →
        ModNCompletedGroupAlgebraStageInClass n G C U) = m • x

The inclusion of the \(C\)-indexed mod-\(n\) completed group algebra into the ambient completed group algebra preserves natural-number scalar multiplication.

Show Lean proof

Theorem FoxDifferential.coe_zsmul_modNCompletedGroupAlgebraInClass

omit [Fact (0 < n)] in
@[simp]
theorem coe_zsmul_modNCompletedGroupAlgebraInClass
    (C : ProCGroups.FiniteGroupClass.{u})
    (m : ℤ) (x : ModNCompletedGroupAlgebraInClass n G C) :
    ((m • x : ModNCompletedGroupAlgebraInClass n G C) :
      (U : CompletedGroupAlgebraIndexInClass G C) →
        ModNCompletedGroupAlgebraStageInClass n G C U) = m • x

The inclusion of the \(C\)-indexed mod-\(n\) completed group algebra into the ambient completed group algebra preserves integer scalar multiplication.

Show Lean proof

Instance FoxDifferential.instAddCommGroupModNCompletedGroupAlgebraInClass

instance instAddCommGroupModNCompletedGroupAlgebraInClass
    (C : ProCGroups.FiniteGroupClass.{u}) :
    AddCommGroup (ModNCompletedGroupAlgebraInClass n G C) :=
  Function.Injective.addCommGroup
    (fun x : ModNCompletedGroupAlgebraInClass n G C =>
      (x :
        (U : CompletedGroupAlgebraIndexInClass G C) →
          ModNCompletedGroupAlgebraStageInClass n G C U))
    Subtype.val_injective
    (coe_zero_modNCompletedGroupAlgebraInClass (n := n) (G := G) C)
    (coe_add_modNCompletedGroupAlgebraInClass (n := n) (G := G) C)
    (coe_neg_modNCompletedGroupAlgebraInClass (n := n) (G := G) C)
    (coe_sub_modNCompletedGroupAlgebraInClass (n := n) (G := G) C)
    (fun x m => coe_nsmul_modNCompletedGroupAlgebraInClass (n := n) (G := G) C m x)
    (fun x m => coe_zsmul_modNCompletedGroupAlgebraInClass (n := n) (G := G) C m x)

The class-indexed mod-\(n\) completion inherits an additive commutative group structure from its injective inclusion into the family of finite stages.

Theorem FoxDifferential.modNCompletedGroupAlgebraProjectionInClass_zero

omit [Fact (0 < n)] in
@[simp]
theorem modNCompletedGroupAlgebraProjectionInClass_zero
    (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C) :
    modNCompletedGroupAlgebraProjectionInClass n G C U
      (0 : ModNCompletedGroupAlgebraInClass n G C) = 0

The finite-stage projection sends \(0\) to \(0\).

Show Lean proof

Theorem FoxDifferential.modNCompletedGroupAlgebraProjectionInClass_add

omit [Fact (0 < n)] in
@[simp]
theorem modNCompletedGroupAlgebraProjectionInClass_add
    (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C)
    (x y : ModNCompletedGroupAlgebraInClass n G C) :
    modNCompletedGroupAlgebraProjectionInClass n G C U (x + y) =
      modNCompletedGroupAlgebraProjectionInClass n G C U x +
        modNCompletedGroupAlgebraProjectionInClass n G C U y

The mod-\(n\) finite-stage projection preserves addition.

Show Lean proof

Theorem FoxDifferential.modNCompletedGroupAlgebraProjectionInClass_neg

omit [Fact (0 < n)] in
@[simp]
theorem modNCompletedGroupAlgebraProjectionInClass_neg
    (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C)
    (x : ModNCompletedGroupAlgebraInClass n G C) :
    modNCompletedGroupAlgebraProjectionInClass n G C U (-x) =
      -modNCompletedGroupAlgebraProjectionInClass n G C U x

The mod-\(n\) finite-stage projection preserves negation.

Show Lean proof

Theorem FoxDifferential.modNCompletedGroupAlgebraProjectionInClass_sub

omit [Fact (0 < n)] in
@[simp]
theorem modNCompletedGroupAlgebraProjectionInClass_sub
    (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C)
    (x y : ModNCompletedGroupAlgebraInClass n G C) :
    modNCompletedGroupAlgebraProjectionInClass n G C U (x - y) =
      modNCompletedGroupAlgebraProjectionInClass n G C U x -
        modNCompletedGroupAlgebraProjectionInClass n G C U y

The mod-\(n\) finite-stage projection preserves subtraction.

Show Lean proof

Theorem FoxDifferential.modNCompletedGroupAlgebraProjectionInClass_nsmul

omit [Fact (0 < n)] in
@[simp]
theorem modNCompletedGroupAlgebraProjectionInClass_nsmul
    (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C)
    (m : ℕ) (x : ModNCompletedGroupAlgebraInClass n G C) :
    modNCompletedGroupAlgebraProjectionInClass n G C U (m • x) =
      m • modNCompletedGroupAlgebraProjectionInClass n G C U x

The finite-stage projection is compatible with natural-number scalar multiplication.

Show Lean proof

Theorem FoxDifferential.modNCompletedGroupAlgebraProjectionInClass_zsmul

omit [Fact (0 < n)] in
@[simp]
theorem modNCompletedGroupAlgebraProjectionInClass_zsmul
    (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C)
    (m : ℤ) (x : ModNCompletedGroupAlgebraInClass n G C) :
    modNCompletedGroupAlgebraProjectionInClass n G C U (m • x) =
      m • modNCompletedGroupAlgebraProjectionInClass n G C U x

The finite-stage projection is compatible with integer scalar multiplication.

Show Lean proof

ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.InClass.AddCommGroup

Declarations