Module

Naturality.lean

Nyll.ProCGroups.FoxDifferential.Completed.Continuous.Naturality

20 declarations indexed from sourceView source ↗

Module documentation

Fox differential: completed — continuous — naturality

The principal declarations in this module are:

zcCompletedFoxSemidirectMapTarget

Target functoriality for completed Fox semidirect products.

zcCompletedFoxSemidirectMapTargetHom

Target functoriality for completed Fox semidirect products as a continuous homomorphism.

continuous_zcCompletedGroupAlgebraMap

The completed group-algebra map induced by a continuous target homomorphism is continuous.

zcCompletedGroupAlgebraMap_surjective_of_surjective

A surjective target homomorphism induces a surjective completed group-algebra map.

Imports1

Nyll.ProCGroups.FoxDifferential.Completed.Continuous.Free.Rules

Imported by4

theorem

continuous_zcCompletedGroupAlgebraMap

L44 ↗

FoxDifferential.continuous_zcCompletedGroupAlgebraMap

Documentation

The completed group-algebra map induced by a continuous target homomorphism is continuous.

Source context 13 commands

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

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

Lean source · statement

theorem continuous_zcCompletedGroupAlgebraMap (η : H →ₜ* K) :
    Continuous (zcCompletedGroupAlgebraMap C hC η)

theorem

zcCompletedGroupAlgebraMap_surjective_of_surjective

L58 ↗

FoxDifferential.zcCompletedGroupAlgebraMap_surjective_of_surjective

Documentation

A surjective target homomorphism induces a surjective completed group-algebra map.

Source context 13 commands

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

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

Lean source · statement

theorem zcCompletedGroupAlgebraMap_surjective_of_surjective
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (η : H →ₜ* K) (hη : Function.Surjective η) :
    Function.Surjective (zcCompletedGroupAlgebraMap C hC η)

theorem

isQuotientMap_zcCompletedGroupAlgebraMap_of_surjective

L117 ↗

FoxDifferential.isQuotientMap_zcCompletedGroupAlgebraMap_of_surjective

Documentation

A surjective completed group-algebra map is a quotient map.

Source context 13 commands

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

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

Lean source · statement

theorem isQuotientMap_zcCompletedGroupAlgebraMap_of_surjective
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (η : H →ₜ* K) (hη : Function.Surjective η) :
    Topology.IsQuotientMap (zcCompletedGroupAlgebraMap C hC η)

theorem

isOpenQuotientMap_zcCompletedGroupAlgebraMap_of_surjective

L130 ↗

FoxDifferential.isOpenQuotientMap_zcCompletedGroupAlgebraMap_of_surjective

Documentation

A surjective completed group-algebra map is an open quotient map as an additive-group homomorphism.

Source context 13 commands

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

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

Lean source · statement

theorem isOpenQuotientMap_zcCompletedGroupAlgebraMap_of_surjective
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (η : H →ₜ* K) (hη : Function.Surjective η) :
    IsOpenQuotientMap (zcCompletedGroupAlgebraMap C hC η)

theorem

continuous_zcFreeFoxCoordinatesMap

L141 ↗

FoxDifferential.continuous_zcFreeFoxCoordinatesMap

Documentation

The coordinatewise target map on completed Fox-coordinate vectors is continuous.

Source context 14 commands

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

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

Lean source · statement

theorem continuous_zcFreeFoxCoordinatesMap (η : H →ₜ* K) :
    Continuous (zcFreeFoxCoordinatesMap (X := X) C hC η)

theorem

freeProCZCCompletedFoxBoundary_mapTarget

L157 ↗

FoxDifferential.freeProCZCCompletedFoxBoundary_mapTarget

Documentation

Source-shaped completed Fox boundary maps are natural in the target group.

Source context 13 commands

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

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

Lean source · full declaration

