Module

AddCommGroup.lean

Nyll.ProCGroups.FoxDifferential.Completed.FiniteStage.PrimePower.System.Limit.AddCommGroup

26 declarations indexed from sourceView source ↗

Module documentation

Fox differential: prime power — system — limit — add comm group

The principal declarations in this module are:

foxAlgebraicStagePrimePowerSourceLimitToFamily_zero

The source-limit family of zero is the zero family.

foxAlgebraicStagePrimePowerSourceLimitToFamily_add

The source-limit family map preserves addition.

foxAlgebraicStagePrimePowerSourceLimitToFamily_neg

The source-limit family map preserves negation.

foxAlgebraicStagePrimePowerSourceLimitToFamily_sub

The source-limit family map preserves subtraction.

Imports1

Nyll.ProCGroups.FoxDifferential.Completed.FiniteStage.PrimePower.System.Limit.Basic

Imported by2

instance

instZeroFoxAlgebraicStagePrimePowerSourceLimit

L46 ↗

FoxDifferential.instZeroFoxAlgebraicStagePrimePowerSourceLimit

Documentation

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

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 v
variable (ℓ : ℕ)
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

Lean source · full declaration

instance instZeroFoxAlgebraicStagePrimePowerSourceLimit
    (N : Subgroup (FreeGroup X)) :
    Zero (FoxAlgebraicStagePrimePowerSourceLimit (ℓ := ℓ) (X := X) N) where
  zero := ⟨fun a => (0 : foxAlgebraicStagePrimePowerSourceGroupAlgebra (ℓ := ℓ) (X := X) N a),
    by
      intro a b hab
      change foxAlgebraicStagePrimePowerSourceTransition (ℓ := ℓ) (X := X) N hab
          (0 : foxAlgebraicStagePrimePowerSourceGroupAlgebra (ℓ := ℓ) (X := X) N b) = 0
      exact map_zero _⟩

instance

instAddFoxAlgebraicStagePrimePowerSourceLimit

L60 ↗

FoxDifferential.instAddFoxAlgebraicStagePrimePowerSourceLimit

Documentation

Addition in the finite Fox prime-power source limit is defined coordinatewise through finite stages.

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 v
variable (ℓ : ℕ)
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

Lean source · full declaration

instance instAddFoxAlgebraicStagePrimePowerSourceLimit
    (N : Subgroup (FreeGroup X)) :
    Add (FoxAlgebraicStagePrimePowerSourceLimit (ℓ := ℓ) (X := X) N) where
  add x y := ⟨fun a =>
      (show foxAlgebraicStagePrimePowerSourceGroupAlgebra (ℓ := ℓ) (X := X) N a from x.1 a) +
        (show foxAlgebraicStagePrimePowerSourceGroupAlgebra (ℓ := ℓ) (X := X) N a from y.1 a),
    by
      intro a b hab
      change foxAlgebraicStagePrimePowerSourceTransition (ℓ := ℓ) (X := X) N hab
          ((show foxAlgebraicStagePrimePowerSourceGroupAlgebra (ℓ := ℓ) (X := X) N b from x.1 b) +
            (show foxAlgebraicStagePrimePowerSourceGroupAlgebra (ℓ := ℓ) (X := X) N b from y.1 b)) =
        (show foxAlgebraicStagePrimePowerSourceGroupAlgebra (ℓ := ℓ) (X := X) N a from x.1 a) +
          (show foxAlgebraicStagePrimePowerSourceGroupAlgebra (ℓ := ℓ) (X := X) N a from y.1 a)
      rw [map_add]
      exact congrArg₂ HAdd.hAdd (x.2 a b hab) (y.2 a b hab)⟩

instance

instNegFoxAlgebraicStagePrimePowerSourceLimit

L80 ↗

FoxDifferential.instNegFoxAlgebraicStagePrimePowerSourceLimit

Documentation

Negation on the prime-power source inverse limit is defined coordinatewise through finite-stage source negations.

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 v
variable (ℓ : ℕ)
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

Lean source · full declaration

