ProCGroups.FoxDifferential.Completed.FreeProC.SemidirectKernelBasis

8 Theorems | 4 Definitions

The principal declarations in this module are:

HasAdditiveIdentityQuotientKernelNeighbourhoodBasis Additive-coordinate quotient kernels form a neighborhood basis at zero. This is the additive analogue of HasIdentityQuotientKernelNeighborhoodBasis. It is used for the left coordinate \(\mathbb{Z}_C\llbracket H\rrbracket^{X}\), whose finite-stage maps are additive homomorphisms rather than multiplicative homomorphisms. - HasFiniteCoordinateZeroRectangularNeighbourhoods A finite product neighborhood around zero in \(X \to A\), formulated for coordinatewise kernel-basis statements. - coordinatewiseAddMonoidHom_apply The coordinatewise additive homomorphism evaluates by applying the chosen additive map to each coordinate. - coordinatewiseAdditiveKernelBasis_of_component_basis If coefficient kernels form a zero-neighborhood basis and stage kernels are monotone along a directed finite-stage system, then the coordinatewise finite product maps also form a zero-neighborhood kernel basis.

import

ProCGroups.FoxDifferential.Completed.FreeProC.ProCIntegerBifilteredStageRightProjection

Imported by

Definition FoxDifferential.HasAdditiveIdentityQuotientKernelNeighbourhoodBasis

def HasAdditiveIdentityQuotientKernelNeighbourhoodBasis : Prop :=
  ∀ U : Set A, IsOpen U → (0 : A) ∈ U →
    ∃ j : J, ∀ z : A, π j z = 0 → z ∈ U

Additive-coordinate quotient kernels form a neighborhood basis at zero. This is the additive analogue of HasIdentityQuotientKernelNeighborhoodBasis. It is used for the left coordinate \(\mathbb{Z}_C\llbracket H\rrbracket^{X}\), whose finite-stage maps are additive homomorphisms rather than multiplicative homomorphisms.

Definition FoxDifferential.HasFiniteCoordinateZeroRectangularNeighbourhoods

def HasFiniteCoordinateZeroRectangularNeighbourhoods : Prop :=
  ∀ U : Set (X → A), IsOpen U → (0 : X → A) ∈ U →
    ∃ V : X → Set A,
      (∀ x : X, IsOpen (V x) ∧ (0 : A) ∈ V x) ∧
      ∀ v : X → A, (∀ x : X, v x ∈ V x) → v ∈ U

A finite product neighborhood around zero in \(X \to A\), formulated for coordinatewise kernel-basis statements.

Definition FoxDifferential.coordinatewiseAddMonoidHom

def coordinatewiseAddMonoidHom
    (π : ∀ j : J, A →+ B j) (j : J) :
    (X → A) →+ (X → B j) where
  toFun v := fun x => π j (v x)
  map_zero' := by
    funext x
    exact map_zero (π j)
  map_add' v w := by
    funext x
    exact map_add (π j) (v x) (w x)

A stage coefficient map induces a coordinatewise additive homomorphism.

Theorem FoxDifferential.coordinatewiseAddMonoidHom_apply

omit [TopologicalSpace A] [Preorder J] [Nonempty J] [Finite X] in
@[simp]
theorem coordinatewiseAddMonoidHom_apply
    (π : ∀ j : J, A →+ B j) (j : J) (v : X → A) (x : X) :
    coordinatewiseAddMonoidHom (X := X) π j v x = π j (v x)

The coordinatewise additive homomorphism evaluates by applying the chosen additive map to each coordinate.

Show Lean proof

Theorem FoxDifferential.coordinatewiseAdditiveKernelBasis_of_component_basis

theorem coordinatewiseAdditiveKernelBasis_of_component_basis
    (π : ∀ j : J, A →+ B j)
    (hrect : HasFiniteCoordinateZeroRectangularNeighbourhoods (A := A) (X := X))
    (hdir : Directed (· ≤ ·) (id : J → J))
    (hbasis : HasAdditiveIdentityQuotientKernelNeighbourhoodBasis (A := A) π)
    (hmono : ∀ {i j : J}, i ≤ j → ∀ a : A, π j a = 0 → π i a = 0) :
    HasAdditiveIdentityQuotientKernelNeighbourhoodBasis
      (A := X → A)
      (fun j : J => coordinatewiseAddMonoidHom (X := X) π j)

If coefficient kernels form a zero-neighborhood basis and stage kernels are monotone along a directed finite-stage system, then the coordinatewise finite product maps also form a zero-neighborhood kernel basis.