theorem freeProCZCCompletedFoxBoundary_mapTarget
    (η : H →ₜ* K) (φ : X → H)
    (v : ZCFreeFoxCoordinates C (X := X) (H := H)) :
    zcCompletedGroupAlgebraMap C hC η (freeProCZCCompletedFoxBoundary C φ v) =
      freeProCZCCompletedFoxBoundary C (fun x : X => η (φ x))
        (zcFreeFoxCoordinatesMap (X := X) C hC η v) := by
  simp only [freeProCZCCompletedFoxBoundary_apply, map_sum, map_mul, map_sub,
    zcCompletedGroupAlgebraMap_groupLike, map_one, zcFreeFoxCoordinatesMap]

def

zcCompletedFoxSemidirectMapTarget

L177 ↗

FoxDifferential.zcCompletedFoxSemidirectMapTarget

Documentation

Target functoriality for completed Fox semidirect products.

Source context 13 commands

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

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

Lean source · full declaration

def zcCompletedFoxSemidirectMapTarget (η : H →ₜ* K) :
    ZCCompletedFoxSemidirect C X H →* ZCCompletedFoxSemidirect C X K where
  toFun a :=
    { left := zcFreeFoxCoordinatesMap (X := X) C hC η a.left
      right := η a.right }
  map_one' := by
    ext x
    · simp only [ZCCompletedFoxSemidirect.one_left, zcFreeFoxCoordinatesMap_apply,
        Pi.zero_apply, map_zero, zcCompletedGroupAlgebraProjection_zero]
    · simp only [ZCCompletedFoxSemidirect.one_right, map_one]
  map_mul' a b := by
    ext x
    · simp only [ZCCompletedFoxSemidirect.mul_left, zcFreeFoxCoordinatesMap_apply,
        Pi.add_apply, Pi.smul_apply, smul_eq_mul, map_add, map_mul,
        zcCompletedGroupAlgebraMap_groupLike, zcCompletedGroupAlgebraProjection_add,
        zcCompletedGroupAlgebraProjection_map, zcCompletedGroupAlgebraProjection_mul,
        zcCompletedGroupAlgebraProjection_groupLike,
        MonoidAlgebra.coeff_add]
    · simp only [ZCCompletedFoxSemidirect.mul_right, map_mul]

theorem

zcCompletedFoxSemidirectMapTarget_left

L203 ↗

FoxDifferential.zcCompletedFoxSemidirectMapTarget_left

Documentation

This declaration identifies the left component of the target map on completed Fox semidirect products.

Source context 14 commands

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

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

Lean source · statement

theorem zcCompletedFoxSemidirectMapTarget_left
    (η : H →ₜ* K) (a : ZCCompletedFoxSemidirect C X H) :
    (zcCompletedFoxSemidirectMapTarget (X := X) C hC η a).left =
      zcFreeFoxCoordinatesMap (X := X) C hC η a.left

theorem

zcCompletedFoxSemidirectMapTarget_right

L215 ↗

FoxDifferential.zcCompletedFoxSemidirectMapTarget_right

Documentation

This declaration identifies the right component of the target map on completed Fox semidirect products.

Source context 14 commands

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

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

Lean source · statement

theorem zcCompletedFoxSemidirectMapTarget_right
    (η : H →ₜ* K) (a : ZCCompletedFoxSemidirect C X H) :
    (zcCompletedFoxSemidirectMapTarget (X := X) C hC η a).right = η a.right

theorem

continuous_zcCompletedFoxSemidirectMapTarget

L222 ↗

FoxDifferential.continuous_zcCompletedFoxSemidirectMapTarget

Documentation

The target map on completed Fox semidirect products is continuous.

Source context 14 commands

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

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

Lean source · statement

theorem continuous_zcCompletedFoxSemidirectMapTarget
    (η : H →ₜ* K) :
    Continuous (zcCompletedFoxSemidirectMapTarget (X := X) C hC η)

def

zcCompletedFoxSemidirectMapTargetHom

L231 ↗

FoxDifferential.zcCompletedFoxSemidirectMapTargetHom

Documentation

Target functoriality for completed Fox semidirect products as a continuous homomorphism.

Source context 13 commands

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

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

Lean source · full declaration

