Module

AddCommGroup.lean

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

16 declarations indexed from sourceView source ↗

Module documentation

Fox differential: prime-power completed group algebra — system — ring — add comm group

The principal declarations in this module are:

instAddCommGroupPrimePowerCompletedGroupAlgebraStage

Each finite prime-power group-algebra stage carries its standard additive group.

instAddCommGroupPrimePowerCompletedGroupAlgebraFamily

The dependent family of finite prime-power group-algebra stages carries the pointwise additive commutative group structure.

coe_zero_primePowerCompletedGroupAlgebra

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

coe_add_primePowerCompletedGroupAlgebra

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

Imports1

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

Imported by2

instance

instZeroPrimePowerCompletedGroupAlgebra

L41 ↗

FoxDifferential.instZeroPrimePowerCompletedGroupAlgebra

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 instZeroPrimePowerCompletedGroupAlgebra : Zero (PrimePowerCompletedGroupAlgebra ℓ G) where
  zero := ⟨fun i => (0 : PrimePowerCompletedGroupAlgebraStage ℓ G i), by
    intro i j hij
    change primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
      (0 : PrimePowerCompletedGroupAlgebraStage ℓ G j) = 0
    exact map_zero _⟩

instance

instAddPrimePowerCompletedGroupAlgebra

L52 ↗

FoxDifferential.instAddPrimePowerCompletedGroupAlgebra

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 instAddPrimePowerCompletedGroupAlgebra : Add (PrimePowerCompletedGroupAlgebra ℓ G) where
  add x y := ⟨fun i =>
      (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i) +
        (show PrimePowerCompletedGroupAlgebraStage ℓ G i from y.1 i), by
    intro i j hij
    calc
      primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
          ((show PrimePowerCompletedGroupAlgebraStage ℓ G j from x.1 j) +
            (show PrimePowerCompletedGroupAlgebraStage ℓ G j from y.1 j))
        =
      primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
          (show PrimePowerCompletedGroupAlgebraStage ℓ G j from x.1 j) +
        primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
          (show PrimePowerCompletedGroupAlgebraStage ℓ G j from y.1 j) := by
            rw [map_add]
      _ =
      (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i) +
        (show PrimePowerCompletedGroupAlgebraStage ℓ G i from y.1 i) := by
            exact congrArg₂ HAdd.hAdd (x.2 i j hij) (y.2 i j hij)⟩

instance

instAddZeroClassPrimePowerCompletedGroupAlgebra

L76 ↗

FoxDifferential.instAddZeroClassPrimePowerCompletedGroupAlgebra

Documentation

Coordinatewise zero and addition on the 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 instAddZeroClassPrimePowerCompletedGroupAlgebra :
    AddZeroClass (PrimePowerCompletedGroupAlgebra ℓ G) where
  zero := 0
  add := (· + ·)
  zero_add x := by
    apply Subtype.ext
    funext i
    change (0 : PrimePowerCompletedGroupAlgebraStage ℓ G i) +
      (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i) =
        (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i)
    exact zero_add (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i)
  add_zero x := by
    apply Subtype.ext
    funext i
    change (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i) +
      (0 : PrimePowerCompletedGroupAlgebraStage ℓ G i) =
        (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i)
    exact add_zero (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i)

instance

instNegPrimePowerCompletedGroupAlgebra

L99 ↗

FoxDifferential.instNegPrimePowerCompletedGroupAlgebra

Documentation

Negation on the 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 instNegPrimePowerCompletedGroupAlgebra : Neg (PrimePowerCompletedGroupAlgebra ℓ G) where
  neg x := ⟨fun i => -(show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i), by
    intro i j hij
    change primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
        (-(show PrimePowerCompletedGroupAlgebraStage ℓ G j from x.1 j)) =
      -(show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i)
    rw [map_neg]
    exact congrArg Neg.neg (x.2 i j hij)⟩

instance

instSubPrimePowerCompletedGroupAlgebra

L112 ↗

