Yamaguchi Lean 4 Library
ProCGroups.FoxDifferential.Completed.Continuous.SemidirectKernelBasis
ProCGroups/FoxDifferential/Completed/Continuous/SemidirectKernelBasis

ProCGroups.FoxDifferential.Completed.Continuous.SemidirectKernelBasis

6 Theorems

The principal declarations in this module are:

  • finiteCoordinateZeroRectangularNeighbourhoods_pi Finite-coordinate product neighborhoods in a function space contain coordinate rectangles. This is the generic topological input needed to pass from coefficient-kernel bases for \(\mathbb{Z}_C\llbracket H\rrbracket\) to coordinate-kernel bases for \(\mathbb{Z}_C\llbracket H\rrbracket^{X}\). It uses the product topology directly and keeps no algebraic assumptions. - zcFreeFoxCoordinates_hasFiniteCoordinateZeroRectangularNeighbourhoods Standard product-topology coordinate rectangles for completed Fox-coordinate families. - zcCompletedFoxSemidirect_hasRectangularIdentityNeighbourhoods In the standard topology on \(\mathbb{Z}_C\llbracket H\rrbracket^{X} \rtimes H\), every identity neighborhood contains a product rectangle around (0,1) in the coordinate and target components. - freeProCZCFoxSemiZCBifilteredStageMap_identity_basis_of_component_bases_standardTopology Standard-topology form of the componentwise kernel-basis theorem for actual \(\mathbb{Z}_C\llbracket H\rrbracket\) bifiltered finite stages.
import
Imported by

Declarations

Theorem FoxDifferential.finiteCoordinateZeroRectangularNeighbourhoods_pi 
theorem finiteCoordinateZeroRectangularNeighbourhoods_pi :
    HasFiniteCoordinateZeroRectangularNeighbourhoods (A := A) (X := X)

Finite-coordinate product neighborhoods in a function space contain coordinate rectangles. This is the generic topological input needed to pass from coefficient-kernel bases for \(\mathbb{Z}_C\llbracket H\rrbracket\) to coordinate-kernel bases for \(\mathbb{Z}_C\llbracket H\rrbracket^{X}\). It uses the product topology directly and keeps no algebraic assumptions.