def zcCompletedFoxSemidirectMapTargetHom (η : H →ₜ* K) :
    ZCCompletedFoxSemidirect C X H →ₜ* ZCCompletedFoxSemidirect C X K where
  toMonoidHom := zcCompletedFoxSemidirectMapTarget (X := X) C hC η
  continuous_toFun := continuous_zcCompletedFoxSemidirectMapTarget (X := X) C hC η

theorem

zcCompletedFoxSemidirectMapTargetHom_toMonoidHom

L239 ↗

FoxDifferential.zcCompletedFoxSemidirectMapTargetHom_toMonoidHom

Documentation

The continuous target map has the expected underlying homomorphism.

Source context 14 commands

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

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

Lean source · statement

theorem zcCompletedFoxSemidirectMapTargetHom_toMonoidHom
    (η : H →ₜ* K) :
    (zcCompletedFoxSemidirectMapTargetHom (X := X) C hC η).toMonoidHom =
      zcCompletedFoxSemidirectMapTarget (X := X) C hC η

theorem

zcCompletedFoxSemidirectMapTargetHom_left

L251 ↗

FoxDifferential.zcCompletedFoxSemidirectMapTargetHom_left

Documentation

This declaration identifies the left component of the continuous target map on completed Fox semidirect products.

Source context 14 commands

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

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

Lean source · statement

theorem zcCompletedFoxSemidirectMapTargetHom_left
    (η : H →ₜ* K) (a : ZCCompletedFoxSemidirect C X H) :
    (zcCompletedFoxSemidirectMapTargetHom (X := X) C hC η a).left =
      zcFreeFoxCoordinatesMap (X := X) C hC η a.left

theorem

zcCompletedFoxSemidirectMapTargetHom_right

L263 ↗

FoxDifferential.zcCompletedFoxSemidirectMapTargetHom_right

Documentation

This declaration identifies the right component of the continuous target map on completed Fox semidirect products.

Source context 14 commands

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

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

Lean source · statement

theorem zcCompletedFoxSemidirectMapTargetHom_right
    (η : H →ₜ* K) (a : ZCCompletedFoxSemidirect C X H) :
    (zcCompletedFoxSemidirectMapTargetHom (X := X) C hC η a).right = η a.right

theorem

freeProCZCCompletedFoxSemidirectLift_mapTarget

L290 ↗

FoxDifferential.freeProCZCCompletedFoxSemidirectLift_mapTarget

Documentation

Target naturality of the canonical completed Fox semidirect lift.