instance instNegFoxAlgebraicStagePrimePowerSourceLimit
    (N : Subgroup (FreeGroup X)) :
    Neg (FoxAlgebraicStagePrimePowerSourceLimit (ℓ := ℓ) (X := X) N) where
  neg x := ⟨fun a =>
      -(show foxAlgebraicStagePrimePowerSourceGroupAlgebra (ℓ := ℓ) (X := X) N a from x.1 a),
    by
      intro a b hab
      change foxAlgebraicStagePrimePowerSourceTransition (ℓ := ℓ) (X := X) N hab
          (-(show foxAlgebraicStagePrimePowerSourceGroupAlgebra (ℓ := ℓ) (X := X) N b from x.1 b)) =
        -(show foxAlgebraicStagePrimePowerSourceGroupAlgebra (ℓ := ℓ) (X := X) N a from x.1 a)
      rw [map_neg]
      exact congrArg Neg.neg (x.2 a b hab)⟩

instance

instSubFoxAlgebraicStagePrimePowerSourceLimit

L97 ↗

FoxDifferential.instSubFoxAlgebraicStagePrimePowerSourceLimit

Documentation

Subtraction on the prime-power source inverse limit is defined coordinatewise through finite-stage source subtractions.

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 v
variable (ℓ : ℕ)
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

Lean source · full declaration

instance instSubFoxAlgebraicStagePrimePowerSourceLimit
    (N : Subgroup (FreeGroup X)) :
    Sub (FoxAlgebraicStagePrimePowerSourceLimit (ℓ := ℓ) (X := X) N) where
  sub x y := ⟨fun a =>
      (show foxAlgebraicStagePrimePowerSourceGroupAlgebra (ℓ := ℓ) (X := X) N a from x.1 a) -
        (show foxAlgebraicStagePrimePowerSourceGroupAlgebra (ℓ := ℓ) (X := X) N a from y.1 a),
    by
      intro a b hab
      change foxAlgebraicStagePrimePowerSourceTransition (ℓ := ℓ) (X := X) N hab
          ((show foxAlgebraicStagePrimePowerSourceGroupAlgebra (ℓ := ℓ) (X := X) N b from x.1 b) -
            (show foxAlgebraicStagePrimePowerSourceGroupAlgebra (ℓ := ℓ) (X := X) N b from y.1 b)) =
        (show foxAlgebraicStagePrimePowerSourceGroupAlgebra (ℓ := ℓ) (X := X) N a from x.1 a) -
          (show foxAlgebraicStagePrimePowerSourceGroupAlgebra (ℓ := ℓ) (X := X) N a from y.1 a)
      rw [map_sub]
      exact congrArg₂ HSub.hSub (x.2 a b hab) (y.2 a b hab)⟩

instance

instSMulNatFoxAlgebraicStagePrimePowerSourceLimit

L117 ↗

FoxDifferential.instSMulNatFoxAlgebraicStagePrimePowerSourceLimit

Documentation

The prime-power source inverse limit carries natural-number scalar multiplication coordinatewise.

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 v
variable (ℓ : ℕ)
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

Lean source · full declaration

instance instSMulNatFoxAlgebraicStagePrimePowerSourceLimit
    (N : Subgroup (FreeGroup X)) :
    SMul ℕ (FoxAlgebraicStagePrimePowerSourceLimit (ℓ := ℓ) (X := X) N) where
  smul m x := ⟨fun a =>
      m • (show foxAlgebraicStagePrimePowerSourceGroupAlgebra (ℓ := ℓ) (X := X) N a from x.1 a),
    by
      intro a b hab
      change foxAlgebraicStagePrimePowerSourceTransition (ℓ := ℓ) (X := X) N hab
          (m • (show foxAlgebraicStagePrimePowerSourceGroupAlgebra (ℓ := ℓ) (X := X) N b from
              x.1 b)) =
        m • (show foxAlgebraicStagePrimePowerSourceGroupAlgebra (ℓ := ℓ) (X := X) N a from x.1 a)
      rw [map_nsmul]
      exact congrArg (m • ·) (x.2 a b hab)⟩

instance

instSMulIntFoxAlgebraicStagePrimePowerSourceLimit

L132 ↗

FoxDifferential.instSMulIntFoxAlgebraicStagePrimePowerSourceLimit

Documentation

The prime-power source inverse limit carries integer scalar multiplication coordinatewise.

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 v
variable (ℓ : ℕ)
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

Lean source · full declaration

