Module

Topology.lean

Nyll.ProCGroups.FoxDifferential.Completed.Continuous.Topology

55 declarations indexed from sourceView source ↗

Module documentation

Fox differential: completed — continuous — topology

The principal declarations in this module are:

freeProCZCCompletedFoxBoundary

Source-shaped completed Fox boundary map for a finite generating set. It evaluates a vector of completed Fox coefficients against the generator boundaries \([\varphi(x)]-1\).

zcCompletedFoxSemidirectHomeomorphProd

The completed Fox semidirect target is homeomorphic to its product of components.

continuous_foxBoundaryMap

A finite Fox boundary map is continuous over any topological ring.

continuous_zcCompletedGroupAlgebraProjection

A finite stage projection from \(\mathbb{Z}_C\llbracket G\rrbracket\) is continuous.

Imports2

Imported by7

theorem

continuous_foxBoundaryMap

L42 ↗

FoxDifferential.continuous_foxBoundaryMap

Documentation

A finite Fox boundary map is continuous over any topological ring.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.Completion
open scoped BigOperators
universe u v
section BoundaryMapContinuity
variable {R : Type u} [Ring R] [TopologicalSpace R] [ContinuousAdd R] [ContinuousMul R]
variable {X : Type v} [Fintype X]

Lean source · statement

theorem continuous_foxBoundaryMap (generatorBoundary : X → R) :
    Continuous (foxBoundaryMap generatorBoundary)

instance

instTopologicalSpaceZCCompletedGroupAlgebraStage

L55 ↗

FoxDifferential.instTopologicalSpaceZCCompletedGroupAlgebraStage

Documentation

Each finite-stage \(\mathbb{Z}_C\)-completed group algebra carries its finite-stage topology.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.Completion
open scoped BigOperators
universe u v
section CompletedGroupAlgebraTopology
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

instance instTopologicalSpaceZCCompletedGroupAlgebraStage
    (i : ZCCompletedGroupAlgebraIndex C G) :
    TopologicalSpace (ZCCompletedGroupAlgebraStage C G i)

instance

instDiscreteTopologyZCCompletedGroupAlgebraStage

L61 ↗

FoxDifferential.instDiscreteTopologyZCCompletedGroupAlgebraStage

Documentation

Each finite-stage \(\mathbb{Z}_C\)-completed group algebra carries the discrete topology.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.Completion
open scoped BigOperators
universe u v
section CompletedGroupAlgebraTopology
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

instance instDiscreteTopologyZCCompletedGroupAlgebraStage
    (i : ZCCompletedGroupAlgebraIndex C G) :
    DiscreteTopology (ZCCompletedGroupAlgebraStage C G i)

instance

instCompactSpaceZCCompletedGroupAlgebraStage

L67 ↗

FoxDifferential.instCompactSpaceZCCompletedGroupAlgebraStage

Documentation

Each finite-stage \(\mathbb{Z}_C\)-completed group algebra is compact.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.Completion
open scoped BigOperators
universe u v
section CompletedGroupAlgebraTopology
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

instance instCompactSpaceZCCompletedGroupAlgebraStage
    (i : ZCCompletedGroupAlgebraIndex C G) :
    CompactSpace (ZCCompletedGroupAlgebraStage C G i)

instance

instT2SpaceZCCompletedGroupAlgebraStage

L79 ↗

FoxDifferential.instT2SpaceZCCompletedGroupAlgebraStage

Documentation

Each finite-stage \(\mathbb{Z}_C\)-completed group algebra is a \(T_2\) space.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.Completion
open scoped BigOperators
universe u v
section CompletedGroupAlgebraTopology
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

instance instT2SpaceZCCompletedGroupAlgebraStage
    (i : ZCCompletedGroupAlgebraIndex C G) :
    T2Space (ZCCompletedGroupAlgebraStage C G i)

instance

instTotallyDisconnectedSpaceZCCompletedGroupAlgebraStage

L85 ↗

FoxDifferential.instTotallyDisconnectedSpaceZCCompletedGroupAlgebraStage

Documentation

Each finite-stage \(\mathbb{Z}_C\)-completed group algebra is totally disconnected.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.Completion
open scoped BigOperators
universe u v
section CompletedGroupAlgebraTopology
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

instance instTotallyDisconnectedSpaceZCCompletedGroupAlgebraStage
    (i : ZCCompletedGroupAlgebraIndex C G) :
    TotallyDisconnectedSpace (ZCCompletedGroupAlgebraStage C G i)

instance

instCompactSpaceZCCompletedGroupAlgebra

L91 ↗

FoxDifferential.instCompactSpaceZCCompletedGroupAlgebra

Documentation

The completed \(\mathbb{Z}_C\)-group algebra is compact.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.Completion
open scoped BigOperators
universe u v
section CompletedGroupAlgebraTopology
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

instance instCompactSpaceZCCompletedGroupAlgebra :
    CompactSpace (ZCCompletedGroupAlgebra C G)

instance

instT2SpaceZCCompletedGroupAlgebra

L112 ↗

FoxDifferential.instT2SpaceZCCompletedGroupAlgebra

Documentation

The completed \(\mathbb{Z}_C\)-group algebra is a \(T_2\) space.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.Completion
open scoped BigOperators
universe u v
section CompletedGroupAlgebraTopology
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

instance instT2SpaceZCCompletedGroupAlgebra :
    T2Space (ZCCompletedGroupAlgebra C G)

theorem

continuous_zcCompletedGroupAlgebraProjection

L125 ↗

FoxDifferential.continuous_zcCompletedGroupAlgebraProjection

Documentation

A finite stage projection from \(\mathbb{Z}_C\llbracket G\rrbracket\) is continuous.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.Completion
open scoped BigOperators
universe u v
section CompletedGroupAlgebraTopology
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

theorem continuous_zcCompletedGroupAlgebraProjection
    (i : ZCCompletedGroupAlgebraIndex C G) :
    Continuous (zcCompletedGroupAlgebraProjection C G i)

theorem