Show Lean proof
Theorem FoxDifferential.zcFreeFoxCoordinates_hasFiniteCoordinateZeroRectangularNeighbourhoods 
theorem zcFreeFoxCoordinates_hasFiniteCoordinateZeroRectangularNeighbourhoods
    (C : ProCGroups.FiniteGroupClass.{u}) (X H : Type u)
    [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    HasFiniteCoordinateZeroRectangularNeighbourhoods
      (A := ZCCompletedGroupAlgebra C H) (X := X)

Standard product-topology coordinate rectangles for completed Fox-coordinate families.

Show Lean proof
Theorem FoxDifferential.zcCompletedFoxSemidirect_hasRectangularIdentityNeighbourhoods 
omit [DecidableEq X] in
theorem zcCompletedFoxSemidirect_hasRectangularIdentityNeighbourhoods :
    HasSemidirectRectangularIdentityNeighbourhoods
      (X := X) (H := H) C

In the standard topology on \(\mathbb{Z}_C\llbracket H\rrbracket^{X} \rtimes H\), every identity neighborhood contains a product rectangle around (0,1) in the coordinate and target components.

Show Lean proof
Theorem FoxDifferential.freeProCZCFoxSemiZCBifilteredStageMap_identity_basis_of_component_bases_standardTopology 
omit [DecidableEq X] [∀ (j : J), Fact (0 < nstage j)] in
theorem freeProCZCFoxSemiZCBifilteredStageMap_identity_basis_of_component_bases_standardTopology
    (hdir : Directed (· ≤ ·) (id : J → J))
    (hcoeff_mod : ∀ {i j : J} (hij : i ≤ j),
      ∀ a : ModNCompletedCoeff (zcIndex j).1.modulus,
        modNCompletedCoeffMap
            (n := nstage i) (m := (zcIndex i).1.modulus) (hmod i)
            (modNCompletedCoeffMap
              (n := (zcIndex i).1.modulus) (m := (zcIndex j).1.modulus)
              (hzcIndex hij).1 a) =
          modNCompletedCoeffMap (n := nstage i) (m := nstage j) (hn hij)
            (modNCompletedCoeffMap
              (n := nstage j) (m := (zcIndex j).1.modulus) (hmod j) a))
    (hqmap_transition : ∀ {i j : J} (hij : i ≤ j),
      ∀ q : CompletedGroupAlgebraQuotientInClass H C (zcIndex j).2,
        qmap i
            ((OpenNormalSubgroupInClass.map
              (C := C) (G := H)
              (U := OrderDual.ofDual (zcIndex i).2)
              (V := OrderDual.ofDual (zcIndex j).2)
              (hzcIndex hij).2) q) =
          foxAlgebraicStageTargetQuotientMap (X := X) (hN hij) (qmap j q))
    (hleft_basis :
      HasAdditiveIdentityQuotientKernelNeighbourhoodBasis
        (A := ZCFreeFoxCoordinates C (X := X) (H := H))
        (fun j : J =>
          zcFreeFoxCoordinatesBifilteredStageMap
            (C := C) (X := X) (H := H) Nstage nstage
            (fun k => zcCompletedGroupAlgebraBifilteredStageCoeffMap
              (C := C) (X := X) (H := H) Nstage nstage zcIndex hmod qmap k) j))
    (hright_basis :
      HasIdentityQuotientKernelNeighbourhoodBasis
        (Y := H)
        (fun j : J =>
          zcCompletedGroupAlgebraBifilteredStageRightMap
            (C := C) (X := X) (H := H) Nstage zcIndex qmap j)) :
    HasIdentityQuotientKernelNeighbourhoodBasis
      (Y := ZCCompletedFoxSemidirect C X H)
      (fun j : J =>
        freeProCZCCompletedFoxSemidirectZCBifilteredStageMap
          (C := C) (X := X) (H := H) Nstage nstage zcIndex hmod qmap j)

Standard-topology form of the componentwise kernel-basis theorem for actual \(\mathbb{Z}_C\llbracket H\rrbracket\) bifiltered finite stages.

Show Lean proof
Theorem FoxDifferential.zcFreeFoxCoordinatesBifilteredStageMap_additive_basis_of_coeff_basis_standardTopology 
omit [DecidableEq X] [∀ (j : J), Fact (0 < nstage j)] in
theorem zcFreeFoxCoordinatesBifilteredStageMap_additive_basis_of_coeff_basis_standardTopology
    [Finite X] [Nonempty J]
    (hdir : Directed (· ≤ ·) (id : J → J))
    (hcoeff_mod : ∀ {i j : J} (hij : i ≤ j),
      ∀ a : ModNCompletedCoeff (zcIndex j).1.modulus,
        modNCompletedCoeffMap
            (n := nstage i) (m := (zcIndex i).1.modulus) (hmod i)
            (modNCompletedCoeffMap
              (n := (zcIndex i).1.modulus) (m := (zcIndex j).1.modulus)
              (hzcIndex hij).1 a) =
          modNCompletedCoeffMap (n := nstage i) (m := nstage j) (hn hij)
            (modNCompletedCoeffMap
              (n := nstage j) (m := (zcIndex j).1.modulus) (hmod j) a))
    (hqmap_transition : ∀ {i j : J} (hij : i ≤ j),
      ∀ q : CompletedGroupAlgebraQuotientInClass H C (zcIndex j).2,
        qmap i
            ((OpenNormalSubgroupInClass.map
              (C := C) (G := H)
              (U := OrderDual.ofDual (zcIndex i).2)
              (V := OrderDual.ofDual (zcIndex j).2)
              (hzcIndex hij).2) q) =
          foxAlgebraicStageTargetQuotientMap (X := X) (hN hij) (qmap j q))
    (hcoeff_basis :
      HasAdditiveIdentityQuotientKernelNeighbourhoodBasis
        (A := ZCCompletedGroupAlgebra C H)
        (fun j : J =>
          (zcCompletedGroupAlgebraBifilteredStageCoeffMap
            (C := C) (X := X) (H := H) Nstage nstage zcIndex hmod qmap j).toAddMonoidHom)) :
    HasAdditiveIdentityQuotientKernelNeighbourhoodBasis
      (A := ZCFreeFoxCoordinates C (X := X) (H := H))
      (fun j : J =>
        zcFreeFoxCoordinatesBifilteredStageMap
          (C := C) (X := X) (H := H) Nstage nstage
          (fun k => zcCompletedGroupAlgebraBifilteredStageCoeffMap
            (C := C) (X := X) (H := H) Nstage nstage zcIndex hmod qmap k) j)

Standard-topology additive kernel basis for completed Fox coordinates, reduced to the coefficient-ring kernel basis. For finite Fox coordinate families, product neighborhoods give the coordinate rectangles needed for the coordinate-kernel theorem.

Show Lean proof
Theorem FoxDifferential.semiZCBiStageMap_identityBasis_of_coeff_rightBases 
omit [DecidableEq X] [∀ (j : J), Fact (0 < nstage j)] in
theorem semiZCBiStageMap_identityBasis_of_coeff_rightBases
    [Finite X] [Nonempty J]
    (hdir : Directed (· ≤ ·) (id : J → J))
    (hcoeff_mod : ∀ {i j : J} (hij : i ≤ j),
      ∀ a : ModNCompletedCoeff (zcIndex j).1.modulus,
        modNCompletedCoeffMap
            (n := nstage i) (m := (zcIndex i).1.modulus) (hmod i)
            (modNCompletedCoeffMap
              (n := (zcIndex i).1.modulus) (m := (zcIndex j).1.modulus)
              (hzcIndex hij).1 a) =
          modNCompletedCoeffMap (n := nstage i) (m := nstage j) (hn hij)
            (modNCompletedCoeffMap
              (n := nstage j) (m := (zcIndex j).1.modulus) (hmod j) a))
    (hqmap_transition : ∀ {i j : J} (hij : i ≤ j),
      ∀ q : CompletedGroupAlgebraQuotientInClass H C (zcIndex j).2,
        qmap i
            ((OpenNormalSubgroupInClass.map
              (C := C) (G := H)
              (U := OrderDual.ofDual (zcIndex i).2)
              (V := OrderDual.ofDual (zcIndex j).2)
              (hzcIndex hij).2) q) =
          foxAlgebraicStageTargetQuotientMap (X := X) (hN hij) (qmap j q))
    (hcoeff_basis :
      HasAdditiveIdentityQuotientKernelNeighbourhoodBasis
        (A := ZCCompletedGroupAlgebra C H)
        (fun j : J =>
          (zcCompletedGroupAlgebraBifilteredStageCoeffMap
            (C := C) (X := X) (H := H) Nstage nstage zcIndex hmod qmap j).toAddMonoidHom))
    (hright_basis :
      HasIdentityQuotientKernelNeighbourhoodBasis
        (Y := H)
        (fun j : J =>
          zcCompletedGroupAlgebraBifilteredStageRightMap
            (C := C) (X := X) (H := H) Nstage zcIndex qmap j)) :
    HasIdentityQuotientKernelNeighbourhoodBasis
      (Y := ZCCompletedFoxSemidirect C X H)
      (fun j : J =>
        freeProCZCCompletedFoxSemidirectZCBifilteredStageMap
          (C := C) (X := X) (H := H) Nstage nstage zcIndex hmod qmap j)

The semidirect kernel basis for the standard topology from coefficient and target component bases. This is the componentwise kernel-basis theorem with the left coordinate basis built internally from the coefficient maps \(\mathbb{Z}_C\llbracket H\rrbracket \to (\mathbb{Z}/n_j\mathbb{Z})[F/N_j]\).

Show Lean proof