instance instSMulIntFoxAlgebraicStagePrimePowerSourceLimit
    (N : Subgroup (FreeGroup X)) :
    SMul ℤ (FoxAlgebraicStagePrimePowerSourceLimit (ℓ := ℓ) (X := X) N) where
  smul m x := ⟨fun a =>
      m • (show foxAlgebraicStagePrimePowerSourceGroupAlgebra (ℓ := ℓ) (X := X) N a from x.1 a),
    by
      intro a b hab
      change foxAlgebraicStagePrimePowerSourceTransition (ℓ := ℓ) (X := X) N hab
          (m • (show foxAlgebraicStagePrimePowerSourceGroupAlgebra (ℓ := ℓ) (X := X) N b from
              x.1 b)) =
        m • (show foxAlgebraicStagePrimePowerSourceGroupAlgebra (ℓ := ℓ) (X := X) N a from x.1 a)
      rw [map_zsmul]
      exact congrArg (m • ·) (x.2 a b hab)⟩

theorem

foxAlgebraicStagePrimePowerSourceLimitToFamily_zero

L148 ↗

FoxDifferential.foxAlgebraicStagePrimePowerSourceLimitToFamily_zero

Documentation

The source-limit family of zero is the zero family.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u v
variable (ℓ : ℕ)
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
omit [DecidableEq X] in

Lean source · statement

theorem foxAlgebraicStagePrimePowerSourceLimitToFamily_zero
    (N : Subgroup (FreeGroup X)) :
    foxAlgebraicStagePrimePowerSourceLimitToFamily (ℓ := ℓ) (X := X) N 0 = 0

theorem

foxAlgebraicStagePrimePowerSourceLimitToFamily_add

L156 ↗

FoxDifferential.foxAlgebraicStagePrimePowerSourceLimitToFamily_add

Documentation

The source-limit family map preserves addition.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u v
variable (ℓ : ℕ)
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
omit [DecidableEq X] in

Lean source · statement

theorem foxAlgebraicStagePrimePowerSourceLimitToFamily_add
    (N : Subgroup (FreeGroup X))
    (x y : FoxAlgebraicStagePrimePowerSourceLimit (ℓ := ℓ) (X := X) N) :
    foxAlgebraicStagePrimePowerSourceLimitToFamily (ℓ := ℓ) (X := X) N (x + y) =
      foxAlgebraicStagePrimePowerSourceLimitToFamily (ℓ := ℓ) (X := X) N x +
        foxAlgebraicStagePrimePowerSourceLimitToFamily (ℓ := ℓ) (X := X) N y

theorem

foxAlgebraicStagePrimePowerSourceLimitToFamily_neg

L167 ↗

FoxDifferential.foxAlgebraicStagePrimePowerSourceLimitToFamily_neg

Documentation

The source-limit family map preserves negation.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u v
variable (ℓ : ℕ)
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
omit [DecidableEq X] in

Lean source · statement

theorem foxAlgebraicStagePrimePowerSourceLimitToFamily_neg
    (N : Subgroup (FreeGroup X))
    (x : FoxAlgebraicStagePrimePowerSourceLimit (ℓ := ℓ) (X := X) N) :
    foxAlgebraicStagePrimePowerSourceLimitToFamily (ℓ := ℓ) (X := X) N (-x) =
      -foxAlgebraicStagePrimePowerSourceLimitToFamily (ℓ := ℓ) (X := X) N x

theorem

foxAlgebraicStagePrimePowerSourceLimitToFamily_sub

L177 ↗

FoxDifferential.foxAlgebraicStagePrimePowerSourceLimitToFamily_sub

Documentation

The source-limit family map preserves subtraction.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u v
variable (ℓ : ℕ)
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
omit [DecidableEq X] in

Lean source · statement

theorem foxAlgebraicStagePrimePowerSourceLimitToFamily_sub
    (N : Subgroup (FreeGroup X))
    (x y : FoxAlgebraicStagePrimePowerSourceLimit (ℓ := ℓ) (X := X) N) :
    foxAlgebraicStagePrimePowerSourceLimitToFamily (ℓ := ℓ) (X := X) N (x - y) =
      foxAlgebraicStagePrimePowerSourceLimitToFamily (ℓ := ℓ) (X := X) N x -
        foxAlgebraicStagePrimePowerSourceLimitToFamily (ℓ := ℓ) (X := X) N y

theorem