Source context 24 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.InverseSystems
open ProCGroups.ProC
open scoped BigOperators
universe u v
section SourceNaturality
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable (hC : ProCGroups.FiniteGroupClass.Hereditary C)
include hC
variable {X F H K : Type u}
variable [Fintype X] [DecidableEq X] [TopologicalSpace X] [DiscreteTopology X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
variable [T2Space (ZCCompletedFoxSemidirect C X H)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
variable [CompactSpace (ZCCompletedFoxSemidirect C X K)]
variable [T2Space (ZCCompletedFoxSemidirect C X K)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X K)]
omit [Fintype X] in

Lean source · full declaration

theorem freeProCZCCompletedFoxSemidirectLift_mapTarget
    {ι : X → F}
    (hι : ProCGroups.FreeProC.IsFreeProCGroup (C := C) ι)
    (htargetH :
    ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
    (htargetK :
    ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X K))
    (η : H →ₜ* K) (φ : X → H) (g : F) :
    zcCompletedFoxSemidirectMapTarget (X := X) C hC η
        (freeProCZCCompletedFoxSemidirectLift
          (C := C) hι htargetH φ
          (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C := C) X H φ) g) =
      freeProCZCCompletedFoxSemidirectLift
        (C := C) hι htargetK (fun x : X => η (φ x))
        (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C := C) X K (fun x :
            X => η (φ x))) g := by
  let hφH : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ) :=
    continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C := C) X H φ
  let φK : X → K := fun x => η (φ x)
  let hφK : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φK) :=
    continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C := C) X K φK
  let f : F →* ZCCompletedFoxSemidirect C X K :=
    (zcCompletedFoxSemidirectMapTarget (X := X) C hC η).comp
      (freeProCZCCompletedFoxSemidirectLift
        (C := C) hι htargetH φ hφH)
  let h : F →* ZCCompletedFoxSemidirect C X K :=
    freeProCZCCompletedFoxSemidirectLift
      (C := C) hι htargetK φK hφK
  have hf_continuous : Continuous f :=
    (continuous_zcCompletedFoxSemidirectMapTarget
      (X := X) C hC η).comp
      (continuous_freeProCZCCompletedFoxSemidirectLift
        (C := C) hι htargetH φ hφH)
  have hh_continuous : Continuous h :=
    continuous_freeProCZCCompletedFoxSemidirectLift
      (C := C) hι htargetK φK hφK
  have hfg : ∀ x : X, f (ι x) = h (ι x) := by
    intro x
    change
      zcCompletedFoxSemidirectMapTarget (X := X) C hC η
          (freeProCZCCompletedFoxSemidirectLift
            (C := C) hι htargetH φ hφH (ι x)) =
        freeProCZCCompletedFoxSemidirectLift
          (C := C) hι htargetK φK hφK (ι x)
    rw [freeProCZCCompletedFoxSemidirectLift_generator,
      freeProCZCCompletedFoxSemidirectLift_generator]
    apply ZCCompletedFoxSemidirect.ext
    · funext y
      by_cases hxy : x = y
      · subst y
        simp only [zcCompletedFoxSemidirectMapTarget_left, zcFreeFoxCoordinatesMap,
          freeProCZCCompletedFoxSemidirectGenerator_left, Pi.single_eq_same, map_one]
      · simp only [zcCompletedFoxSemidirectMapTarget_left, zcFreeFoxCoordinatesMap,
          freeProCZCCompletedFoxSemidirectGenerator_left, ne_eq, hxy, not_false_eq_true,
          Pi.single_eq_of_ne', map_zero]
    · simp only [zcCompletedFoxSemidirectMapTarget_right,
        freeProCZCCompletedFoxSemidirectGenerator_right, φK]
  have hfh : f = h := hι.hom_ext htargetK hf_continuous hh_continuous hfg
  exact congrFun (congrArg DFunLike.coe hfh) g

theorem

freeProCZCCompletedFoxSemidirectLiftHom_mapTarget

L352 ↗

FoxDifferential.freeProCZCCompletedFoxSemidirectLiftHom_mapTarget

Documentation

Continuous-hom form of target naturality for the canonical completed Fox semidirect lift.

Source context 24 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.InverseSystems
open ProCGroups.ProC
open scoped BigOperators
universe u v
section SourceNaturality
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable (hC : ProCGroups.FiniteGroupClass.Hereditary C)
include hC
variable {X F H K : Type u}
variable [Fintype X] [DecidableEq X] [TopologicalSpace X] [DiscreteTopology X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
variable [T2Space (ZCCompletedFoxSemidirect C X H)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
variable [CompactSpace (ZCCompletedFoxSemidirect C X K)]
variable [T2Space (ZCCompletedFoxSemidirect C X K)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X K)]
omit [Fintype X] in

Lean source · full declaration

theorem freeProCZCCompletedFoxSemidirectLiftHom_mapTarget
    {ι : X → F}
    (hι : ProCGroups.FreeProC.IsFreeProCGroup (C := C) ι)
    (htargetH :
    ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
    (htargetK :
    ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X K))
    (η : H →ₜ* K) (φ : X → H) :
    (zcCompletedFoxSemidirectMapTargetHom (X := X) C hC η).comp
        (freeProCZCCompletedFoxSemidirectLiftHom
          (C := C) hι htargetH φ
          (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C := C) X H φ)) =
      freeProCZCCompletedFoxSemidirectLiftHom
        (C := C) hι htargetK (fun x : X => η (φ x))
        (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C := C) X K (fun x :
            X => η (φ x))) := by
  apply ContinuousMonoidHom.ext
  intro g
  exact freeProCZCCompletedFoxSemidirectLift_mapTarget
    (C := C) (X := X) (F := F) (H := H) (K := K)
    hC hι htargetH htargetK η φ g

