ProCGroups.FoxDifferential.Completed.Continuous.Free.Rules
The principal declarations in this module are:
freeProCZCCompletedFoxRightHomContinuousMonoidHomThe right component of the completed free pro-\(C\) Fox lift is bundled as a continuous homomorphism. -freeProCZCCompletedFoxDerivativeVectorContinuousMapThe completed free pro-\(C\) Fox derivative vector is bundled as a continuous map; it is a crossed differential, not a homomorphism. -freeProCZCCompletedFoxRightHomContinuousMonoidHom_toMonoidHomThe bundled right homomorphism has the expected underlying monoid homomorphism. -freeProCZCCompletedFoxRightHomContinuousMonoidHom_applyEvaluation of the bundled right homomorphism.
imports
def freeProCZCCompletedFoxRightHomContinuousMonoidHom : F →ₜ* H where
toMonoidHom := freeProCZCCompletedFoxRightHom (C := C) hι htarget φ hφ
continuous_toFun :=
continuous_freeProCZCCompletedFoxRightHom (C := C) X H hι htarget φ hφThe right component of the completed free pro-\(C\) Fox lift is bundled as a continuous homomorphism.
@[simp]
theorem freeProCZCCompletedFoxRightHomContinuousMonoidHom_toMonoidHom :
(freeProCZCCompletedFoxRightHomContinuousMonoidHom
(C := C) hι htarget φ hφ).toMonoidHom =
freeProCZCCompletedFoxRightHom (C := C) hι htarget φ hφThe bundled right homomorphism has the expected underlying monoid homomorphism.
Show Lean proof
rfl@[simp]
theorem freeProCZCCompletedFoxRightHomContinuousMonoidHom_apply (g : F) :
freeProCZCCompletedFoxRightHomContinuousMonoidHom
(C := C) hι htarget φ hφ g =
freeProCZCCompletedFoxRightHom (C := C) hι htarget φ hφ gEvaluation of the bundled right homomorphism.
Show Lean proof
rfl@[simp]
theorem freeProCZCCompletedFoxRightHomContinuousMonoidHom_generator (x : X) :
freeProCZCCompletedFoxRightHomContinuousMonoidHom
(C := C) hι htarget φ hφ (ι x) = φ xThe bundled right homomorphism has the prescribed generator values.
Show Lean proof
by
exact freeProCZCCompletedFoxRightHom_generator (C := C) hι htarget φ hφ xdef freeProCZCCompletedFoxDerivativeVectorContinuousMap :
ContinuousMap F (ZCFreeFoxCoordinates C (X := X) (H := H)) where
toFun := freeProCZCCompletedFoxDerivativeVector (C := C) hι htarget φ hφ
continuous_toFun :=
continuous_freeProCZCCompletedFoxDerivativeVector (C := C) X H hι htarget φ hφThe completed free pro-\(C\) Fox derivative vector is bundled as a continuous map; it is a crossed differential, not a homomorphism.
@[simp]
theorem freeProCZCCompletedFoxDerivativeVectorContinuousMap_apply (g : F) :
freeProCZCCompletedFoxDerivativeVectorContinuousMap
(C := C) hι htarget φ hφ g =
freeProCZCCompletedFoxDerivativeVector (C := C) hι htarget φ hφ gEvaluation of the bundled continuous completed Fox derivative vector.
Show Lean proof
rfl@[simp]
theorem freeProCZCCompletedFoxDerivativeVectorContinuousMap_generator (x : X) :
freeProCZCCompletedFoxDerivativeVectorContinuousMap
(C := C) hι htarget φ hφ (ι x) =
Pi.single x (1 : ZCCompletedGroupAlgebra C H)The bundled continuous completed Fox derivative vector has the prescribed generator values.
Show Lean proof
by
simp only [freeProCZCCompletedFoxDerivativeVectorContinuousMap, ContinuousMap.coe_mk,
freeProCZCCompletedFoxDerivativeVector_generator]
Theorem
FoxDifferential.zcFreeGroupFoxDerivativeVector_eq_freeProCCompletedFoxDerivativeVector_comp_lift
theorem zcFreeGroupFoxDerivativeVector_eq_freeProCCompletedFoxDerivativeVector_comp_lift
(w : FreeGroup X) :
zcFreeGroupFoxDerivativeVector C
((freeProCZCCompletedFoxRightHom (C := C) hι htarget φ hφ).comp
(FreeGroup.lift ι)) w =
freeProCZCCompletedFoxDerivativeVector
(C := C) hι htarget φ hφ ((FreeGroup.lift ι) w)Restricting the continuous completed Fox derivative to the abstract free group generated by the chosen free pro-\(C\) basis recovers the completed free-group Fox derivative.
Show Lean proof
by
let ρ : F →* H :=
freeProCZCCompletedFoxRightHom (C := C) hι htarget φ hφ
let D : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ρ)
(ZCFreeFoxCoordinates C (X := X) (H := H)) :=
freeProCZCCompletedFoxDerivativeVector (C := C) hι htarget φ hφ
let δ : ScalarCrossedHom
(zcCompletedGroupAlgebraScalar C (ρ.comp (FreeGroup.lift ι)))
(ZCFreeFoxCoordinates C (X := X) (H := H)) :=
{ toFun := fun w => D ((FreeGroup.lift ι) w)
map_mul' := by
intro u v
simp [ρ, D, map_mul, MonoidHom.comp_apply] }
have hbasis :
∀ x : X, δ (FreeGroup.of x) =
Pi.single x (1 : ZCCompletedGroupAlgebra C H) := by
intro x
change D ((FreeGroup.lift ι) (FreeGroup.of x)) =
Pi.single x (1 : ZCCompletedGroupAlgebra C H)
rw [FreeGroup.lift_apply_of]
exact freeProCZCCompletedFoxDerivativeVector_generator
(C := C) hι htarget φ hφ x
have hδeq :
δ =
zcFreeGroupFoxDerivativeVector C
(ρ.comp (FreeGroup.lift ι)) :=
zcFreeGroupFoxDerivativeVector_unique
C (ρ.comp (FreeGroup.lift ι)) δ hbasis
exact congrArg
(fun d : ScalarCrossedHom
(zcCompletedGroupAlgebraScalar C (ρ.comp (FreeGroup.lift ι)))
(ZCFreeFoxCoordinates C (X := X) (H := H)) => d w)
hδeq.symmtheorem zcFreeFoxDerivVec_eq_freeProCCompletedFoxDerivVec_comp_lift_mapTarget
(hC : ProCGroups.FiniteGroupClass.Hereditary C)
{K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
(η : H →ₜ* K) (w : FreeGroup X) :
zcFreeGroupFoxDerivativeVector C
(η.toMonoidHom.comp
((freeProCZCCompletedFoxRightHom (C := C) hι htarget φ hφ).comp
(FreeGroup.lift ι))) w =
zcFreeFoxCoordinatesMap (X := X) C hC η
(freeProCZCCompletedFoxDerivativeVector
(C := C) hι htarget φ hφ ((FreeGroup.lift ι) w))Source restriction and target naturality for the continuous completed Fox derivative.
Show Lean proof
by
rw [zcFreeGroupFoxDerivativeVector_mapTarget]
rw [zcFreeGroupFoxDerivativeVector_eq_freeProCCompletedFoxDerivativeVector_comp_lift
(C := C) hι htarget φ hφ w]omit [TopologicalSpace X] in
theorem zcFreeFoxDerivVec_eq_freeProCDerivVecOfConvergingSet_comp_lift
(w : FreeGroup X) :
zcFreeGroupFoxDerivativeVector C
((freeProCZCCompletedFoxRightHomOfConvergingSet
(C := C) hι htarget φ hφconv hφgen).comp
(FreeGroup.lift ι)) w =
freeProCZCCompletedFoxDerivativeVectorOfConvergingSet
(C := C) hι htarget φ hφconv hφgen ((FreeGroup.lift ι) w)Restricting the converging-set continuous completed Fox derivative to the abstract free group generated by the chosen free pro-\(C\) basis recovers the completed free-group Fox derivative.
Show Lean proof
by
let ρ : F →* H :=
freeProCZCCompletedFoxRightHomOfConvergingSet
(C := C) hι htarget φ hφconv hφgen
let D : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ρ)
(ZCFreeFoxCoordinates C (X := X) (H := H)) :=
freeProCZCCompletedFoxDerivativeVectorOfConvergingSet
(C := C) hι htarget φ hφconv hφgen
let δ : ScalarCrossedHom
(zcCompletedGroupAlgebraScalar C (ρ.comp (FreeGroup.lift ι)))
(ZCFreeFoxCoordinates C (X := X) (H := H)) :=
{ toFun := fun w => D ((FreeGroup.lift ι) w)
map_mul' := by
intro u v
simp [ρ, D, map_mul, MonoidHom.comp_apply] }
have hbasis :
∀ x : X, δ (FreeGroup.of x) =
Pi.single x (1 : ZCCompletedGroupAlgebra C H) := by
intro x
change D ((FreeGroup.lift ι) (FreeGroup.of x)) =
Pi.single x (1 : ZCCompletedGroupAlgebra C H)
rw [FreeGroup.lift_apply_of]
exact freeProCZCCompletedFoxDerivativeVectorOfConvergingSet_generator
(C := C) hι htarget φ hφconv hφgen x
have hδeq :
δ =
zcFreeGroupFoxDerivativeVector C
(ρ.comp (FreeGroup.lift ι)) :=
zcFreeGroupFoxDerivativeVector_unique
C (ρ.comp (FreeGroup.lift ι)) δ hbasis
exact congrArg
(fun d : ScalarCrossedHom
(zcCompletedGroupAlgebraScalar C (ρ.comp (FreeGroup.lift ι)))
(ZCFreeFoxCoordinates C (X := X) (H := H)) => d w)
hδeq.symmomit [TopologicalSpace X] in
theorem zcFreeFoxDerivVec_eq_freeProCDerivVecOfConvergingSet_comp_lift_mapTarget
(hC : ProCGroups.FiniteGroupClass.Hereditary C)
{K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
(η : H →ₜ* K) (w : FreeGroup X) :
zcFreeGroupFoxDerivativeVector C
(η.toMonoidHom.comp
((freeProCZCCompletedFoxRightHomOfConvergingSet
(C := C) hι htarget φ hφconv hφgen).comp
(FreeGroup.lift ι))) w =
zcFreeFoxCoordinatesMap (X := X) C hC η
(freeProCZCCompletedFoxDerivativeVectorOfConvergingSet
(C := C) hι htarget φ hφconv hφgen ((FreeGroup.lift ι) w))Source restriction and target naturality for the converging-set continuous completed Fox derivative.
Show Lean proof
by
rw [zcFreeGroupFoxDerivativeVector_mapTarget]
rw [zcFreeFoxDerivVec_eq_freeProCDerivVecOfConvergingSet_comp_lift
(C := C) hι htarget φ hφconv hφgen w]omit [TopologicalSpace X] in
theorem zcFreeFoxDerivVec_eq_freeProCDerivVecViaClosedGen_comp_lift
(w : FreeGroup X) :
zcFreeGroupFoxDerivativeVector C
((freeProCZCCompletedFoxRightHomViaClosedGenerated
(C := C) hι φ htarget hφconv).comp
(FreeGroup.lift ι)) w =
freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
(C := C) hι φ htarget hφconv ((FreeGroup.lift ι) w)Restricting the closed-generated continuous completed Fox derivative to the abstract free group generated by the chosen free pro-\(C\) basis recovers the completed free-group Fox derivative.
Show Lean proof
by
let ρ : F →* H :=
freeProCZCCompletedFoxRightHomViaClosedGenerated
(C := C) hι φ htarget hφconv
let D : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ρ)
(ZCFreeFoxCoordinates C (X := X) (H := H)) :=
freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
(C := C) hι φ htarget hφconv
let δ : ScalarCrossedHom
(zcCompletedGroupAlgebraScalar C (ρ.comp (FreeGroup.lift ι)))
(ZCFreeFoxCoordinates C (X := X) (H := H)) :=
{ toFun := fun w => D ((FreeGroup.lift ι) w)
map_mul' := by
intro u v
simp [ρ, D, map_mul, MonoidHom.comp_apply] }
have hbasis :
∀ x : X, δ (FreeGroup.of x) =
Pi.single x (1 : ZCCompletedGroupAlgebra C H) := by
intro x
change D ((FreeGroup.lift ι) (FreeGroup.of x)) =
Pi.single x (1 : ZCCompletedGroupAlgebra C H)
rw [FreeGroup.lift_apply_of]
exact freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated_generator
(C := C) hι φ htarget hφconv x
have hδeq :
δ =
zcFreeGroupFoxDerivativeVector C
(ρ.comp (FreeGroup.lift ι)) :=
zcFreeGroupFoxDerivativeVector_unique
C (ρ.comp (FreeGroup.lift ι)) δ hbasis
exact congrArg
(fun d : ScalarCrossedHom
(zcCompletedGroupAlgebraScalar C (ρ.comp (FreeGroup.lift ι)))
(ZCFreeFoxCoordinates C (X := X) (H := H)) => d w)
hδeq.symmomit [TopologicalSpace X] in
theorem zcFreeFoxDerivVec_eq_freeProCDerivVecViaClosedGen_comp_lift_mapTarget
(hC : ProCGroups.FiniteGroupClass.Hereditary C)
{K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
(η : H →ₜ* K) (w : FreeGroup X) :
zcFreeGroupFoxDerivativeVector C
(η.toMonoidHom.comp
((freeProCZCCompletedFoxRightHomViaClosedGenerated
(C := C) hι φ htarget hφconv).comp
(FreeGroup.lift ι))) w =
zcFreeFoxCoordinatesMap (X := X) C hC η
(freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
(C := C) hι φ htarget hφconv ((FreeGroup.lift ι) w))Source restriction and target naturality for the closed-generated continuous completed Fox derivative.
Show Lean proof
by
rw [zcFreeGroupFoxDerivativeVector_mapTarget]
rw [zcFreeFoxDerivVec_eq_freeProCDerivVecViaClosedGen_comp_lift
(C := C) hι φ htarget hφconv w]