foxAlgebraicStagePrimePowerSourceLimitToFamily_nsmul

L188 ↗

FoxDifferential.foxAlgebraicStagePrimePowerSourceLimitToFamily_nsmul

Documentation

The source-limit family map preserves natural-number scalar multiplication.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u v
variable (ℓ : ℕ)
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
omit [DecidableEq X] in

Lean source · statement

theorem foxAlgebraicStagePrimePowerSourceLimitToFamily_nsmul
    (N : Subgroup (FreeGroup X)) (m : ℕ)
    (x : FoxAlgebraicStagePrimePowerSourceLimit (ℓ := ℓ) (X := X) N) :
    foxAlgebraicStagePrimePowerSourceLimitToFamily (ℓ := ℓ) (X := X) N (m • x) =
      m • foxAlgebraicStagePrimePowerSourceLimitToFamily (ℓ := ℓ) (X := X) N x

theorem

foxAlgebraicStagePrimePowerSourceLimitToFamily_zsmul

L198 ↗

FoxDifferential.foxAlgebraicStagePrimePowerSourceLimitToFamily_zsmul

Documentation

The source-limit family map preserves integer scalar multiplication.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u v
variable (ℓ : ℕ)
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
omit [DecidableEq X] in

Lean source · statement

theorem foxAlgebraicStagePrimePowerSourceLimitToFamily_zsmul
    (N : Subgroup (FreeGroup X)) (m : ℤ)
    (x : FoxAlgebraicStagePrimePowerSourceLimit (ℓ := ℓ) (X := X) N) :
    foxAlgebraicStagePrimePowerSourceLimitToFamily (ℓ := ℓ) (X := X) N (m • x) =
      m • foxAlgebraicStagePrimePowerSourceLimitToFamily (ℓ := ℓ) (X := X) N x

instance

instAddCommGroupFoxAlgebraicStagePrimePowerSourceLimit

L210 ↗

FoxDifferential.instAddCommGroupFoxAlgebraicStagePrimePowerSourceLimit

Documentation

The prime-power source limit inherits an additive commutative group structure from its injective map into the family of source stages.

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 v
variable (ℓ : ℕ)
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

Lean source · statement

instance instAddCommGroupFoxAlgebraicStagePrimePowerSourceLimit
    (N : Subgroup (FreeGroup X)) :
    AddCommGroup (FoxAlgebraicStagePrimePowerSourceLimit (ℓ := ℓ) (X := X) N)

instance

instZeroFoxAlgebraicStagePrimePowerTargetLimit

L229 ↗

FoxDifferential.instZeroFoxAlgebraicStagePrimePowerTargetLimit

Documentation

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

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 v
variable (ℓ : ℕ)
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

Lean source · full declaration

instance instZeroFoxAlgebraicStagePrimePowerTargetLimit
    (N : Subgroup (FreeGroup X)) [N.Normal] :
    Zero (FoxAlgebraicStagePrimePowerTargetLimit (ℓ := ℓ) (X := X) N) where
  zero := ⟨fun a => (0 : foxAlgebraicStagePrimePowerTargetGroupAlgebra (ℓ := ℓ) (X := X) N a),
    by
      intro a b hab
      change foxAlgebraicStagePrimePowerTargetTransition (ℓ := ℓ) (X := X) N hab
          (0 : foxAlgebraicStagePrimePowerTargetGroupAlgebra (ℓ := ℓ) (X := X) N b) = 0
      exact map_zero _⟩

instance

instAddFoxAlgebraicStagePrimePowerTargetLimit

L243 ↗

FoxDifferential.instAddFoxAlgebraicStagePrimePowerTargetLimit

Documentation

Addition in the finite Fox prime-power target limit is defined coordinatewise through finite stages.

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 v
variable (ℓ : ℕ)
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

Lean source · full declaration

