Module

AddCommGroup.lean

Nyll.ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.System.Ring.AddCommGroup

14 declarations indexed from sourceView source ↗

Module documentation

Fox differential: in class — system — ring — add comm group

The principal declarations in this module are:

instAddCommGroupPrimePowerCompletedGroupAlgebraInClass

The class-indexed prime-power completion inherits an additive commutative group structure from its injective inclusion into the family of finite stages.

coe_zero_primePowerCompletedGroupAlgebraInClass

The inclusion of the class-indexed prime-power completed group algebra preserves zero.

coe_add_primePowerCompletedGroupAlgebraInClass

The inclusion of the class-indexed prime-power completed group algebra preserves addition.

coe_neg_primePowerCompletedGroupAlgebraInClass

The inclusion of the class-indexed prime-power completed group algebra preserves negation.

Imports1

Nyll.ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.System.Basic

Imported by2

instance

instZeroPrimePowerCompletedGroupAlgebraInClass

L41 ↗

FoxDifferential.instZeroPrimePowerCompletedGroupAlgebraInClass

Documentation

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

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · full declaration

instance instZeroPrimePowerCompletedGroupAlgebraInClass
    (C : ProCGroups.FiniteGroupClass.{u}) :
    Zero (PrimePowerCompletedGroupAlgebraInClass ℓ G C) where
  zero := ⟨fun i => (0 : PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i), by
    intro i j hij
    change primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij
      (0 : PrimePowerCompletedGroupAlgebraStageInClass ℓ G C j) = 0
    exact map_zero _⟩

instance

instAddPrimePowerCompletedGroupAlgebraInClass

L54 ↗

FoxDifferential.instAddPrimePowerCompletedGroupAlgebraInClass

Documentation

Addition in the prime-power completed group algebra is defined coordinatewise through finite-stage group-algebra additions.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · full declaration

instance instAddPrimePowerCompletedGroupAlgebraInClass
    (C : ProCGroups.FiniteGroupClass.{u}) :
    Add (PrimePowerCompletedGroupAlgebraInClass ℓ G C) where
  add x y := ⟨fun i =>
      (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i from x.1 i) +
        (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i from y.1 i), by
    intro i j hij
    calc
      primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij
          ((show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C j from x.1 j) +
            (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C j from y.1 j))
        =
      primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij
          (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C j from x.1 j) +
        primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij
          (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C j from y.1 j) := by
            rw [map_add]
      _ =
      (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i from x.1 i) +
        (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i from y.1 i) := by
            exact congrArg₂ HAdd.hAdd (x.2 i j hij) (y.2 i j hij)⟩

instance

instAddZeroClassPrimePowerCompletedGroupAlgebraInClass

L80 ↗

FoxDifferential.instAddZeroClassPrimePowerCompletedGroupAlgebraInClass

Documentation

Coordinatewise zero and addition on the class-indexed prime-power completed group algebra satisfy the left and right zero laws.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · full declaration

instance instAddZeroClassPrimePowerCompletedGroupAlgebraInClass
    (C : ProCGroups.FiniteGroupClass.{u}) :
    AddZeroClass (PrimePowerCompletedGroupAlgebraInClass ℓ G C) where
  zero := 0
  add := (· + ·)
  zero_add x := by
    apply Subtype.ext
    funext i
    change (0 : PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i) +
      (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i from x.1 i) =
        (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i from x.1 i)
    simp only [zero_add]
  add_zero x := by
    apply Subtype.ext
    funext i
    change (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i from x.1 i) +
      (0 : PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i) =
        (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i from x.1 i)
    simp only [add_zero]

instance

instNegPrimePowerCompletedGroupAlgebraInClass

L104 ↗

FoxDifferential.instNegPrimePowerCompletedGroupAlgebraInClass

Documentation

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

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · full declaration

instance instNegPrimePowerCompletedGroupAlgebraInClass
    (C : ProCGroups.FiniteGroupClass.{u}) :
    Neg (PrimePowerCompletedGroupAlgebraInClass ℓ G C) where
  neg x := ⟨fun i => -(show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i from x.1 i), by
    intro i j hij
    change primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij
        (-(show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C j from x.1 j)) =
      -(show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i from x.1 i)
    rw [map_neg]
    exact congrArg Neg.neg (x.2 i j hij)⟩

instance

instSubPrimePowerCompletedGroupAlgebraInClass

L119 ↗

FoxDifferential.instSubPrimePowerCompletedGroupAlgebraInClass

Documentation

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

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · full declaration

instance instSubPrimePowerCompletedGroupAlgebraInClass
    (C : ProCGroups.FiniteGroupClass.{u}) :
    Sub (PrimePowerCompletedGroupAlgebraInClass ℓ G C) where
  sub x y := ⟨fun i =>
      (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i from x.1 i) -
        (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i from y.1 i), by
    intro i j hij
    change primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij
        ((show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C j from x.1 j) -
          (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C j from y.1 j)) =
      (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i from x.1 i) -
        (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i from y.1 i)
    rw [map_sub]
    exact congrArg₂ HSub.hSub (x.2 i j hij) (y.2 i j hij)⟩

instance

instSMulNatPrimePowerCompletedGroupAlgebraInClass

L138 ↗

FoxDifferential.instSMulNatPrimePowerCompletedGroupAlgebraInClass

Documentation

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

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · full declaration