theorem

freeProCZCCompletedFoxRightHom_mapTarget

L376 ↗

FoxDifferential.freeProCZCCompletedFoxRightHom_mapTarget

Documentation

Target naturality of the right homomorphism of the canonical completed Fox lift.

Source context 24 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.InverseSystems
open ProCGroups.ProC
open scoped BigOperators
universe u v
section SourceNaturality
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable (hC : ProCGroups.FiniteGroupClass.Hereditary C)
include hC
variable {X F H K : Type u}
variable [Fintype X] [DecidableEq X] [TopologicalSpace X] [DiscreteTopology X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
variable [T2Space (ZCCompletedFoxSemidirect C X H)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
variable [CompactSpace (ZCCompletedFoxSemidirect C X K)]
variable [T2Space (ZCCompletedFoxSemidirect C X K)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X K)]
omit [Fintype X] in

Lean source · full declaration

theorem freeProCZCCompletedFoxRightHom_mapTarget
    {ι : X → F}
    (hι : ProCGroups.FreeProC.IsFreeProCGroup (C := C) ι)
    (htargetH :
    ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
    (htargetK :
    ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X K))
    (η : H →ₜ* K) (φ : X → H) :
    freeProCZCCompletedFoxRightHom
        (C := C) hι htargetK (fun x : X => η (φ x))
        (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C := C) X K (fun x :
            X => η (φ x))) =
      η.toMonoidHom.comp
        (freeProCZCCompletedFoxRightHom
          (C := C) hι htargetH φ
          (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C := C) X H φ)) := by
  ext g
  have h := congrArg ZCCompletedFoxSemidirect.right
    (freeProCZCCompletedFoxSemidirectLift_mapTarget
      (C := C) (X := X) (F := F) (H := H) (K := K)
      hC hι htargetH htargetK η φ g)
  simpa [freeProCZCCompletedFoxRightHom_apply, MonoidHom.comp_apply] using h.symm

theorem

freeProCZCCompletedFoxDerivativeVector_mapTarget

L401 ↗

FoxDifferential.freeProCZCCompletedFoxDerivativeVector_mapTarget

Documentation

Target naturality of the derivative vector of the canonical completed Fox lift.

Source context 24 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.InverseSystems
open ProCGroups.ProC
open scoped BigOperators
universe u v
section SourceNaturality
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable (hC : ProCGroups.FiniteGroupClass.Hereditary C)
include hC
variable {X F H K : Type u}
variable [Fintype X] [DecidableEq X] [TopologicalSpace X] [DiscreteTopology X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
variable [T2Space (ZCCompletedFoxSemidirect C X H)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
variable [CompactSpace (ZCCompletedFoxSemidirect C X K)]
variable [T2Space (ZCCompletedFoxSemidirect C X K)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X K)]
omit [Fintype X] in

Lean source · full declaration

theorem freeProCZCCompletedFoxDerivativeVector_mapTarget
    {ι : X → F}
    (hι : ProCGroups.FreeProC.IsFreeProCGroup (C := C) ι)
    (htargetH :
    ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
    (htargetK :
    ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X K))
    (η : H →ₜ* K) (φ : X → H) (g : F) :
    freeProCZCCompletedFoxDerivativeVector
        (C := C) hι htargetK (fun x : X => η (φ x))
        (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C := C) X K (fun x :
            X => η (φ x))) g =
      zcFreeFoxCoordinatesMap (X := X) C hC η
        (freeProCZCCompletedFoxDerivativeVector
          (C := C) hι htargetH φ
          (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C := C) X H φ) g) := by
  have h := congrArg ZCCompletedFoxSemidirect.left
    (freeProCZCCompletedFoxSemidirectLift_mapTarget
      (C := C) (X := X) (F := F) (H := H) (K := K)
      hC hι htargetH htargetK η φ g)
  convert h.symm using 1 <;> rfl

theorem

freeProCZCCompletedFoxDerivativeVector_mapTarget_apply

L425 ↗