instance instAddFoxAlgebraicStagePrimePowerTargetLimit
    (N : Subgroup (FreeGroup X)) [N.Normal] :
    Add (FoxAlgebraicStagePrimePowerTargetLimit (ℓ := ℓ) (X := X) N) where
  add x y := ⟨fun a =>
      (show foxAlgebraicStagePrimePowerTargetGroupAlgebra (ℓ := ℓ) (X := X) N a from x.1 a) +
        (show foxAlgebraicStagePrimePowerTargetGroupAlgebra (ℓ := ℓ) (X := X) N a from y.1 a),
    by
      intro a b hab
      change foxAlgebraicStagePrimePowerTargetTransition (ℓ := ℓ) (X := X) N hab
          ((show foxAlgebraicStagePrimePowerTargetGroupAlgebra (ℓ := ℓ) (X := X) N b from x.1 b) +
            (show foxAlgebraicStagePrimePowerTargetGroupAlgebra (ℓ := ℓ) (X := X) N b from y.1 b)) =
        (show foxAlgebraicStagePrimePowerTargetGroupAlgebra (ℓ := ℓ) (X := X) N a from x.1 a) +
          (show foxAlgebraicStagePrimePowerTargetGroupAlgebra (ℓ := ℓ) (X := X) N a from y.1 a)
      rw [map_add]
      exact congrArg₂ HAdd.hAdd (x.2 a b hab) (y.2 a b hab)⟩

instance

instNegFoxAlgebraicStagePrimePowerTargetLimit

L263 ↗

FoxDifferential.instNegFoxAlgebraicStagePrimePowerTargetLimit

Documentation

Negation on the prime-power target inverse limit is defined coordinatewise through finite-stage target negations.

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 v
variable (ℓ : ℕ)
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

Lean source · full declaration

instance instNegFoxAlgebraicStagePrimePowerTargetLimit
    (N : Subgroup (FreeGroup X)) [N.Normal] :
    Neg (FoxAlgebraicStagePrimePowerTargetLimit (ℓ := ℓ) (X := X) N) where
  neg x := ⟨fun a =>
      -(show foxAlgebraicStagePrimePowerTargetGroupAlgebra (ℓ := ℓ) (X := X) N a from x.1 a),
    by
      intro a b hab
      change foxAlgebraicStagePrimePowerTargetTransition (ℓ := ℓ) (X := X) N hab
          (-(show foxAlgebraicStagePrimePowerTargetGroupAlgebra (ℓ := ℓ) (X := X) N b from x.1 b)) =
        -(show foxAlgebraicStagePrimePowerTargetGroupAlgebra (ℓ := ℓ) (X := X) N a from x.1 a)
      rw [map_neg]
      exact congrArg Neg.neg (x.2 a b hab)⟩

instance

instSubFoxAlgebraicStagePrimePowerTargetLimit

L280 ↗

FoxDifferential.instSubFoxAlgebraicStagePrimePowerTargetLimit

Documentation

Subtraction on the prime-power target inverse limit is defined coordinatewise through finite-stage target subtractions.

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 v
variable (ℓ : ℕ)
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

Lean source · full declaration

instance instSubFoxAlgebraicStagePrimePowerTargetLimit
    (N : Subgroup (FreeGroup X)) [N.Normal] :
    Sub (FoxAlgebraicStagePrimePowerTargetLimit (ℓ := ℓ) (X := X) N) where
  sub x y := ⟨fun a =>
      (show foxAlgebraicStagePrimePowerTargetGroupAlgebra (ℓ := ℓ) (X := X) N a from x.1 a) -
        (show foxAlgebraicStagePrimePowerTargetGroupAlgebra (ℓ := ℓ) (X := X) N a from y.1 a),
    by
      intro a b hab
      change foxAlgebraicStagePrimePowerTargetTransition (ℓ := ℓ) (X := X) N hab
          ((show foxAlgebraicStagePrimePowerTargetGroupAlgebra (ℓ := ℓ) (X := X) N b from x.1 b) -
            (show foxAlgebraicStagePrimePowerTargetGroupAlgebra (ℓ := ℓ) (X := X) N b from y.1 b)) =
        (show foxAlgebraicStagePrimePowerTargetGroupAlgebra (ℓ := ℓ) (X := X) N a from x.1 a) -
          (show foxAlgebraicStagePrimePowerTargetGroupAlgebra (ℓ := ℓ) (X := X) N a from y.1 a)
      rw [map_sub]
      exact congrArg₂ HSub.hSub (x.2 a b hab) (y.2 a b hab)⟩

instance

instSMulNatFoxAlgebraicStagePrimePowerTargetLimit

L300 ↗

FoxDifferential.instSMulNatFoxAlgebraicStagePrimePowerTargetLimit

Documentation