continuous_zcCompletedGroupAlgebraProjectionRingHom

L134 ↗

FoxDifferential.continuous_zcCompletedGroupAlgebraProjectionRingHom

Documentation

A finite stage projection from \(\mathbb{Z}_C\llbracket G\rrbracket\), regarded as a ring homomorphism, is continuous.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.Completion
open scoped BigOperators
universe u v
section CompletedGroupAlgebraTopology
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

theorem continuous_zcCompletedGroupAlgebraProjectionRingHom
    (i : ZCCompletedGroupAlgebraIndex C G) :
    Continuous (zcCompletedGroupAlgebraProjectionRingHom C G i)

instance

instTotallyDisconnectedSpaceZCCompletedGroupAlgebra

L140 ↗

FoxDifferential.instTotallyDisconnectedSpaceZCCompletedGroupAlgebra

Documentation

The completed \(\mathbb{Z}_C\)-group algebra is totally disconnected.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.Completion
open scoped BigOperators
universe u v
section CompletedGroupAlgebraTopology
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

instance instTotallyDisconnectedSpaceZCCompletedGroupAlgebra :
    TotallyDisconnectedSpace (ZCCompletedGroupAlgebra C G)

instance

instContinuousAddZCCompletedGroupAlgebra

L156 ↗

FoxDifferential.instContinuousAddZCCompletedGroupAlgebra

Documentation

Addition on \(\mathbb{Z}_C\llbracket H\rrbracket\) is continuous for the inverse-limit topology.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.Completion
open scoped BigOperators
universe u v
section CompletedGroupAlgebraTopology
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · full declaration

instance instContinuousAddZCCompletedGroupAlgebra :
    ContinuousAdd (ZCCompletedGroupAlgebra C G) where
  continuous_add := by
    have hval : Continuous (fun p : ZCCompletedGroupAlgebra C G ×
        ZCCompletedGroupAlgebra C G =>
        ((p.1 + p.2 : ZCCompletedGroupAlgebra C G) :
          (i : ZCCompletedGroupAlgebraIndex C G) → ZCCompletedGroupAlgebraStage C G i)) := by
      exact continuous_pi fun i =>
        (continuous_of_discreteTopology :
          Continuous (fun q : ZCCompletedGroupAlgebraStage C G i ×
              ZCCompletedGroupAlgebraStage C G i => q.1 + q.2)).comp
            (((continuous_apply i).comp (continuous_subtype_val.comp continuous_fst)).prodMk
              ((continuous_apply i).comp (continuous_subtype_val.comp continuous_snd)))
    convert
      (Continuous.subtype_mk (p := ZCCompletedGroupAlgebraCompatible C G) hval
        (fun p => (p.1 + p.2 : ZCCompletedGroupAlgebra C G).property)) using 1

instance

instContinuousNegZCCompletedGroupAlgebra

L174 ↗

FoxDifferential.instContinuousNegZCCompletedGroupAlgebra

Documentation

Negation on the completed group algebra is continuous for the inverse-limit topology.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.Completion
open scoped BigOperators
universe u v
section CompletedGroupAlgebraTopology
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · full declaration

instance instContinuousNegZCCompletedGroupAlgebra :
    ContinuousNeg (ZCCompletedGroupAlgebra C G) where
  continuous_neg := by
    change Continuous (fun x : ZCCompletedGroupAlgebra C G => -x)
    have hval : Continuous (fun x : ZCCompletedGroupAlgebra C G =>
        ((-x : ZCCompletedGroupAlgebra C G) :
          (i : ZCCompletedGroupAlgebraIndex C G) → ZCCompletedGroupAlgebraStage C G i)) := by
      exact continuous_pi fun i =>
        (continuous_of_discreteTopology :
          Continuous (fun y : ZCCompletedGroupAlgebraStage C G i => -y)).comp
          ((continuous_apply i).comp continuous_subtype_val)
    convert
      (Continuous.subtype_mk (p := ZCCompletedGroupAlgebraCompatible C G) hval
        (fun x => (-x : ZCCompletedGroupAlgebra C G).property)) using 1

instance

instIsTopologicalAddGroupZCCompletedGroupAlgebra

L190 ↗

FoxDifferential.instIsTopologicalAddGroupZCCompletedGroupAlgebra

Documentation

The completed group algebra has addition defined coordinatewise on compatible families.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.Completion
open scoped BigOperators
universe u v
section CompletedGroupAlgebraTopology
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · full declaration

instance instIsTopologicalAddGroupZCCompletedGroupAlgebra :
    IsTopologicalAddGroup (ZCCompletedGroupAlgebra C G) where
  continuous_add := continuous_add
  continuous_neg := continuous_neg

instance

instContinuousMulZCCompletedGroupAlgebra

L196 ↗

FoxDifferential.instContinuousMulZCCompletedGroupAlgebra

Documentation

Multiplication on the completed group algebra is continuous for the inverse-limit topology.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.Completion
open scoped BigOperators
universe u v
section CompletedGroupAlgebraTopology
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · full declaration

instance instContinuousMulZCCompletedGroupAlgebra :
    ContinuousMul (ZCCompletedGroupAlgebra C G) where
  continuous_mul := by
    have hval : Continuous (fun p : ZCCompletedGroupAlgebra C G ×
        ZCCompletedGroupAlgebra C G =>
        ((p.1 * p.2 : ZCCompletedGroupAlgebra C G) :
          (i : ZCCompletedGroupAlgebraIndex C G) → ZCCompletedGroupAlgebraStage C G i)) := by
      exact continuous_pi fun i =>
        (continuous_of_discreteTopology :
          Continuous (fun q : ZCCompletedGroupAlgebraStage C G i ×
              ZCCompletedGroupAlgebraStage C G i => q.1 * q.2)).comp
            (((continuous_apply i).comp (continuous_subtype_val.comp continuous_fst)).prodMk
              ((continuous_apply i).comp (continuous_subtype_val.comp continuous_snd)))
    convert
      (Continuous.subtype_mk (p := ZCCompletedGroupAlgebraCompatible C G) hval
        (fun p => (p.1 * p.2 : ZCCompletedGroupAlgebra C G).property)) using 1