Show Lean proof

Definition FoxDifferential.HasSemidirectRectangularIdentityNeighbourhoods

def HasSemidirectRectangularIdentityNeighbourhoods
    (C : ProCGroups.FiniteGroupClass.{u})
    [TopologicalSpace (ZCCompletedGroupAlgebra C H)]
    [TopologicalSpace (ZCCompletedFoxSemidirect C X H)] : Prop :=
  ∀ U : Set (ZCCompletedFoxSemidirect C X H),
    IsOpen U → (1 : ZCCompletedFoxSemidirect C X H) ∈ U →
      ∃ UL : Set (ZCFreeFoxCoordinates C (X := X) (H := H)),
      ∃ UR : Set H,
        IsOpen UL ∧ (0 : ZCFreeFoxCoordinates C (X := X) (H := H)) ∈ UL ∧
        IsOpen UR ∧ (1 : H) ∈ UR ∧
        ∀ y : ZCCompletedFoxSemidirect C X H,
          y.left ∈ UL → y.right ∈ UR → y ∈ U

Identity neighborhoods in the completed Fox semidirect product contain component rectangles; the standard product homeomorphism identifies the semidirect carrier with \(\mathbb{Z}_C\llbracket H\rrbracket^{X} \times H\).

Theorem FoxDifferential.freeProCZCCompletedFoxSemidirectStageMap_identity_basis_of_component_bases

omit [∀ (j : J), Fact (0 < nstage j)] in
omit [DecidableEq X] in
theorem freeProCZCCompletedFoxSemidirectStageMap_identity_basis_of_component_bases
    (hrect : HasSemidirectRectangularIdentityNeighbourhoods
      (X := X) (H := H) C)
    (hdir : Directed (· ≤ ·) (id : J → J))
    (stageLeft : ∀ j : J,
      ZCFreeFoxCoordinates C (X := X) (H := H) →+
        foxAlgebraicStageCoordinateVector (X := X) (Nstage j) (nstage j))
    (stageRight : ∀ j : J, H →* foxAlgebraicStageTargetQuotient (X := X) (Nstage j))
    (hscalar : ∀ j : J, ∀ (h : H)
      (v : ZCFreeFoxCoordinates C (X := X) (H := H)),
        stageLeft j (zcGroupLike C H h • v) =
          (MonoidAlgebra.of (ModNCompletedCoeff (nstage j))
            (foxAlgebraicStageTargetQuotient (X := X) (Nstage j)) (stageRight j h)) •
            stageLeft j v)
    (hleft_basis :
      HasAdditiveIdentityQuotientKernelNeighbourhoodBasis
        (A := ZCFreeFoxCoordinates C (X := X) (H := H))
        stageLeft)
    (hright_basis :
      HasIdentityQuotientKernelNeighbourhoodBasis (Y := H) stageRight)
    (hleft_mono : ∀ {i j : J}, i ≤ j →
      ∀ v : ZCFreeFoxCoordinates C (X := X) (H := H),
        stageLeft j v = 0 → stageLeft i v = 0)
    (hright_mono : ∀ {i j : J}, i ≤ j → ∀ h : H,
        stageRight j h = 1 → stageRight i h = 1) :
    HasIdentityQuotientKernelNeighbourhoodBasis
      (Y := ZCCompletedFoxSemidirect C X H)
      (fun j : J =>
        freeProCZCCompletedFoxSemidirectStageMap
          (C := C) (X := X) (H := H) (Nstage j) (nstage j)
          (stageLeft j) (stageRight j) (hscalar j))

If the coordinate kernels and target kernels are neighborhood bases in the two components, and the finite-stage kernels are monotone along the directed stage system, then the semidirect stage kernels are a neighborhood basis at the identity. This is the topological bridge needed to feed actual finite quotient projections into the completed Fox density theorem.

Show Lean proof

Theorem FoxDifferential.zcFreeFoxCoordinatesBifilteredStageMap_kernel_mono

omit [TopologicalSpace (ZCCompletedGroupAlgebra C H)] in
omit [DecidableEq X] [∀ (j : J), Fact (0 < nstage j)] in
omit [TopologicalSpace (ZCCompletedFoxSemidirect C X H)] [IsTopologicalGroup
    (ZCCompletedFoxSemidirect C X H)] in