The prime-power target inverse limit carries natural-number scalar multiplication coordinatewise.

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 v
variable (ℓ : ℕ)
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

Lean source · full declaration

instance instSMulNatFoxAlgebraicStagePrimePowerTargetLimit
    (N : Subgroup (FreeGroup X)) [N.Normal] :
    SMul ℕ (FoxAlgebraicStagePrimePowerTargetLimit (ℓ := ℓ) (X := X) N) where
  smul m x := ⟨fun a =>
      m • (show foxAlgebraicStagePrimePowerTargetGroupAlgebra (ℓ := ℓ) (X := X) N a from x.1 a),
    by
      intro a b hab
      change foxAlgebraicStagePrimePowerTargetTransition (ℓ := ℓ) (X := X) N hab
          (m • (show foxAlgebraicStagePrimePowerTargetGroupAlgebra (ℓ := ℓ) (X := X) N b from
              x.1 b)) =
        m • (show foxAlgebraicStagePrimePowerTargetGroupAlgebra (ℓ := ℓ) (X := X) N a from x.1 a)
      rw [map_nsmul]
      exact congrArg (m • ·) (x.2 a b hab)⟩

instance

instSMulIntFoxAlgebraicStagePrimePowerTargetLimit

L315 ↗

FoxDifferential.instSMulIntFoxAlgebraicStagePrimePowerTargetLimit

Documentation

The prime-power target inverse limit carries integer scalar multiplication coordinatewise.

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 v
variable (ℓ : ℕ)
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

Lean source · full declaration

instance instSMulIntFoxAlgebraicStagePrimePowerTargetLimit
    (N : Subgroup (FreeGroup X)) [N.Normal] :
    SMul ℤ (FoxAlgebraicStagePrimePowerTargetLimit (ℓ := ℓ) (X := X) N) where
  smul m x := ⟨fun a =>
      m • (show foxAlgebraicStagePrimePowerTargetGroupAlgebra (ℓ := ℓ) (X := X) N a from x.1 a),
    by
      intro a b hab
      change foxAlgebraicStagePrimePowerTargetTransition (ℓ := ℓ) (X := X) N hab
          (m • (show foxAlgebraicStagePrimePowerTargetGroupAlgebra (ℓ := ℓ) (X := X) N b from
              x.1 b)) =
        m • (show foxAlgebraicStagePrimePowerTargetGroupAlgebra (ℓ := ℓ) (X := X) N a from x.1 a)
      rw [map_zsmul]
      exact congrArg (m • ·) (x.2 a b hab)⟩

theorem

foxAlgebraicStagePrimePowerTargetLimitToFamily_zero

L331 ↗

FoxDifferential.foxAlgebraicStagePrimePowerTargetLimitToFamily_zero

Documentation

The target-limit family of zero is the zero family.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u v
variable (ℓ : ℕ)
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
omit [DecidableEq X] in

Lean source · statement

theorem foxAlgebraicStagePrimePowerTargetLimitToFamily_zero
    (N : Subgroup (FreeGroup X)) [N.Normal] :
    foxAlgebraicStagePrimePowerTargetLimitToFamily (ℓ := ℓ) (X := X) N 0 = 0

theorem

foxAlgebraicStagePrimePowerTargetLimitToFamily_add

L339 ↗

FoxDifferential.foxAlgebraicStagePrimePowerTargetLimitToFamily_add

Documentation

The target-limit family map preserves addition.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u v
variable (ℓ : ℕ)
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
omit [DecidableEq X] in

Lean source · statement

theorem foxAlgebraicStagePrimePowerTargetLimitToFamily_add
    (N : Subgroup (FreeGroup X)) [N.Normal]
    (x y : FoxAlgebraicStagePrimePowerTargetLimit (ℓ := ℓ) (X := X) N) :
    foxAlgebraicStagePrimePowerTargetLimitToFamily (ℓ := ℓ) (X := X) N (x + y) =
      foxAlgebraicStagePrimePowerTargetLimitToFamily (ℓ := ℓ) (X := X) N x +
        foxAlgebraicStagePrimePowerTargetLimitToFamily (ℓ := ℓ) (X := X) N y

theorem

foxAlgebraicStagePrimePowerTargetLimitToFamily_neg

L350 ↗

