NYLL
Module

Mul.lean

Nyll.ProCGroups.FoxDifferential.Completed.FiniteStage.PrimePower.System.Limit.Mul
8 declarations indexed from sourceView source ↗

Module documentation

Fox differential: prime power — system — limit — mul

The principal declarations in this module are:

  • foxAlgebraicStagePrimePowerSourceLimitToFamily_one

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

  • foxAlgebraicStagePrimePowerSourceLimitToFamily_mul

The source-limit family map preserves multiplication.

  • foxAlgebraicStagePrimePowerTargetLimitToFamily_one

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

  • foxAlgebraicStagePrimePowerTargetLimitToFamily_mul

The target-limit family map preserves multiplication.

Imports1
Imported by2

Declarations

instance

instOneFoxAlgebraicStagePrimePowerSourceLimit

L43 ↗
FoxDifferential.instOneFoxAlgebraicStagePrimePowerSourceLimit
Documentation

The prime-power finite Fox source inverse limit has a coordinatewise multiplicative identity.

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 instOneFoxAlgebraicStagePrimePowerSourceLimit
    (N : Subgroup (FreeGroup X)) :
    One (FoxAlgebraicStagePrimePowerSourceLimit (ℓ := ℓ) (X := X) N) where
  one := ⟨fun a => (1 : foxAlgebraicStagePrimePowerSourceGroupAlgebra (ℓ := ℓ) (X := X) N a),
    by
      intro a b hab
      change foxAlgebraicStagePrimePowerSourceTransition (ℓ := ℓ) (X := X) N hab
          (1 : foxAlgebraicStagePrimePowerSourceGroupAlgebra (ℓ := ℓ) (X := X) N b) = 1
      exact map_one _⟩
instance

instMulFoxAlgebraicStagePrimePowerSourceLimit

L57 ↗
FoxDifferential.instMulFoxAlgebraicStagePrimePowerSourceLimit
Documentation

Multiplication on the prime-power source inverse limit is defined coordinatewise through finite-stage group-algebra products.

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 instMulFoxAlgebraicStagePrimePowerSourceLimit
    (N : Subgroup (FreeGroup X)) :
    Mul (FoxAlgebraicStagePrimePowerSourceLimit (ℓ := ℓ) (X := X) N) where
  mul 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_mul]
      exact congrArg₂ HMul.hMul (x.2 a b hab) (y.2 a b hab)⟩
instance

instOneFoxAlgebraicStagePrimePowerTargetLimit

L74 ↗
FoxDifferential.instOneFoxAlgebraicStagePrimePowerTargetLimit
Documentation

The prime-power finite Fox target inverse limit has a coordinatewise multiplicative identity.

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 instOneFoxAlgebraicStagePrimePowerTargetLimit
    (N : Subgroup (FreeGroup X)) [N.Normal] :
    One (FoxAlgebraicStagePrimePowerTargetLimit (ℓ := ℓ) (X := X) N) where
  one := ⟨fun a => (1 : foxAlgebraicStagePrimePowerTargetGroupAlgebra (ℓ := ℓ) (X := X) N a),
    by
      intro a b hab
      change foxAlgebraicStagePrimePowerTargetTransition (ℓ := ℓ) (X := X) N hab
          (1 : foxAlgebraicStagePrimePowerTargetGroupAlgebra (ℓ := ℓ) (X := X) N b) = 1
      exact map_one _⟩
instance

instMulFoxAlgebraicStagePrimePowerTargetLimit

L88 ↗
FoxDifferential.instMulFoxAlgebraicStagePrimePowerTargetLimit
Documentation

Multiplication on the prime-power target inverse limit is defined coordinatewise through finite-stage group-algebra products.

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 instMulFoxAlgebraicStagePrimePowerTargetLimit
    (N : Subgroup (FreeGroup X)) [N.Normal] :
    Mul (FoxAlgebraicStagePrimePowerTargetLimit (ℓ := ℓ) (X := X) N) where
  mul 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_mul]
      exact congrArg₂ HMul.hMul (x.2 a b hab) (y.2 a b hab)⟩
theorem

foxAlgebraicStagePrimePowerSourceLimitToFamily_one

L107 ↗
FoxDifferential.foxAlgebraicStagePrimePowerSourceLimitToFamily_one
Documentation

The source-limit family of one is the one 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_one
    (N : Subgroup (FreeGroup X)) :
    foxAlgebraicStagePrimePowerSourceLimitToFamily (ℓ := ℓ) (X := X) N 1 = 1
theorem

foxAlgebraicStagePrimePowerSourceLimitToFamily_mul

L116 ↗
FoxDifferential.foxAlgebraicStagePrimePowerSourceLimitToFamily_mul
Documentation

The source-limit family map preserves 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_mul
    (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

foxAlgebraicStagePrimePowerTargetLimitToFamily_one

L128 ↗
FoxDifferential.foxAlgebraicStagePrimePowerTargetLimitToFamily_one
Documentation

The target-limit family of one is the one 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_one
    (N : Subgroup (FreeGroup X)) [N.Normal] :
    foxAlgebraicStagePrimePowerTargetLimitToFamily (ℓ := ℓ) (X := X) N 1 = 1
theorem

foxAlgebraicStagePrimePowerTargetLimitToFamily_mul

L137 ↗
FoxDifferential.foxAlgebraicStagePrimePowerTargetLimitToFamily_mul
Documentation

The target-limit family map preserves 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_mul
    (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

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.