FoxDifferential.freeProCZCCompletedFoxDerivativeVector_mapTarget_apply

Documentation

Target naturality for the canonical completed Fox derivative holds componentwise.

Source context 24 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.InverseSystems
open ProCGroups.ProC
open scoped BigOperators
universe u v
section SourceNaturality
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable (hC : ProCGroups.FiniteGroupClass.Hereditary C)
include hC
variable {X F H K : Type u}
variable [Fintype X] [DecidableEq X] [TopologicalSpace X] [DiscreteTopology X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
variable [T2Space (ZCCompletedFoxSemidirect C X H)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
variable [CompactSpace (ZCCompletedFoxSemidirect C X K)]
variable [T2Space (ZCCompletedFoxSemidirect C X K)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X K)]
omit [Fintype X] in

Lean source · full declaration

theorem freeProCZCCompletedFoxDerivativeVector_mapTarget_apply
    {ι : X → F}
    (hι : ProCGroups.FreeProC.IsFreeProCGroup (C := C) ι)
    (htargetH :
    ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
    (htargetK :
    ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X K))
    (η : H →ₜ* K) (φ : X → H) (g : F) (x : X) :
    freeProCZCCompletedFoxDerivativeVector
        (C := C) hι htargetK (fun x : X => η (φ x))
        (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C := C) X K (fun x :
            X => η (φ x))) g x =
      zcCompletedGroupAlgebraMap C hC η
        (freeProCZCCompletedFoxDerivativeVector
          (C := C) hι htargetH φ
          (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C := C) X H φ) g x)
              := by
  have h := congrFun
    (freeProCZCCompletedFoxDerivativeVector_mapTarget
      (C := C) (X := X) (F := F) (H := H) (K := K)
      hC hι htargetH htargetK η φ g) x
  simpa [zcFreeFoxCoordinatesMap] using h

theorem

freeProCZCCompletedFoxBoundary_mapTarget_of_derivativeVector

L452 ↗

FoxDifferential.freeProCZCCompletedFoxBoundary_mapTarget_of_derivativeVector

Documentation

Target naturality for the source-shaped boundary applied to the canonical completed Fox derivative vector.

Source context 23 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.InverseSystems
open ProCGroups.ProC
open scoped BigOperators
universe u v
section SourceNaturality
variable {C : ProCGroups.FiniteGroupClass.{u}}
variable (hC : ProCGroups.FiniteGroupClass.Hereditary C)
include hC
variable {X F H K : Type u}
variable [Fintype X] [DecidableEq X] [TopologicalSpace X] [DiscreteTopology X]
variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
variable [T2Space (ZCCompletedFoxSemidirect C X H)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
variable [CompactSpace (ZCCompletedFoxSemidirect C X K)]
variable [T2Space (ZCCompletedFoxSemidirect C X K)]
variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X K)]

Lean source · full declaration

theorem freeProCZCCompletedFoxBoundary_mapTarget_of_derivativeVector
    {ι : X → F}
    (hι : ProCGroups.FreeProC.IsFreeProCGroup (C := C) ι)
    (htargetH :
    ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
    (htargetK :
    ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X K))
    (η : H →ₜ* K) (φ : X → H) (g : F) :
    zcCompletedGroupAlgebraMap C hC η
        (freeProCZCCompletedFoxBoundary C φ
          (freeProCZCCompletedFoxDerivativeVector
            (C := C) hι htargetH φ
            (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C := C) X H φ) g)) =
      freeProCZCCompletedFoxBoundary C (fun x : X => η (φ x))
        (freeProCZCCompletedFoxDerivativeVector
          (C := C) hι htargetK (fun x : X => η (φ x))
          (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C := C) X K (fun x
              : X => η (φ x))) g) := by
  rw [freeProCZCCompletedFoxBoundary_mapTarget]
  rw [← freeProCZCCompletedFoxDerivativeVector_mapTarget
    (C := C) (X := X) (F := F) (H := H) (K := K)
    hC hι htargetH htargetK η φ g]

Module documentation

Fox differential: completed — continuous — naturality

Declarations