instance

instIsTopologicalRingZCCompletedGroupAlgebra

L214 ↗

FoxDifferential.instIsTopologicalRingZCCompletedGroupAlgebra

Documentation

The completed group algebra inherits a ring structure from the compatible finite-stage rings.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.Completion
open scoped BigOperators
universe u v
section CompletedGroupAlgebraTopology
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · full declaration

instance instIsTopologicalRingZCCompletedGroupAlgebra :
    IsTopologicalRing (ZCCompletedGroupAlgebra C G) where
  continuous_add := continuous_add
  continuous_mul := continuous_mul
  continuous_neg := continuous_neg

instance

instContinuousSMulZCCompletedGroupAlgebraSelf

L221 ↗

FoxDifferential.instContinuousSMulZCCompletedGroupAlgebraSelf

Documentation

Scalar multiplication is continuous for the relevant inverse-limit topology.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.Completion
open scoped BigOperators
universe u v
section CompletedGroupAlgebraTopology
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

instance instContinuousSMulZCCompletedGroupAlgebraSelf :
    ContinuousSMul (ZCCompletedGroupAlgebra C G) (ZCCompletedGroupAlgebra C G)

theorem

continuous_zcCompletedGroupAlgebra_smul

L226 ↗

FoxDifferential.continuous_zcCompletedGroupAlgebra_smul

Documentation

The scalar action map on the completed group algebra is continuous.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.Completion
open scoped BigOperators
universe u v
section CompletedGroupAlgebraTopology
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · full declaration

theorem continuous_zcCompletedGroupAlgebra_smul :
    Continuous (fun p : ZCCompletedGroupAlgebra C G × ZCCompletedGroupAlgebra C G =>
      p.1 • p.2) :=
  continuous_smul

theorem

continuous_zcGroupLike

L232 ↗

FoxDifferential.continuous_zcGroupLike

Documentation

The completed group-like map \(G \to \mathbb{Z}_C\llbracket G\rrbracket\) is continuous.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.Completion
open scoped BigOperators
universe u v
section CompletedGroupAlgebraTopology
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

theorem continuous_zcGroupLike : Continuous (zcGroupLike C G)

theorem

continuous_zcCompletedGroupAlgebraAugmentation

L255 ↗

FoxDifferential.continuous_zcCompletedGroupAlgebraAugmentation

Documentation

The completed augmentation \(\mathbb{Z}_C\llbracket G\rrbracket \to \mathbb{Z}_C\) is continuous in the inverse-limit topology.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.Completion
open scoped BigOperators
universe u v
section CompletedGroupAlgebraTopology
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

theorem continuous_zcCompletedGroupAlgebraAugmentation
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C] :
    Continuous (zcCompletedGroupAlgebraAugmentation C G)

theorem

isClosed_zcCompletedGroupAlgebraAugmentationIdeal

L275 ↗

FoxDifferential.isClosed_zcCompletedGroupAlgebraAugmentationIdeal

Documentation

The completed augmentation ideal is closed in \(\mathbb{Z}_C\llbracket G\rrbracket\).

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.Completion
open scoped BigOperators
universe u v
section CompletedGroupAlgebraTopology
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

theorem isClosed_zcCompletedGroupAlgebraAugmentationIdeal
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C] :
    IsClosed
      ((zcCompletedGroupAlgebraAugmentationIdeal C G :
        Ideal (ZCCompletedGroupAlgebra C G)) : Set (ZCCompletedGroupAlgebra C G))

instance

instCompactSpaceZCCompletedGroupAlgebraAugmentationIdeal

L285 ↗

FoxDifferential.instCompactSpaceZCCompletedGroupAlgebraAugmentationIdeal

Documentation

The completed \(\mathbb{Z}_C\)-group algebra augmentation ideal is compact.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.Completion
open scoped BigOperators
universe u v
section CompletedGroupAlgebraTopology
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

instance instCompactSpaceZCCompletedGroupAlgebraAugmentationIdeal
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C] :
    CompactSpace (ZCCompletedGroupAlgebraAugmentationIdeal C G)

instance

instT2SpaceZCCompletedGroupAlgebraAugmentationIdeal

L293 ↗

FoxDifferential.instT2SpaceZCCompletedGroupAlgebraAugmentationIdeal

Documentation

The completed \(\mathbb{Z}_C\)-group algebra augmentation ideal is a \(T_2\) space.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.Completion
open scoped BigOperators
universe u v
section CompletedGroupAlgebraTopology
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

instance instT2SpaceZCCompletedGroupAlgebraAugmentationIdeal
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C] :
    T2Space (ZCCompletedGroupAlgebraAugmentationIdeal C G)

theorem

continuous_zcCompletedGroupAlgebraBoundary

L304 ↗

FoxDifferential.continuous_zcCompletedGroupAlgebraBoundary

Documentation

The completed group-algebra boundary \(a \mapsto [\psi(a)] - 1\) is continuous whenever \(\psi\) is continuous.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.Completion
open scoped BigOperators
universe u v
section CompletedGroupAlgebraTopology
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {A : Type v} [Group A] [TopologicalSpace A]

Lean source · statement

theorem continuous_zcCompletedGroupAlgebraBoundary
    (ψ : A →* G) (hψ : Continuous ψ) :
    Continuous (zcCompletedGroupAlgebraBoundary C ψ)

theorem

continuous_zcFreeGroupFoxBoundary

L315 ↗

FoxDifferential.continuous_zcFreeGroupFoxBoundary

Documentation

The completed \(\mathbb{Z}_C\llbracket G\rrbracket\) Fox boundary/Euler map is continuous.

Source context 12 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.Completion
open scoped BigOperators
universe u v
section CompletedGroupAlgebraTopology
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {A : Type v} [Group A] [TopologicalSpace A]
variable {X : Type v} [Fintype X] [DecidableEq X]
omit [DecidableEq X] in

Lean source · statement