FoxDifferential.foxAlgebraicStagePrimePowerTargetLimitToFamily_neg

Documentation

The target-limit family map preserves negation.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u v
variable (ℓ : ℕ)
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
omit [DecidableEq X] in

Lean source · statement

theorem foxAlgebraicStagePrimePowerTargetLimitToFamily_neg
    (N : Subgroup (FreeGroup X)) [N.Normal]
    (x : FoxAlgebraicStagePrimePowerTargetLimit (ℓ := ℓ) (X := X) N) :
    foxAlgebraicStagePrimePowerTargetLimitToFamily (ℓ := ℓ) (X := X) N (-x) =
      -foxAlgebraicStagePrimePowerTargetLimitToFamily (ℓ := ℓ) (X := X) N x

theorem

foxAlgebraicStagePrimePowerTargetLimitToFamily_sub

L360 ↗

FoxDifferential.foxAlgebraicStagePrimePowerTargetLimitToFamily_sub

Documentation

The target-limit family map preserves subtraction.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u v
variable (ℓ : ℕ)
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
omit [DecidableEq X] in

Lean source · statement

theorem foxAlgebraicStagePrimePowerTargetLimitToFamily_sub
    (N : Subgroup (FreeGroup X)) [N.Normal]
    (x y : FoxAlgebraicStagePrimePowerTargetLimit (ℓ := ℓ) (X := X) N) :
    foxAlgebraicStagePrimePowerTargetLimitToFamily (ℓ := ℓ) (X := X) N (x - y) =
      foxAlgebraicStagePrimePowerTargetLimitToFamily (ℓ := ℓ) (X := X) N x -
        foxAlgebraicStagePrimePowerTargetLimitToFamily (ℓ := ℓ) (X := X) N y

theorem

foxAlgebraicStagePrimePowerTargetLimitToFamily_nsmul

L371 ↗

FoxDifferential.foxAlgebraicStagePrimePowerTargetLimitToFamily_nsmul

Documentation

The target-limit family map preserves natural-number scalar multiplication.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u v
variable (ℓ : ℕ)
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
omit [DecidableEq X] in

Lean source · statement

theorem foxAlgebraicStagePrimePowerTargetLimitToFamily_nsmul
    (N : Subgroup (FreeGroup X)) [N.Normal] (m : ℕ)
    (x : FoxAlgebraicStagePrimePowerTargetLimit (ℓ := ℓ) (X := X) N) :
    foxAlgebraicStagePrimePowerTargetLimitToFamily (ℓ := ℓ) (X := X) N (m • x) =
      m • foxAlgebraicStagePrimePowerTargetLimitToFamily (ℓ := ℓ) (X := X) N x

theorem

foxAlgebraicStagePrimePowerTargetLimitToFamily_zsmul

L381 ↗

FoxDifferential.foxAlgebraicStagePrimePowerTargetLimitToFamily_zsmul

Documentation

The target-limit family map preserves integer scalar multiplication.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u v
variable (ℓ : ℕ)
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
omit [DecidableEq X] in

Lean source · statement

theorem foxAlgebraicStagePrimePowerTargetLimitToFamily_zsmul
    (N : Subgroup (FreeGroup X)) [N.Normal] (m : ℤ)
    (x : FoxAlgebraicStagePrimePowerTargetLimit (ℓ := ℓ) (X := X) N) :
    foxAlgebraicStagePrimePowerTargetLimitToFamily (ℓ := ℓ) (X := X) N (m • x) =
      m • foxAlgebraicStagePrimePowerTargetLimitToFamily (ℓ := ℓ) (X := X) N x

instance

instAddCommGroupFoxAlgebraicStagePrimePowerTargetLimit

L393 ↗

FoxDifferential.instAddCommGroupFoxAlgebraicStagePrimePowerTargetLimit

Documentation

The prime-power target limit inherits an additive commutative group structure from its injective map into the family of target stages.

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 v
variable (ℓ : ℕ)
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

Lean source · statement

instance instAddCommGroupFoxAlgebraicStagePrimePowerTargetLimit
    (N : Subgroup (FreeGroup X)) [N.Normal] :
    AddCommGroup (FoxAlgebraicStagePrimePowerTargetLimit (ℓ := ℓ) (X := X) N)

Module documentation

Fox differential: prime power — system — limit — add comm group

Declarations