FoxDifferential.instSubPrimePowerCompletedGroupAlgebra

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 instSubPrimePowerCompletedGroupAlgebra : Sub (PrimePowerCompletedGroupAlgebra ℓ G) where
  sub x y := ⟨fun i =>
      (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i) -
        (show PrimePowerCompletedGroupAlgebraStage ℓ G i from y.1 i), by
    intro i j hij
    change primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
        ((show PrimePowerCompletedGroupAlgebraStage ℓ G j from x.1 j) -
          (show PrimePowerCompletedGroupAlgebraStage ℓ G j from y.1 j)) =
      (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i) -
        (show PrimePowerCompletedGroupAlgebraStage ℓ G i from y.1 i)
    rw [map_sub]
    exact congrArg₂ HSub.hSub (x.2 i j hij) (y.2 i j hij)⟩

instance

instSMulNatPrimePowerCompletedGroupAlgebra

L129 ↗

FoxDifferential.instSMulNatPrimePowerCompletedGroupAlgebra

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 instSMulNatPrimePowerCompletedGroupAlgebra :
    SMul ℕ (PrimePowerCompletedGroupAlgebra ℓ G) where
  smul m x := ⟨fun i => m • (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i), by
    intro i j hij
    change primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
        (m • (show PrimePowerCompletedGroupAlgebraStage ℓ G j from x.1 j)) =
      m • (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i)
    rw [map_nsmul]
    exact congrArg (m • ·) (x.2 i j hij)⟩

instance

instSMulIntPrimePowerCompletedGroupAlgebra

L143 ↗

FoxDifferential.instSMulIntPrimePowerCompletedGroupAlgebra

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 instSMulIntPrimePowerCompletedGroupAlgebra :
    SMul ℤ (PrimePowerCompletedGroupAlgebra ℓ G) where
  smul m x := ⟨fun i => m • (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i), by
    intro i j hij
    change primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
        (m • (show PrimePowerCompletedGroupAlgebraStage ℓ G j from x.1 j)) =
      m • (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i)
    rw [map_zsmul]
    exact congrArg (m • ·) (x.2 i j hij)⟩

def

instAddCommGroupPrimePowerCompletedGroupAlgebraStage

L154 ↗

FoxDifferential.instAddCommGroupPrimePowerCompletedGroupAlgebraStage

Documentation

Each finite prime-power group-algebra stage carries its standard additive group.

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 instAddCommGroupPrimePowerCompletedGroupAlgebraStage
    (i : PrimePowerCompletedGroupAlgebraIndex G) :
    AddCommGroup ((primePowerCompletedGroupAlgebraSystem ℓ G).X i)

def

instAddCommGroupPrimePowerCompletedGroupAlgebraFamily

L166 ↗

FoxDifferential.instAddCommGroupPrimePowerCompletedGroupAlgebraFamily

Documentation

The dependent family of finite prime-power group-algebra stages carries the pointwise additive commutative group structure.

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]
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebraStage

Lean source · statement

def instAddCommGroupPrimePowerCompletedGroupAlgebraFamily :
    AddCommGroup
      ((i : PrimePowerCompletedGroupAlgebraIndex G) →
        (primePowerCompletedGroupAlgebraSystem ℓ G).X i)

theorem

coe_zero_primePowerCompletedGroupAlgebra

L177 ↗

FoxDifferential.coe_zero_primePowerCompletedGroupAlgebra

Documentation

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

Source context 10 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]
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebraStage
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebraFamily
omit [Fact (0 < ℓ)] in

Lean source · statement

theorem coe_zero_primePowerCompletedGroupAlgebra :
    ((0 : PrimePowerCompletedGroupAlgebra ℓ G) :
      (i : PrimePowerCompletedGroupAlgebraIndex G) →
        (primePowerCompletedGroupAlgebraSystem ℓ G).X i) = 0

theorem

coe_add_primePowerCompletedGroupAlgebra

L187 ↗

FoxDifferential.coe_add_primePowerCompletedGroupAlgebra

