FoxDifferential.Completed.Comparison.QuotientFamily
This module supplies the topological part of the construction. It checks continuity and stagewise neighborhood properties so that the completed object inherits the required topology.
structure ZCFiniteStageQuotientBundle where
targetTopology : TopologicalSpace (finiteFoxStageTargetQuotient (X := X) N)
targetIsTopologicalGroup :
@IsTopologicalGroup (finiteFoxStageTargetQuotient (X := X) N)
targetTopology inferInstanceA bundled finite-stage quotient family for source-stage comparison theorems. The purpose is to carry the topology and topological-group structure on the quotient target once, instead of repeating these hypotheses at every comparison theorem.
abbrev Target (_B : ZCFiniteStageQuotientBundle N) : Type u :=
finiteFoxStageTargetQuotient (X := X) NThe target quotient carried by a finite-stage quotient bundle.
abbrev Index (B : ZCFiniteStageQuotientBundle N) : Type u :=
letI : TopologicalSpace (Target (N := N) B) := B.targetTopology
ZCCompletedGroupAlgebraIndex C (Target (N := N) B)The completed pro-\(C\) stage indices for the bundled target quotient.
abbrev CompletedGroupAlgebra (B : ZCFiniteStageQuotientBundle N) : Type u :=
letI : TopologicalSpace (Target (N := N) B) := B.targetTopology
letI : IsTopologicalGroup (Target (N := N) B) := B.targetIsTopologicalGroup
ZCCompletedGroupAlgebra C (Target (N := N) B)The completed group algebra of the bundled target quotient.
theorem scalarStage_apply
(B : ZCFiniteStageQuotientBundle N)
(j : B.Index C) (w : FreeGroup X) :
letI : TopologicalSpace (Target (N := N) B)The scalar stage attached to the quotient bundle is evaluated at the corresponding finite quotient and coefficient stage.
Show proof
B.targetTopology
letI : IsTopologicalGroup (Target (N := N) B) := B.targetIsTopologicalGroup
zcCompletedGroupAlgebraScalarStage C N j w =
(letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
modNCompletedGroupAlgebraStageMapInClass j.1.modulus
(zcFiniteStageTarget X N) C j.2
(finiteFoxStageCoefficient (X := X) N j.1.modulus w)) := by
letI : TopologicalSpace (Target (N := N) B) := B.targetTopology
letI : IsTopologicalGroup (Target (N := N) B) := B.targetIsTopologicalGroup
exact zcCompletedGroupAlgebraScalarStage_apply (C := C) (X := X) N j wProof. Unfold the finite-stage quotient bundle. The bundle stores the target quotient, its completed group algebra, and the relevant finite-stage index data so that comparison theorems can reuse the same topological and algebraic hypotheses. Projection and reduction statements are then checked by applying the stored finite-stage projections and the compatible quotient maps.
□theorem derivative_finiteStageProjection
(B : ZCFiniteStageQuotientBundle N)
(j : B.Index C) (i : X) (w : FreeGroup X) :
letI : TopologicalSpace (Target (N := N) B)Completed derivative projection theorem, using the bundled quotient-family hypotheses.
Show proof
B.targetTopology
letI : IsTopologicalGroup (Target (N := N) B) := B.targetIsTopologicalGroup
zcCompletedGroupAlgebraProjection C (zcFiniteStageTarget X N) j
(zcFreeGroupFoxDerivative C (QuotientGroup.mk' N) i w) =
(letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
modNCompletedGroupAlgebraStageMapInClass j.1.modulus
(zcFiniteStageTarget X N) C j.2
(finiteFoxStageDerivative (X := X) N j.1.modulus i w)) := by
letI : TopologicalSpace (Target (N := N) B) := B.targetTopology
letI : IsTopologicalGroup (Target (N := N) B) := B.targetIsTopologicalGroup
exact zcFreeGroupFoxDerivative_finiteStageProjection (C := C) (X := X) N j i wProof. Unfold the finite-stage quotient bundle. The bundle stores the target quotient, its completed group algebra, and the relevant finite-stage index data so that comparison theorems can reuse the same topological and algebraic hypotheses. Projection and reduction statements are then checked by applying the stored finite-stage projections and the compatible quotient maps.
□theorem derivativeVector_finiteStageProjection
(B : ZCFiniteStageQuotientBundle N)
(j : B.Index C) (w : FreeGroup X) :
letI : TopologicalSpace (Target (N := N) B)Completed derivative-vector projection theorem, using the bundled quotient-family hypotheses.
Show proof
B.targetTopology
letI : IsTopologicalGroup (Target (N := N) B) := B.targetIsTopologicalGroup
(fun i : X =>
zcCompletedGroupAlgebraProjection C (zcFiniteStageTarget X N) j
(zcFreeGroupFoxDerivativeVector C (QuotientGroup.mk' N) w i)) =
fun i : X =>
letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
modNCompletedGroupAlgebraStageMapInClass j.1.modulus
(zcFiniteStageTarget X N) C j.2
(finiteFoxStageDerivative (X := X) N j.1.modulus i w) := by
letI : TopologicalSpace (Target (N := N) B) := B.targetTopology
letI : IsTopologicalGroup (Target (N := N) B) := B.targetIsTopologicalGroup
exact zcFreeGroupFoxDerivativeVector_finiteStageProjection (C := C) (X := X) N j wProof. Unfold the finite-stage quotient bundle. The bundle stores the target quotient, its completed group algebra, and the relevant finite-stage index data so that comparison theorems can reuse the same topological and algebraic hypotheses. Projection and reduction statements are then checked by applying the stored finite-stage projections and the compatible quotient maps.
□theorem derivative_finiteStageProjection_discreteReduction
(B : ZCFiniteStageQuotientBundle N)
(j : B.Index C) (i : X) (w : FreeGroup X) :
letI : TopologicalSpace (Target (N := N) B)Discrete-reduction derivative projection theorem, using the bundled quotient-family hypotheses.
Show proof
B.targetTopology
letI : IsTopologicalGroup (Target (N := N) B) := B.targetIsTopologicalGroup
zcCompletedGroupAlgebraProjection C (zcFiniteStageTarget X N) j
(zcFreeGroupFoxDerivative C (QuotientGroup.mk' N) i w) =
(letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
modNCompletedGroupAlgebraStageMapInClass j.1.modulus
(zcFiniteStageTarget X N) C j.2
(finiteFoxStageGroupRingReduction (X := X) N j.1.modulus
(FoxCalculus.relativeFreeGroupFoxDerivative
(H := zcFiniteStageTarget X N) X (QuotientGroup.mk' N) w i))) := by
letI : TopologicalSpace (Target (N := N) B) := B.targetTopology
letI : IsTopologicalGroup (Target (N := N) B) := B.targetIsTopologicalGroup
exact zcFreeGroupFoxDerivative_finiteStageProjection_discreteReduction
(C := C) (X := X) N i w jProof. Unfold the finite-stage quotient bundle. The bundle stores the target quotient, its completed group algebra, and the relevant finite-stage index data so that comparison theorems can reuse the same topological and algebraic hypotheses. Projection and reduction statements are then checked by applying the stored finite-stage projections and the compatible quotient maps.
□theorem derivativeVector_finiteStageProjection_discreteReduction
(B : ZCFiniteStageQuotientBundle N)
(j : B.Index C) (w : FreeGroup X) :
letI : TopologicalSpace (Target (N := N) B)Discrete-reduction derivative-vector projection theorem, using the bundled quotient-family hypotheses.
Show proof
B.targetTopology
letI : IsTopologicalGroup (Target (N := N) B) := B.targetIsTopologicalGroup
(fun i : X =>
zcCompletedGroupAlgebraProjection C (zcFiniteStageTarget X N) j
(zcFreeGroupFoxDerivativeVector C (QuotientGroup.mk' N) w i)) =
fun i : X =>
letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
modNCompletedGroupAlgebraStageMapInClass j.1.modulus
(zcFiniteStageTarget X N) C j.2
(finiteFoxStageGroupRingReduction (X := X) N j.1.modulus
(FoxCalculus.relativeFreeGroupFoxDerivative
(H := zcFiniteStageTarget X N) X (QuotientGroup.mk' N) w i)) := by
letI : TopologicalSpace (Target (N := N) B) := B.targetTopology
letI : IsTopologicalGroup (Target (N := N) B) := B.targetIsTopologicalGroup
exact zcFreeGroupFoxDerivativeVector_finiteStageProjection_discreteReduction
(C := C) (X := X) N w jProof. Unfold the finite-stage quotient bundle. The bundle stores the target quotient, its completed group algebra, and the relevant finite-stage index data so that comparison theorems can reuse the same topological and algebraic hypotheses. Projection and reduction statements are then checked by applying the stored finite-stage projections and the compatible quotient maps.
□