Continuous Local Factor Gluing

Abstract

Compatible continuous local factors glue uniquely and factor the target globally.

Theorem 1.1 (Continuous local factors glue uniquely).

$$\forall I\in \mathrm{Type}\left(\right),X\in \mathrm{Type}\left(\right),B\in \mathrm{Type}\left(\right),Y\in \mathrm{Type}\left(\right),q\in X\to B,T\in X\to Y,U\in I\to \left(B\to \mathrm{Prop}\left(\right)\right),f\in \forall i:I,\mathrm{ContinuousMap}\left(\mathrm{Subtype}\left(U\left(i\right)\right),Y\right),\left(\left(\mathrm{TopologicalSpace}\left(B\right)\wedge \mathrm{TopologicalSpace}\left(Y\right)\right)\wedge \left(\left(\forall i\in I,\mathrm{IsOpen}\left(U\left(i\right)\right)\right)\wedge \left(\mathrm{iUnion}\left(U\right)=\mathrm{univ}\left(B\right)\wedge \left(\mathrm{Surjective}\left(q\right)\wedge \left(\forall i\in I,x\in X,\mathrm{mem}\left(q\left(x\right),U\left(i\right)\right)\Rightarrow T\left(x\right)=\mathrm{localApply}\left(f,i,q\left(x\right)\right)\right)\right)\right)\right)\right)\Rightarrow \left(\left(\forall i\in I,j\in I,b\in B,\left(\mathrm{mem}\left(b,U\left(i\right)\right)\wedge \mathrm{mem}\left(b,U\left(j\right)\right)\right)\Rightarrow \mathrm{localApply}\left(f,i,b\right)=\mathrm{localApply}\left(f,j,b\right)\right)\wedge \exists !g:\mathrm{ContinuousMap}\left(B,Y\right),\left(\forall i\in I,b\in B,\mathrm{mem}\left(b,U\left(i\right)\right)\Rightarrow g\left(b\right)=\mathrm{localApply}\left(f,i,b\right)\right)\wedge T=\mathrm{compose}\left(g,q\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Gluing/ContinuousLocalFactorGluing.continuous_local_factors_glue_uniquely (✓ std3). ∎

Source. Repository-derived.

Commentary.

The local factors are continuous maps on the exact cover subtypes. Surjectivity and the shared target factorization invoke the frozen overlap theorem, giving equality on every pairwise intersection.

The domains are publicly open and cover the base. Mathlib’s canonical continuous-map lift therefore glues the local maps, and its computation rule states that the global map restricts to each local factor.

Cover membership proves uniqueness pointwise. Applying the same local computation rule at q(x), together with the supplied local factorization equation, proves the public identity T = f composed with q.

References

• Truth anchor: D5/S3/ConceptDynamics/Gluing/ContinuousLocalFactorGluing.continuous_local_factors_glue_uniquely
• Dependency: D5/S3/ConceptDynamics/Gluing/LocalFactorOverlapCompatibility