theorem continuous_zcFreeGroupFoxBoundary (ψ : FreeGroup X →* G) :
    Continuous (zcFreeGroupFoxBoundary C ψ)

def

freeProCZCCompletedFoxBoundary

L333 ↗

FoxDifferential.freeProCZCCompletedFoxBoundary

Documentation

Source-shaped completed Fox boundary map for a finite generating set. It evaluates a vector of completed Fox coefficients against the generator boundaries \([\varphi(x)]-1\).

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.Completion
open scoped BigOperators
universe u v
section CompletedSourceBoundary
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {X H : Type u} [Fintype X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

def freeProCZCCompletedFoxBoundary (φ : X → H) :
    ZCFreeFoxCoordinates C (X := X) (H := H) →ₗ[ZCCompletedGroupAlgebra C H]
      ZCCompletedGroupAlgebra C H

theorem

freeProCZCCompletedFoxBoundary_apply

L343 ↗

FoxDifferential.freeProCZCCompletedFoxBoundary_apply

Documentation

The boundary map is evaluated on the canonical generators and then extended linearly to the completed coordinate module.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.Completion
open scoped BigOperators
universe u v
section CompletedSourceBoundary
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {X H : Type u} [Fintype X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem freeProCZCCompletedFoxBoundary_apply
    (φ : X → H) (v : ZCFreeFoxCoordinates C (X := X) (H := H)) :
    freeProCZCCompletedFoxBoundary C φ v =
      ∑ x : X, v x * (zcGroupLike C H (φ x) - 1)

theorem

freeProCZCCompletedFoxBoundary_single

L357 ↗

FoxDifferential.freeProCZCCompletedFoxBoundary_single

Documentation

The source-shaped completed Fox boundary map sends the standard basis vector at \(x\) to \([\varphi(x)]-1\).

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.Completion
open scoped BigOperators
universe u v
section CompletedSourceBoundary
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {X H : Type u} [Fintype X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [DecidableEq X]

Lean source · statement

theorem freeProCZCCompletedFoxBoundary_single
    (φ : X → H) (x : X) :
    freeProCZCCompletedFoxBoundary C φ
        (Pi.single x (1 : ZCCompletedGroupAlgebra C H)) =
      zcGroupLike C H (φ x) - 1

theorem

continuous_freeProCZCCompletedFoxBoundary

L366 ↗

FoxDifferential.continuous_freeProCZCCompletedFoxBoundary

Documentation

The source-shaped completed Fox boundary map is continuous for finite generating sets.

Source context 12 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.Completion
open scoped BigOperators
universe u v
section CompletedSourceBoundary
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {X H : Type u} [Fintype X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [DecidableEq X]
omit [DecidableEq X] in

Lean source · statement

theorem continuous_freeProCZCCompletedFoxBoundary (φ : X → H) :
    Continuous (freeProCZCCompletedFoxBoundary C φ)

theorem

freeProCZCCompletedFoxBoundary_range

L375 ↗

FoxDifferential.freeProCZCCompletedFoxBoundary_range

Documentation

The source-shaped completed Fox boundary has image equal to the submodule generated by the augmentation generators \([\varphi(x)]-1\).

Source context 12 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.Completion
open scoped BigOperators
universe u v
section CompletedSourceBoundary
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {X H : Type u} [Fintype X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [DecidableEq X]
omit [DecidableEq X] in

Lean source · full declaration

theorem freeProCZCCompletedFoxBoundary_range
    (φ : X → H) :
    (freeProCZCCompletedFoxBoundary C φ).range =
      Submodule.span (ZCCompletedGroupAlgebra C H)
        (Set.range fun x : X => zcGroupLike C H (φ x) - 1) := by
  classical
  apply le_antisymm
  · rintro y ⟨v, rfl⟩
    rw [freeProCZCCompletedFoxBoundary_apply]
    exact Submodule.sum_mem _ fun x _ =>
      Submodule.smul_mem _ (v x)
        (Submodule.subset_span (Set.mem_range_self x))
  · refine Submodule.span_le.2 ?_
    rintro y ⟨x, rfl⟩
    exact ⟨Pi.single x (1 : ZCCompletedGroupAlgebra C H), by simp only
        [freeProCZCCompletedFoxBoundary_single]⟩

theorem

freeProCZCCompletedFoxBoundary_range_eq_standardAugmentationIdeal_of_surjective

L397 ↗

FoxDifferential.freeProCZCCompletedFoxBoundary_range_eq_standardAugmentationIdeal_of_surjective

Documentation

If the chosen finite source hits every element of H, the source-shaped completed Fox boundary has image equal to the algebraic standard-generator ideal.

Source context 12 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.Completion
open scoped BigOperators
universe u v
section CompletedSourceBoundary
variable (C : ProCGroups.FiniteGroupClass.{u})
variable {X H : Type u} [Fintype X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [DecidableEq X]
omit [DecidableEq X] in

Lean source · statement

theorem freeProCZCCompletedFoxBoundary_range_eq_standardAugmentationIdeal_of_surjective
    (φ : X → H) (hφ : Function.Surjective φ) :
    (freeProCZCCompletedFoxBoundary C φ).range =
      (zcCompletedGroupAlgebraStandardAugmentationIdeal C H :
        Submodule (ZCCompletedGroupAlgebra C H) (ZCCompletedGroupAlgebra C H))

instance

instTopologicalSpaceZCCompletedFoxSemidirect

L422 ↗

FoxDifferential.instTopologicalSpaceZCCompletedFoxSemidirect

Documentation

The completed Fox semidirect product carries the inverse-limit topological space structure.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.Completion
open scoped BigOperators
universe u v
section SemidirectTopology
variable (C : ProCGroups.FiniteGroupClass.{v})
variable (X : Type u) [DecidableEq X]
variable (H : Type v) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

instance instTopologicalSpaceZCCompletedFoxSemidirect :
    TopologicalSpace (ZCCompletedFoxSemidirect C X H)

def

zcCompletedFoxSemidirectHomeomorphProd

L428 ↗

FoxDifferential.zcCompletedFoxSemidirectHomeomorphProd

Documentation

The completed Fox semidirect target is homeomorphic to its product of components.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.Completion
open scoped BigOperators
universe u v
section SemidirectTopology
variable (C : ProCGroups.FiniteGroupClass.{v})
variable (X : Type u) [DecidableEq X]
variable (H : Type v) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · full declaration

def zcCompletedFoxSemidirectHomeomorphProd :
    ZCCompletedFoxSemidirect C X H ≃ₜ (ZCFreeFoxCoordinates C (X := X) (H := H) × H) where
  toEquiv :=
    { toFun := fun a => (a.left, a.right)
      invFun := fun p => { left := p.1, right := p.2 }
      left_inv := by
        intro a
        cases a
        rfl
      right_inv := by
        intro p
        cases p
        rfl }
  continuous_toFun := continuous_induced_dom
  continuous_invFun := by
    rw [continuous_induced_rng]
    exact continuous_id

theorem

continuous_zcCompletedFoxSemidirect_toProd

L448 ↗

FoxDifferential.continuous_zcCompletedFoxSemidirect_toProd

Documentation

The component-pair map from the semidirect target is continuous.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.Completion
open scoped BigOperators
universe u v
section SemidirectTopology
variable (C : ProCGroups.FiniteGroupClass.{v})
variable (X : Type u) [DecidableEq X]
variable (H : Type v) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [DecidableEq X] in

Lean source · full declaration

theorem continuous_zcCompletedFoxSemidirect_toProd :
    Continuous (fun a : ZCCompletedFoxSemidirect C X H => (a.left, a.right)) :=
  continuous_induced_dom

theorem

continuous_zcCompletedFoxSemidirect_left

L454 ↗

FoxDifferential.continuous_zcCompletedFoxSemidirect_left

Documentation

The Fox-coordinate projection from the semidirect target is continuous.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.Completion
open scoped BigOperators
universe u v
section SemidirectTopology
variable (C : ProCGroups.FiniteGroupClass.{v})
variable (X : Type u) [DecidableEq X]
variable (H : Type v) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [DecidableEq X] in

Lean source · full declaration

theorem continuous_zcCompletedFoxSemidirect_left :
    Continuous (fun a : ZCCompletedFoxSemidirect C X H => a.left) :=
  continuous_fst.comp (continuous_zcCompletedFoxSemidirect_toProd C X H)

theorem

continuous_zcCompletedFoxSemidirect_right

L460 ↗

FoxDifferential.continuous_zcCompletedFoxSemidirect_right

Documentation

The group projection from the semidirect target is continuous.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.Completion
open scoped BigOperators
universe u v
section SemidirectTopology
variable (C : ProCGroups.FiniteGroupClass.{v})
variable (X : Type u) [DecidableEq X]
variable (H : Type v) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [DecidableEq X] in

Lean source · full declaration

theorem continuous_zcCompletedFoxSemidirect_right :
    Continuous (fun a : ZCCompletedFoxSemidirect C X H => a.right) :=
  continuous_snd.comp (continuous_zcCompletedFoxSemidirect_toProd C X H)

instance

instCompactSpaceZCCompletedFoxSemidirect

L465 ↗

FoxDifferential.instCompactSpaceZCCompletedFoxSemidirect

Documentation

The completed Fox semidirect product is compact as an inverse limit of 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.Completion
open scoped BigOperators
universe u v
section SemidirectTopology
variable (C : ProCGroups.FiniteGroupClass.{v})
variable (X : Type u) [DecidableEq X]
variable (H : Type v) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

instance instCompactSpaceZCCompletedFoxSemidirect [CompactSpace H] :
    CompactSpace (ZCCompletedFoxSemidirect C X H)

instance

instT2SpaceZCCompletedFoxSemidirect

L470 ↗

FoxDifferential.instT2SpaceZCCompletedFoxSemidirect

Documentation

The completed Fox semidirect product is Hausdorff for the inverse-limit topology.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.Completion
open scoped BigOperators
universe u v
section SemidirectTopology
variable (C : ProCGroups.FiniteGroupClass.{v})
variable (X : Type u) [DecidableEq X]
variable (H : Type v) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

instance instT2SpaceZCCompletedFoxSemidirect [T2Space H] :
    T2Space (ZCCompletedFoxSemidirect C X H)

instance

instTotallyDisconnectedSpaceZCCompletedFoxSemidirect

L478 ↗

FoxDifferential.instTotallyDisconnectedSpaceZCCompletedFoxSemidirect

Documentation

The completed Fox semidirect product is totally disconnected as an inverse limit of finite discrete stages.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.Completion
open scoped BigOperators
universe u v
section SemidirectTopology
variable (C : ProCGroups.FiniteGroupClass.{v})
variable (X : Type u) [DecidableEq X]
variable (H : Type v) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

instance instTotallyDisconnectedSpaceZCCompletedFoxSemidirect [TotallyDisconnectedSpace H] :
    TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)

instance

instIsTopologicalGroupZCCompletedFoxSemidirect

L483 ↗

FoxDifferential.instIsTopologicalGroupZCCompletedFoxSemidirect

Documentation

The completed Fox semidirect product is a topological group for the inverse-limit topology.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.Completion
open scoped BigOperators
universe u v
section SemidirectTopology
variable (C : ProCGroups.FiniteGroupClass.{v})
variable (X : Type u) [DecidableEq X]
variable (H : Type v) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · full declaration

instance instIsTopologicalGroupZCCompletedFoxSemidirect :
    IsTopologicalGroup (ZCCompletedFoxSemidirect C X H) where
  continuous_mul := by
    rw [continuous_induced_rng]
    have hleft : Continuous (fun p : ZCCompletedFoxSemidirect C X H ×
        ZCCompletedFoxSemidirect C X H => (p.1 * p.2).left) := by
      refine continuous_pi fun x => ?_
      have hleftA : Continuous (fun p : ZCCompletedFoxSemidirect C X H ×
          ZCCompletedFoxSemidirect C X H => p.1.left x) :=
        (continuous_apply x).comp
          ((continuous_zcCompletedFoxSemidirect_left C X H).comp continuous_fst)
      have hrightA : Continuous (fun p : ZCCompletedFoxSemidirect C X H ×
          ZCCompletedFoxSemidirect C X H => p.2.left x) :=
        (continuous_apply x).comp
          ((continuous_zcCompletedFoxSemidirect_left C X H).comp continuous_snd)
      have hgroup : Continuous (fun p : ZCCompletedFoxSemidirect C X H ×
          ZCCompletedFoxSemidirect C X H => zcGroupLike C H p.1.right) :=
        (continuous_zcGroupLike (C := C) (G := H)).comp
          ((continuous_zcCompletedFoxSemidirect_right C X H).comp continuous_fst)
      change Continuous (fun p : ZCCompletedFoxSemidirect C X H ×
          ZCCompletedFoxSemidirect C X H =>
        p.1.left x + zcGroupLike C H p.1.right * p.2.left x)
      exact hleftA.add (hgroup.mul hrightA)
    have hright : Continuous (fun p : ZCCompletedFoxSemidirect C X H ×
        ZCCompletedFoxSemidirect C X H => (p.1 * p.2).right) := by
      exact ((continuous_zcCompletedFoxSemidirect_right C X H).comp continuous_fst).mul
        ((continuous_zcCompletedFoxSemidirect_right C X H).comp continuous_snd)
    exact hleft.prodMk hright
  continuous_inv := by
    rw [continuous_induced_rng]
    have hleft : Continuous (fun a : ZCCompletedFoxSemidirect C X H => a⁻¹.left) := by
      refine continuous_pi fun x => ?_
      have hleftA : Continuous (fun a : ZCCompletedFoxSemidirect C X H => a.left x) :=
        (continuous_apply x).comp (continuous_zcCompletedFoxSemidirect_left C X H)
      have hgroup : Continuous (fun a : ZCCompletedFoxSemidirect C X H =>
          zcGroupLike C H a.right⁻¹) :=
        (continuous_zcGroupLike (C := C) (G := H)).comp
          ((continuous_zcCompletedFoxSemidirect_right C X H).inv)
      change Continuous (fun a : ZCCompletedFoxSemidirect C X H =>
        -(zcGroupLike C H a.right⁻¹ * a.left x))
      exact (hgroup.mul hleftA).neg
    have hright : Continuous (fun a : ZCCompletedFoxSemidirect C X H => a⁻¹.right) := by
      exact (continuous_zcCompletedFoxSemidirect_right C X H).inv
    exact hleft.prodMk hright

theorem

finiteGroupClass_multiplicative_modNCompletedGroupAlgebraStageInClass_mem

L539 ↗

FoxDifferential.finiteGroupClass_multiplicative_modNCompletedGroupAlgebraStageInClass_mem

Documentation

One finite stage \((\mathbb{Z}/n\mathbb{Z})[H/U]\), viewed multiplicatively through its additive group, belongs to \(C\).

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.Completion
open scoped BigOperators
universe u v
section CompletedGroupAlgebraProC
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem finiteGroupClass_multiplicative_modNCompletedGroupAlgebraStageInClass_mem
    (hIso : ProCGroups.FiniteGroupClass.IsomClosed C)
    (hProd : ProCGroups.FiniteGroupClass.FiniteProductClosed C)
    (i : ProCIntegerIndex C) (U : CompletedGroupAlgebraIndexInClass H C) :
    C (Multiplicative (ModNCompletedGroupAlgebraStageInClass i.modulus H C U))

def

zcCompletedGroupAlgebraMultiplicativeSystem

L597 ↗

FoxDifferential.zcCompletedGroupAlgebraMultiplicativeSystem

Documentation

The group-valued inverse system underlying the additive group of \(\mathbb{Z}_C\llbracket H\rrbracket\), written multiplicatively.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.Completion
open scoped BigOperators
universe u v
section CompletedGroupAlgebraProC
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · full declaration

def zcCompletedGroupAlgebraMultiplicativeSystem :
    ProCGroups.InverseSystems.InverseSystem (I := ZCCompletedGroupAlgebraIndex C H) where
  X := fun i => Multiplicative (ZCCompletedGroupAlgebraStage C H i)
  topologicalSpace := fun _ => ⊥
  map := fun {i j} hij =>
    (zcCompletedGroupAlgebraTransition C H hij).toAddMonoidHom.toMultiplicative
  continuous_map := by
    intro i j hij
    exact continuous_bot
  map_id := by
    intro i
    funext x
    apply Multiplicative.ext
    change zcCompletedGroupAlgebraTransition C H (le_rfl : i ≤ i) x.toAdd = x.toAdd
    simp only [zcCompletedGroupAlgebraTransition_id, RingHom.id_apply]
  map_comp := by
    intro i j k hij hjk
    funext x
    apply Multiplicative.ext
    change
      zcCompletedGroupAlgebraTransition C H hij
          (zcCompletedGroupAlgebraTransition C H hjk x.toAdd) =
        zcCompletedGroupAlgebraTransition C H (hij.trans hjk) x.toAdd
    exact congrArg (fun f : ZCCompletedGroupAlgebraStage C H k →+*
        ZCCompletedGroupAlgebraStage C H i => f x.toAdd)
      (zcCompletedGroupAlgebraTransition_comp C H hij hjk)

instance

instDiscreteTopologyZCCompletedGroupAlgebraMultiplicativeSystemStage

L625 ↗

FoxDifferential.instDiscreteTopologyZCCompletedGroupAlgebraMultiplicativeSystemStage

Documentation

Each stage of the multiplicative system carries the discrete topology selected by the system.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.Completion
open scoped BigOperators
universe u v
section CompletedGroupAlgebraProC
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

instance instDiscreteTopologyZCCompletedGroupAlgebraMultiplicativeSystemStage
    (i : ZCCompletedGroupAlgebraIndex C H) :
    DiscreteTopology ((zcCompletedGroupAlgebraMultiplicativeSystem C H).X i)

instance

instFiniteZCCompletedGroupAlgebraMultiplicativeSystemStage

L631 ↗

FoxDifferential.instFiniteZCCompletedGroupAlgebraMultiplicativeSystemStage

Documentation

Each stage of the multiplicative system is finite.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.Completion
open scoped BigOperators
universe u v
section CompletedGroupAlgebraProC
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

instance instFiniteZCCompletedGroupAlgebraMultiplicativeSystemStage
    (i : ZCCompletedGroupAlgebraIndex C H) :
    Finite ((zcCompletedGroupAlgebraMultiplicativeSystem C H).X i)

instance

instGroupZCCompletedGroupAlgebraMultiplicativeSystemStage

L643 ↗

FoxDifferential.instGroupZCCompletedGroupAlgebraMultiplicativeSystemStage

Documentation

Each finite-stage group algebra in the multiplicative system carries its group structure.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.Completion
open scoped BigOperators
universe u v
section CompletedGroupAlgebraProC
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

instance instGroupZCCompletedGroupAlgebraMultiplicativeSystemStage
    (i : ZCCompletedGroupAlgebraIndex C H) :
    Group ((zcCompletedGroupAlgebraMultiplicativeSystem C H).X i)

instance

instIsTopologicalGroupZCCompletedGroupAlgebraMultiplicativeSystemStage

L650 ↗

FoxDifferential.instIsTopologicalGroupZCCompletedGroupAlgebraMultiplicativeSystemStage

Documentation

Each finite-stage group algebra in the multiplicative system is a topological group.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.Completion
open scoped BigOperators
universe u v
section CompletedGroupAlgebraProC
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

instance instIsTopologicalGroupZCCompletedGroupAlgebraMultiplicativeSystemStage
    (i : ZCCompletedGroupAlgebraIndex C H) :
    IsTopologicalGroup ((zcCompletedGroupAlgebraMultiplicativeSystem C H).X i)

instance

instIsGroupSystemZCCompletedGroupAlgebraMultiplicativeSystem

L658 ↗

FoxDifferential.instIsGroupSystemZCCompletedGroupAlgebraMultiplicativeSystem

Documentation

The multiplicative finite-stage group-algebra system is group-valued.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.Completion
open scoped BigOperators
universe u v
section CompletedGroupAlgebraProC
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · full declaration

instance instIsGroupSystemZCCompletedGroupAlgebraMultiplicativeSystem :
    ProCGroups.InverseSystems.IsGroupSystem
      (zcCompletedGroupAlgebraMultiplicativeSystem C H) where
  map_one := by
    intro i j hij
    apply Multiplicative.ext
    change zcCompletedGroupAlgebraTransition C H hij 0 = 0
    exact map_zero _
  map_mul := by
    intro i j hij x y
    change Multiplicative (ZCCompletedGroupAlgebraStage C H j) at x y
    apply Multiplicative.ext
    change zcCompletedGroupAlgebraTransition C H hij (x.toAdd + y.toAdd) =
      zcCompletedGroupAlgebraTransition C H hij x.toAdd +
        zcCompletedGroupAlgebraTransition C H hij y.toAdd
    exact map_add _ _ _
  map_inv := by
    intro i j hij x
    change Multiplicative (ZCCompletedGroupAlgebraStage C H j) at x
    apply Multiplicative.ext
    change zcCompletedGroupAlgebraTransition C H hij (-x.toAdd) =
      -zcCompletedGroupAlgebraTransition C H hij x.toAdd
    exact (zcCompletedGroupAlgebraTransition C H hij).map_neg x.toAdd

def

zcCompletedGroupAlgebraMultiplicativeLimitEquiv

L686 ↗

FoxDifferential.zcCompletedGroupAlgebraMultiplicativeLimitEquiv

Documentation

The multiplicative inverse limit of the finite completed group-algebra stages is the additive group underlying \(\mathbb{Z}_C\llbracket H\rrbracket\), written multiplicatively.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.Completion
open scoped BigOperators
universe u v
section CompletedGroupAlgebraProC
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

def zcCompletedGroupAlgebraMultiplicativeLimitEquiv :
    (zcCompletedGroupAlgebraMultiplicativeSystem C H).inverseLimit ≃ₜ*
      Multiplicative (ZCCompletedGroupAlgebra C H)

theorem

directed_zcCompletedGroupAlgebraIndex_of_formation

L752 ↗

FoxDifferential.directed_zcCompletedGroupAlgebraIndex_of_formation

Documentation

The two-parameter completed group-algebra index is directed when \(C\) is a formation.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.Completion
open scoped BigOperators
universe u v
section CompletedGroupAlgebraProC
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [IsTopologicalGroup H] in

Lean source · statement

theorem directed_zcCompletedGroupAlgebraIndex_of_formation
    (hForm : ProCGroups.FiniteGroupClass.Formation C) :
    Directed (· ≤ ·)
      (id : ZCCompletedGroupAlgebraIndex C H → ZCCompletedGroupAlgebraIndex C H)

theorem

hasOpenNormalBasisInClass_multiplicative_zcCompletedGroupAlgebra

L766 ↗

FoxDifferential.hasOpenNormalBasisInClass_multiplicative_zcCompletedGroupAlgebra

Documentation

The additive group underlying \(\mathbb{Z}_C\llbracket H\rrbracket\), written multiplicatively, has an open-normal \(C\)-basis.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.Completion
open scoped BigOperators
universe u v
section CompletedGroupAlgebraProC
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem hasOpenNormalBasisInClass_multiplicative_zcCompletedGroupAlgebra
    (hForm : ProCGroups.FiniteGroupClass.Formation C) :
        ProCGroups.ProC.HasOpenNormalBasisInClass C (Multiplicative (ZCCompletedGroupAlgebra C
        H))

def

multiplicativePiContinuousMulEquiv

L832 ↗

FoxDifferential.multiplicativePiContinuousMulEquiv

Documentation

Coordinatewise, the multiplicative version of an additive function group is the product of the multiplicative coordinate groups.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.Completion
open scoped BigOperators
universe u v
section CompletedGroupAlgebraProC
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (X : Type u)

Lean source · full declaration

def multiplicativePiContinuousMulEquiv
    (A : Type u) [AddCommGroup A] [TopologicalSpace A] :
    Multiplicative (X → A) ≃ₜ* (X → Multiplicative A) where
  toMulEquiv :=
    { toFun := fun f x => Multiplicative.ofAdd (f.toAdd x)
      invFun := fun f => Multiplicative.ofAdd fun x => (f x).toAdd
      left_inv := by
        intro f
        rfl
      right_inv := by
        intro f
        rfl
      map_mul' := by
        intro f g
        rfl }
  continuous_toFun := by
    exact continuous_pi fun x =>
      continuous_ofAdd.comp ((continuous_apply x).comp continuous_toAdd)
  continuous_invFun := by
    exact continuous_ofAdd.comp
      (continuous_pi fun x => continuous_toAdd.comp (continuous_apply x))

theorem

hasOpenNormalBasisInClass_multiplicative_zcFreeFoxCoordinates

L856 ↗

FoxDifferential.hasOpenNormalBasisInClass_multiplicative_zcFreeFoxCoordinates

Documentation

The additive Fox-coordinate group \(\mathbb{Z}_C\llbracket H\rrbracket^{X}\), written multiplicatively, has an open-normal \(C\)-basis.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.Completion
open scoped BigOperators
universe u v
section CompletedGroupAlgebraProC
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (X : Type u)

Lean source · statement

theorem hasOpenNormalBasisInClass_multiplicative_zcFreeFoxCoordinates
    (hForm : ProCGroups.FiniteGroupClass.Formation C) : ProCGroups.ProC.HasOpenNormalBasisInClass C
      (Multiplicative (ZCFreeFoxCoordinates C (X := X) (H := H)))

def

zcCompletedFoxSemidirectRightKernelEquivCoordinates

L890 ↗

FoxDifferential.zcCompletedFoxSemidirectRightKernelEquivCoordinates

Documentation

The kernel of the right projection \(\mathbb{Z}_C\llbracket H\rrbracket^{X} \rtimes H \to H\) is the additive coordinate group, written multiplicatively.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.Completion
open scoped BigOperators
universe u v
section SemidirectProC
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (X H : Type u) [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · full declaration

def zcCompletedFoxSemidirectRightKernelEquivCoordinates :
    ((ZCCompletedFoxSemidirect.rightMonoidHom C X H).ker :
        Subgroup (ZCCompletedFoxSemidirect C X H)) ≃ₜ*
      Multiplicative (ZCFreeFoxCoordinates C (X := X) (H := H)) where
  toMulEquiv :=
    { toFun := fun a => Multiplicative.ofAdd a.1.left
      invFun := fun v =>
        ⟨{ left := v.toAdd, right := 1 }, by
          simp only [ZCCompletedFoxSemidirect.rightMonoidHom, MonoidHom.mem_ker,
              MonoidHom.coe_mk, OneHom.coe_mk]⟩
      left_inv := by
        intro a
        apply Subtype.ext
        apply ZCCompletedFoxSemidirect.ext
        · rfl
        · change (1 : H) = a.1.right
          exact a.2.symm
      right_inv := by
        intro v
        rfl
      map_mul' := by
        intro a b
        apply Multiplicative.ext
        have ha : a.1.right = 1 := by
          exact a.2
        simp only [Subgroup.coe_mul, ZCCompletedFoxSemidirect.mul_left, ha, map_one, one_smul,
            ofAdd_add, toAdd_mul,
  toAdd_ofAdd]}
  continuous_toFun := by
    exact continuous_ofAdd.comp
      ((continuous_zcCompletedFoxSemidirect_left C X H).comp continuous_subtype_val)
  continuous_invFun := by
    refine Continuous.subtype_mk ?_ (fun v => by
      simp only [ZCCompletedFoxSemidirect.rightMonoidHom, MonoidHom.mem_ker, MonoidHom.coe_mk,
          OneHom.coe_mk])
    rw [continuous_induced_rng]
    exact continuous_toAdd.prodMk continuous_const

theorem

hasOpenNormalBasisInClass_zcCompletedFoxSemidirect_rightKernel

L931 ↗

FoxDifferential.hasOpenNormalBasisInClass_zcCompletedFoxSemidirect_rightKernel

Documentation

The right-projection kernel in the completed Fox semidirect product has an open-normal \(C\)-basis.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.Completion
open scoped BigOperators
universe u v
section SemidirectProC
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (X H : Type u) [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [DecidableEq X] in

Lean source · statement

theorem hasOpenNormalBasisInClass_zcCompletedFoxSemidirect_rightKernel
    (hForm : ProCGroups.FiniteGroupClass.Formation C) : ProCGroups.ProC.HasOpenNormalBasisInClass C
      ((ZCCompletedFoxSemidirect.rightMonoidHom C X H).ker :
        Subgroup (ZCCompletedFoxSemidirect C X H))

theorem

hasOpenNormalBasisInClass_zcCompletedFoxSemidirect_of_hasOpenNormalBasisInClass

L945 ↗

FoxDifferential.hasOpenNormalBasisInClass_zcCompletedFoxSemidirect_of_hasOpenNormalBasisInClass

Documentation

The completed Fox semidirect target \(\mathbb{Z}_C\llbracket H\rrbracket^{X} \rtimes H\) has an open-normal \(C\)-basis when \(H\) does.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.Completion
open scoped BigOperators
universe u v
section SemidirectProC
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (X H : Type u) [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [DecidableEq X] in

Lean source · statement

theorem hasOpenNormalBasisInClass_zcCompletedFoxSemidirect_of_hasOpenNormalBasisInClass
    [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
    (hMel : ProCGroups.FiniteGroupClass.MelnikovFormation C)
    (hH : ProCGroups.ProC.HasOpenNormalBasisInClass C (H)) :
        ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H)

Module documentation

Fox differential: completed — continuous — topology

Declarations