theorem zcFreeFoxCoordinatesBifilteredStageMap_kernel_mono
    (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))
    {i j : J} (hij : i ≤ j)
    (v : ZCFreeFoxCoordinates C (X := X) (H := H))
    (hv :
      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 v = 0) :
      zcFreeFoxCoordinatesBifilteredStageMap
        (C := C) (X := X) (H := H) Nstage nstage
        (fun k => zcCompletedGroupAlgebraBifilteredStageCoeffMap
          (C := C) (X := X) (H := H) Nstage nstage zcIndex hmod qmap k)
        i v = 0

The left coordinate kernels of the actual \(\mathbb{Z}_C\llbracket H\rrbracket\) bifiltered stage maps are monotone along stage refinement.

Show Lean proof

Theorem FoxDifferential.zcCompletedGroupAlgebraBifilteredStageCoeffMap_kernel_mono

omit [TopologicalSpace (ZCCompletedGroupAlgebra C H)] in
omit [DecidableEq X] [∀ (j : J), Fact (0 < nstage j)] in
omit [TopologicalSpace (ZCCompletedFoxSemidirect C X H)] [IsTopologicalGroup
    (ZCCompletedFoxSemidirect C X H)] in
theorem zcCompletedGroupAlgebraBifilteredStageCoeffMap_kernel_mono
    (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))
    {i j : J} (hij : i ≤ j)
    (a : ZCCompletedGroupAlgebra C H)
    (ha :
      zcCompletedGroupAlgebraBifilteredStageCoeffMap
        (C := C) (X := X) (H := H) Nstage nstage zcIndex hmod qmap j a = 0) :
      zcCompletedGroupAlgebraBifilteredStageCoeffMap
        (C := C) (X := X) (H := H) Nstage nstage zcIndex hmod qmap i a = 0

The coefficient kernels of actual \(\mathbb{Z}_C\llbracket H\rrbracket\) bifiltered finite-stage maps are monotone along stage refinement.

Show Lean proof

Theorem FoxDifferential.zcFreeFoxCoordinatesBifilteredStageMap_additive_basis_of_coeff_basis

omit [DecidableEq X] [∀ (j : J), Fact (0 < nstage j)] [TopologicalSpace
    (ZCCompletedFoxSemidirect C X H)] [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)] in
theorem zcFreeFoxCoordinatesBifilteredStageMap_additive_basis_of_coeff_basis
    [Finite X] [Nonempty J]
    (hcoord_rect :
      HasFiniteCoordinateZeroRectangularNeighbourhoods
        (A := ZCCompletedGroupAlgebra C H) (X := X))
    (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)

A finite-coordinate additive kernel-basis criterion for completed Fox-coordinate projections in terms of the coefficient projections.

Show Lean proof

Theorem FoxDifferential.zcCompletedGroupAlgebraBifilteredStageRightMap_kernel_mono

omit [TopologicalSpace (ZCCompletedGroupAlgebra C H)] in
omit [DecidableEq X] [TopologicalSpace (ZCCompletedFoxSemidirect C X H)] [IsTopologicalGroup
    (ZCCompletedFoxSemidirect C X H)] in
theorem zcCompletedGroupAlgebraBifilteredStageRightMap_kernel_mono
    (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))
    {i j : J} (hij : i ≤ j) (h : H)
    (hh :
      zcCompletedGroupAlgebraBifilteredStageRightMap
        (C := C) (X := X) (H := H) Nstage zcIndex qmap j h = 1) :
      zcCompletedGroupAlgebraBifilteredStageRightMap
        (C := C) (X := X) (H := H) Nstage zcIndex qmap i h = 1

The right kernels of the automatically defined bifiltered stage maps are monotone along stage refinement.

Show Lean proof

Theorem FoxDifferential.freeProCZCFoxSemiZCBifilteredStageMap_identity_basis_of_component_bases

omit [DecidableEq X] [∀ (j : J), Fact (0 < nstage j)] [IsTopologicalGroup
    (ZCCompletedFoxSemidirect C X H)] in
theorem freeProCZCFoxSemiZCBifilteredStageMap_identity_basis_of_component_bases
    (hrect : HasSemidirectRectangularIdentityNeighbourhoods
      (X := X) (H := H) C)
    (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)

Componentwise zero and identity kernel bases imply the identity-neighborhood kernel basis for the actual \(\mathbb{Z}_C\llbracket H\rrbracket\) bifiltered semidirect stage maps.

Show Lean proof

ProCGroups.FoxDifferential.Completed.FreeProC.SemidirectKernelBasis

Declarations