FoxDifferential/Completed/Comparison/QuotientFamily.lean

1import FoxDifferential.Completed.Comparison.DiscreteCompletion

3/-

4PUBLIC_PAGE_SNAPSHOT

5generated_at: 2026-05-27T09:47:29+09:00

6lean_source: lean4/FoxDifferential/Completed/Comparison/QuotientFamily.lean

7translation_root: data/translation

8purpose: identifies the local data snapshot used to build pages/

9placement: after imports, never before imports

10-/

11/-!

12# Discrete-completed comparison

14Crossed differentials, universal differential modules, Fox boundaries, Euler formulas, and Jacobians are the common algebraic layer used by Crowell and metabelian applications.

15-/

16namespace FoxDifferential

18noncomputable section

20universe u

22section FiniteStageQuotientBundle

24variable {X : Type u} [DecidableEq X]

25variable (N : Subgroup (FreeGroup X)) [N.Normal]

27/-- A bundled finite-stage quotient family for source-stage comparison theorems.

29The point is to carry the topology and topological-group structure on the quotient target once,

30instead of repeating these hypotheses at every comparison theorem. -/

31structure ZCFiniteStageQuotientBundle where

32 targetTopology : TopologicalSpace (finiteFoxStageTargetQuotient (X := X) N)

33 targetIsTopologicalGroup :

34 @IsTopologicalGroup (finiteFoxStageTargetQuotient (X := X) N)

35 targetTopology inferInstance

37namespace ZCFiniteStageQuotientBundle

39variable {N}

40variable (C : ProCGroups.FiniteGroupClass.{u})

42/-- The target quotient carried by a finite-stage quotient bundle. -/

43abbrev Target (_B : ZCFiniteStageQuotientBundle N) : Type u :=

44 finiteFoxStageTargetQuotient (X := X) N

46/-- The completed pro-`C` stage indices for the bundled target quotient. -/

47abbrev Index (B : ZCFiniteStageQuotientBundle N) : Type u :=

48 letI : TopologicalSpace (Target (N := N) B) := B.targetTopology

49 ZCCompletedGroupAlgebraIndex C (Target (N := N) B)

51/-- The completed group algebra of the bundled target quotient. -/

52abbrev CompletedGroupAlgebra (B : ZCFiniteStageQuotientBundle N) : Type u :=

53 letI : TopologicalSpace (Target (N := N) B) := B.targetTopology

54 letI : IsTopologicalGroup (Target (N := N) B) := B.targetIsTopologicalGroup

55 ZCCompletedGroupAlgebra C (Target (N := N) B)

57/-- Scalar projection theorem, using the bundled quotient-family hypotheses. -/

58theorem scalarStage_apply

59 (B : ZCFiniteStageQuotientBundle N)

60 (j : B.Index C) (w : FreeGroup X) :

61 letI : TopologicalSpace (Target (N := N) B) := B.targetTopology

62 letI : IsTopologicalGroup (Target (N := N) B) := B.targetIsTopologicalGroup

63 zcCompletedGroupAlgebraScalarStage C N j w =

64 (letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩

65 modNCompletedGroupAlgebraStageMapInClass j.1.modulus

66 (zcFiniteStageTarget X N) C j.2

67 (finiteFoxStageCoefficient (X := X) N j.1.modulus w)) := by

68 letI : TopologicalSpace (Target (N := N) B) := B.targetTopology

69 letI : IsTopologicalGroup (Target (N := N) B) := B.targetIsTopologicalGroup

70 exact zcCompletedGroupAlgebraScalarStage_apply (C := C) (X := X) N j w

72/-- Completed derivative projection theorem, using the bundled quotient-family hypotheses. -/

73theorem derivative_finiteStageProjection

74 (B : ZCFiniteStageQuotientBundle N)

75 (j : B.Index C) (i : X) (w : FreeGroup X) :

76 letI : TopologicalSpace (Target (N := N) B) := B.targetTopology

77 letI : IsTopologicalGroup (Target (N := N) B) := B.targetIsTopologicalGroup

78 zcCompletedGroupAlgebraProjection C (zcFiniteStageTarget X N) j