instance instSMulNatPrimePowerCompletedGroupAlgebraInClass
    (C : ProCGroups.FiniteGroupClass.{u}) :
    SMul ℕ (PrimePowerCompletedGroupAlgebraInClass ℓ G C) where
  smul m x := ⟨fun i =>
      m • (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i from x.1 i), by
    intro i j hij
    change primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij
        (m • (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C j from x.1 j)) =
      m • (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i from x.1 i)
    rw [map_nsmul]
    exact congrArg (m • ·) (x.2 i j hij)⟩

instance

instSMulIntPrimePowerCompletedGroupAlgebraInClass

L154 ↗

FoxDifferential.instSMulIntPrimePowerCompletedGroupAlgebraInClass

Documentation

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

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · full declaration

instance instSMulIntPrimePowerCompletedGroupAlgebraInClass
    (C : ProCGroups.FiniteGroupClass.{u}) :
    SMul ℤ (PrimePowerCompletedGroupAlgebraInClass ℓ G C) where
  smul m x := ⟨fun i =>
      m • (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i from x.1 i), by
    intro i j hij
    change primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij
        (m • (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C j from x.1 j)) =
      m • (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i from x.1 i)
    rw [map_zsmul]
    exact congrArg (m • ·) (x.2 i j hij)⟩

theorem

coe_zero_primePowerCompletedGroupAlgebraInClass

L169 ↗

FoxDifferential.coe_zero_primePowerCompletedGroupAlgebraInClass

Documentation

The inclusion of the class-indexed prime-power completed group algebra preserves zero.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < ℓ)] in

Lean source · statement

theorem coe_zero_primePowerCompletedGroupAlgebraInClass
    (C : ProCGroups.FiniteGroupClass.{u}) :
    ((0 : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
      (i : PrimePowerCompletedGroupAlgebraIndexInClass G C) →
        PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i) = 0

theorem

coe_add_primePowerCompletedGroupAlgebraInClass

L180 ↗

FoxDifferential.coe_add_primePowerCompletedGroupAlgebraInClass

Documentation

The inclusion of the class-indexed prime-power completed group algebra preserves addition.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < ℓ)] in

Lean source · statement

theorem coe_add_primePowerCompletedGroupAlgebraInClass
    (C : ProCGroups.FiniteGroupClass.{u})
    (x y : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
    ((x + y : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
      (i : PrimePowerCompletedGroupAlgebraIndexInClass G C) →
        PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i) = x + y

theorem

coe_neg_primePowerCompletedGroupAlgebraInClass

L192 ↗

FoxDifferential.coe_neg_primePowerCompletedGroupAlgebraInClass

Documentation

The inclusion of the class-indexed prime-power completed group algebra preserves negation.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < ℓ)] in

Lean source · statement

theorem coe_neg_primePowerCompletedGroupAlgebraInClass
    (C : ProCGroups.FiniteGroupClass.{u})
    (x : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
    ((-x : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
      (i : PrimePowerCompletedGroupAlgebraIndexInClass G C) →
        PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i) = -x

theorem

coe_sub_primePowerCompletedGroupAlgebraInClass

L206 ↗

FoxDifferential.coe_sub_primePowerCompletedGroupAlgebraInClass

Documentation

Subtraction in the \(C\)-indexed prime-power completed group algebra is computed coordinatewise.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < ℓ)] in

Lean source · statement

theorem coe_sub_primePowerCompletedGroupAlgebraInClass
    (C : ProCGroups.FiniteGroupClass.{u})
    (x y : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
    ((x - y : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
      (i : PrimePowerCompletedGroupAlgebraIndexInClass G C) →
        PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i) = x - y

theorem

coe_nsmul_primePowerCompletedGroupAlgebraInClass

L221 ↗

FoxDifferential.coe_nsmul_primePowerCompletedGroupAlgebraInClass

Documentation

The inclusion of the class-indexed prime-power completed group algebra preserves natural-number scalar multiplication.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < ℓ)] in

Lean source · statement

theorem coe_nsmul_primePowerCompletedGroupAlgebraInClass
    (C : ProCGroups.FiniteGroupClass.{u})
    (m : ℕ) (x : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
    ((m • x : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
      (i : PrimePowerCompletedGroupAlgebraIndexInClass G C) →
        PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i) = m • x

theorem

coe_zsmul_primePowerCompletedGroupAlgebraInClass

L236 ↗

FoxDifferential.coe_zsmul_primePowerCompletedGroupAlgebraInClass

Documentation

The inclusion of the class-indexed prime-power completed group algebra preserves integer scalar multiplication.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < ℓ)] in

Lean source · statement

theorem coe_zsmul_primePowerCompletedGroupAlgebraInClass
    (C : ProCGroups.FiniteGroupClass.{u})
    (m : ℤ) (x : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
    ((m • x : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
      (i : PrimePowerCompletedGroupAlgebraIndexInClass G C) →
        PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i) = m • x

def

instAddCommGroupPrimePowerCompletedGroupAlgebraInClass

L249 ↗

FoxDifferential.instAddCommGroupPrimePowerCompletedGroupAlgebraInClass

Documentation

The class-indexed prime-power completion inherits an additive commutative group structure from its injective inclusion into the family of finite stages.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

def instAddCommGroupPrimePowerCompletedGroupAlgebraInClass
    (C : ProCGroups.FiniteGroupClass.{u}) :
    AddCommGroup (PrimePowerCompletedGroupAlgebraInClass ℓ G C)

Module documentation

Fox differential: in class — system — ring — add comm group

Declarations