ParameterizedSquareFilling.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Boundary-prescribed fillings depend continuously on parameters. This gives literal square-prism extensions, rather than formal cellular coefficients.

lemma OAI.HyperbolicObstruction.SquarePathFilling.quotient_zero line 16
lemma OAI.HyperbolicObstruction.SquarePathFilling.quotient_one line 18

def OAI.HyperbolicObstruction.SquarePathFilling.unfill line 23

Source documentation

Recover the relative path homotopy from a genuine square having the specified four boundary sides.

def unfill (f : C(I × I,X))
    (hb : ∀ x, f (x,0) = p x) (hl : ∀ x, f (0,x) = q x)
    (hr : ∀ x, f (1,x) = r x) (ht : ∀ x, f (x,1) = s x) :
    (p.trans r).Homotopy (q.trans s) where
…

lemma OAI.HyperbolicObstruction.SquarePathFilling.fill_unfill line 73
def OAI.HyperbolicObstruction.SquarePathFilling.paramQuotient line 85
Source documentation
The product quotient is an actual compact closed quotient, ensuring continuous families of fillings without a choice-continuity assumption.
```
def paramQuotient : C(T × (I × I),T × (I × I)) :=
…
```
lemma OAI.HyperbolicObstruction.SquarePathFilling.paramQuotient_surjective line 88
lemma OAI.HyperbolicObstruction.SquarePathFilling.paramQuotient_isQuotientMap line 92
lemma OAI.HyperbolicObstruction.SquarePathFilling.loopFamily_fiber line 98
def OAI.HyperbolicObstruction.SquarePathFilling.paramFill line 106
Source documentation
A family of loop-space paths determines a family of actual square maps.
```
def paramFill (F : C(T × I,Path b b)) : C(T × (I × I),X) where
…
```
lemma OAI.HyperbolicObstruction.SquarePathFilling.paramFill_quotient line 121