79 (zcFreeGroupFoxDerivative C (QuotientGroup.mk' N) i w) =

80 (letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩

81 modNCompletedGroupAlgebraStageMapInClass j.1.modulus

82 (zcFiniteStageTarget X N) C j.2

83 (finiteFoxStageDerivative (X := X) N j.1.modulus i w)) := by

84 letI : TopologicalSpace (Target (N := N) B) := B.targetTopology

85 letI : IsTopologicalGroup (Target (N := N) B) := B.targetIsTopologicalGroup

86 exact zcFreeGroupFoxDerivative_finiteStageProjection (C := C) (X := X) N j i w

88/-- Completed derivative-vector projection theorem, using the bundled quotient-family

89hypotheses. -/

90theorem derivativeVector_finiteStageProjection

91 (B : ZCFiniteStageQuotientBundle N)

92 (j : B.Index C) (w : FreeGroup X) :

93 letI : TopologicalSpace (Target (N := N) B) := B.targetTopology

94 letI : IsTopologicalGroup (Target (N := N) B) := B.targetIsTopologicalGroup

95 (fun i : X =>

96 zcCompletedGroupAlgebraProjection C (zcFiniteStageTarget X N) j

97 (zcFreeGroupFoxDerivativeVector C (QuotientGroup.mk' N) w i)) =

98 fun i : X =>

99 letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩

100 modNCompletedGroupAlgebraStageMapInClass j.1.modulus

101 (zcFiniteStageTarget X N) C j.2

102 (finiteFoxStageDerivative (X := X) N j.1.modulus i w) := by

103 letI : TopologicalSpace (Target (N := N) B) := B.targetTopology

104 letI : IsTopologicalGroup (Target (N := N) B) := B.targetIsTopologicalGroup

105 exact zcFreeGroupFoxDerivativeVector_finiteStageProjection (C := C) (X := X) N j w

106

107/-- Discrete-reduction derivative projection theorem, using the bundled quotient-family

108hypotheses. -/

109theorem derivative_finiteStageProjection_discreteReduction

110 (B : ZCFiniteStageQuotientBundle N)

111 (j : B.Index C) (i : X) (w : FreeGroup X) :

112 letI : TopologicalSpace (Target (N := N) B) := B.targetTopology

113 letI : IsTopologicalGroup (Target (N := N) B) := B.targetIsTopologicalGroup

114 zcCompletedGroupAlgebraProjection C (zcFiniteStageTarget X N) j

115 (zcFreeGroupFoxDerivative C (QuotientGroup.mk' N) i w) =

116 (letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩

117 modNCompletedGroupAlgebraStageMapInClass j.1.modulus

118 (zcFiniteStageTarget X N) C j.2

119 (finiteFoxStageGroupRingReduction (X := X) N j.1.modulus

120 (FoxCalculus.relativeFreeGroupFoxDerivative

121 (H := zcFiniteStageTarget X N) X (QuotientGroup.mk' N) w i))) := by

122 letI : TopologicalSpace (Target (N := N) B) := B.targetTopology

123 letI : IsTopologicalGroup (Target (N := N) B) := B.targetIsTopologicalGroup

124 exact zcFreeGroupFoxDerivative_finiteStageProjection_discreteReduction

125 (C := C) (X := X) N i w j

126

127/-- Discrete-reduction derivative-vector projection theorem, using the bundled quotient-family

128hypotheses. -/

129theorem derivativeVector_finiteStageProjection_discreteReduction

130 (B : ZCFiniteStageQuotientBundle N)

131 (j : B.Index C) (w : FreeGroup X) :

132 letI : TopologicalSpace (Target (N := N) B) := B.targetTopology

133 letI : IsTopologicalGroup (Target (N := N) B) := B.targetIsTopologicalGroup

134 (fun i : X =>

135 zcCompletedGroupAlgebraProjection C (zcFiniteStageTarget X N) j

136 (zcFreeGroupFoxDerivativeVector C (QuotientGroup.mk' N) w i)) =

137 fun i : X =>

138 letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩

139 modNCompletedGroupAlgebraStageMapInClass j.1.modulus

140 (zcFiniteStageTarget X N) C j.2

141 (finiteFoxStageGroupRingReduction (X := X) N j.1.modulus

142 (FoxCalculus.relativeFreeGroupFoxDerivative

143 (H := zcFiniteStageTarget X N) X (QuotientGroup.mk' N) w i)) := by

144 letI : TopologicalSpace (Target (N := N) B) := B.targetTopology

145 letI : IsTopologicalGroup (Target (N := N) B) := B.targetIsTopologicalGroup

146 exact zcFreeGroupFoxDerivativeVector_finiteStageProjection_discreteReduction

147 (C := C) (X := X) N w j

148

149end ZCFiniteStageQuotientBundle

150

151end FiniteStageQuotientBundle

152

153end

154

155end FoxDifferential