Documentation

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

Source context 10 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]
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebraStage
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebraFamily
omit [Fact (0 < ℓ)] in

Lean source · statement

theorem coe_add_primePowerCompletedGroupAlgebra
    (x y : PrimePowerCompletedGroupAlgebra ℓ G) :
    ((x + y : PrimePowerCompletedGroupAlgebra ℓ G) :
      (i : PrimePowerCompletedGroupAlgebraIndex G) →
        (primePowerCompletedGroupAlgebraSystem ℓ G).X i) = x + y

theorem

coe_neg_primePowerCompletedGroupAlgebra

L198 ↗

FoxDifferential.coe_neg_primePowerCompletedGroupAlgebra

Documentation

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

Source context 10 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]
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebraStage
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebraFamily
omit [Fact (0 < ℓ)] in

Lean source · statement

theorem coe_neg_primePowerCompletedGroupAlgebra
    (x : PrimePowerCompletedGroupAlgebra ℓ G) :
    ((-x : PrimePowerCompletedGroupAlgebra ℓ G) :
      (i : PrimePowerCompletedGroupAlgebraIndex G) →
        (primePowerCompletedGroupAlgebraSystem ℓ G).X i) = -x

theorem

coe_sub_primePowerCompletedGroupAlgebra

L209 ↗

FoxDifferential.coe_sub_primePowerCompletedGroupAlgebra

Documentation

The inclusion of the prime-power completed group algebra preserves subtraction.

Source context 10 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]
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebraStage
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebraFamily
omit [Fact (0 < ℓ)] in

Lean source · statement

theorem coe_sub_primePowerCompletedGroupAlgebra
    (x y : PrimePowerCompletedGroupAlgebra ℓ G) :
    ((x - y : PrimePowerCompletedGroupAlgebra ℓ G) :
      (i : PrimePowerCompletedGroupAlgebraIndex G) →
        (primePowerCompletedGroupAlgebraSystem ℓ G).X i) = x - y

theorem

coe_nsmul_primePowerCompletedGroupAlgebra

L223 ↗

FoxDifferential.coe_nsmul_primePowerCompletedGroupAlgebra

Documentation

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

Source context 10 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]
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebraStage
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebraFamily
omit [Fact (0 < ℓ)] in

Lean source · statement

theorem coe_nsmul_primePowerCompletedGroupAlgebra
    (m : ℕ) (x : PrimePowerCompletedGroupAlgebra ℓ G) :
    ((m • x : PrimePowerCompletedGroupAlgebra ℓ G) :
      (i : PrimePowerCompletedGroupAlgebraIndex G) →
        (primePowerCompletedGroupAlgebraSystem ℓ G).X i) = m • x

theorem

coe_zsmul_primePowerCompletedGroupAlgebra

L237 ↗

FoxDifferential.coe_zsmul_primePowerCompletedGroupAlgebra

Documentation

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

Source context 10 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]
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebraStage
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebraFamily
omit [Fact (0 < ℓ)] in

Lean source · statement

theorem coe_zsmul_primePowerCompletedGroupAlgebra
    (m : ℤ) (x : PrimePowerCompletedGroupAlgebra ℓ G) :
    ((m • x : PrimePowerCompletedGroupAlgebra ℓ G) :
      (i : PrimePowerCompletedGroupAlgebraIndex G) →
        (primePowerCompletedGroupAlgebraSystem ℓ G).X i) = m • x

def

instAddCommGroupPrimePowerCompletedGroupAlgebra

L249 ↗

FoxDifferential.instAddCommGroupPrimePowerCompletedGroupAlgebra

Documentation

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

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 (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebraStage
attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebraFamily

Lean source · statement

def instAddCommGroupPrimePowerCompletedGroupAlgebra :
    AddCommGroup (PrimePowerCompletedGroupAlgebra ℓ G)

Module documentation

Fox differential: prime-power completed group algebra — system — ring — add comm group

Declarations