OAI/Algebra/GroupRing/CylinderRetention.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.TorsionFreeZeroDivisors.CylinderRetention.extends_of_path_family line 22

   Source documentation

   Converse to the cylinder filling construction: an extension of the family of paths, with its specified ends, extends the entire cylinder boundary.

   theorem extends_of_path_family (a : C(Sphere n,C(unitInterval,Y)))
       (b : C(Disk n,Y × Y)) (h : ∀ x, pathEndpoint (a x) = b (boundary n x))
       (e : C(Disk n,C(unitInterval,Y))) (he : ∀ x, e (boundary n x) = a x)
       (hend : ∀ x, pathEndpoint (e x) = b x) :
       SphereTopology.Extends (cylinderBoundaryMap a b h) := by
   …

2. def OAI.TorsionFreeZeroDivisors.CylinderRetention.firstHalf line 50
3. def OAI.TorsionFreeZeroDivisors.CylinderRetention.secondHalf line 53
4. def OAI.TorsionFreeZeroDivisors.CylinderRetention.mid line 56
5. lemma OAI.TorsionFreeZeroDivisors.CylinderRetention.firstHalf_zero line 57
6. lemma OAI.TorsionFreeZeroDivisors.CylinderRetention.firstHalf_one line 58
7. lemma OAI.TorsionFreeZeroDivisors.CylinderRetention.secondHalf_zero line 59
8. lemma OAI.TorsionFreeZeroDivisors.CylinderRetention.secondHalf_one line 60
9. def OAI.TorsionFreeZeroDivisors.CylinderRetention.restrictPaths line 62
10. lemma OAI.TorsionFreeZeroDivisors.CylinderRetention.restrictPaths_apply line 65
11. def OAI.TorsionFreeZeroDivisors.CylinderRetention.leftEnds line 69
12. def OAI.TorsionFreeZeroDivisors.CylinderRetention.rightEnds line 71
13. lemma OAI.TorsionFreeZeroDivisors.CylinderRetention.left_compatible line 78
14. lemma OAI.TorsionFreeZeroDivisors.CylinderRetention.right_compatible line 87
15. theorem OAI.TorsionFreeZeroDivisors.CylinderRetention.extends_of_capped_halves line 98

    Source documentation

    If both spheres cut and capped by the SAME middle disk extend, so does the original sphere. This is a topological gluing statement, not word reduction.

    theorem extends_of_capped_halves
        (hL : SphereTopology.Extends (cylinderBoundaryMap (restrictPaths a firstHalf)
          (leftEnds b k) (left_compatible a b h k hk)))
        (hR : SphereTopology.Extends (cylinderBoundaryMap (restrictPaths a secondHalf)
          (rightEnds b k) (right_compatible a b h k hk))) :
        SphereTopology.Extends (cylinderBoundaryMap a b h) := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.CylinderRetention.restrictPaths, OAI.TorsionFreeZeroDivisors.CylinderRetention.firstHalf, OAI.TorsionFreeZeroDivisors.CylinderRetention.leftEnds, OAI.TorsionFreeZeroDivisors.CylinderRetention.left_compatible, OAI.TorsionFreeZeroDivisors.CylinderRetention.secondHalf, OAI.TorsionFreeZeroDivisors.CylinderRetention.rightEnds, OAI.TorsionFreeZeroDivisors.CylinderRetention.right_compatible

16. theorem OAI.TorsionFreeZeroDivisors.CylinderRetention.essential_capped_half line 149

    Source documentation

    A nonextendable sphere retains an essential capped component.

    theorem essential_capped_half
        (hess : ¬ SphereTopology.Extends (cylinderBoundaryMap a b h)) :
        (¬ SphereTopology.Extends (cylinderBoundaryMap (restrictPaths a firstHalf)
          (leftEnds b k) (left_compatible a b h k hk))) ∨
        (¬ SphereTopology.Extends (cylinderBoundaryMap (restrictPaths a secondHalf)
          (rightEnds b k) (right_compatible a b h k hk))) := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.CylinderRetention.restrictPaths, OAI.TorsionFreeZeroDivisors.CylinderRetention.firstHalf, OAI.TorsionFreeZeroDivisors.CylinderRetention.leftEnds, OAI.TorsionFreeZeroDivisors.CylinderRetention.left_compatible, OAI.TorsionFreeZeroDivisors.CylinderRetention.secondHalf, OAI.TorsionFreeZeroDivisors.CylinderRetention.rightEnds, OAI.TorsionFreeZeroDivisors.CylinderRetention.right_compatible

17. theorem OAI.TorsionFreeZeroDivisors.CylinderRetention.exists_common_cap line 160

    Source documentation

    A common contractible cone supplies one and the same middle cap to both pieces. No universal-cover homology comparison is needed for this gluing proof.

    theorem exists_common_cap {Z : Type*} [TopologicalSpace Z] [ContractibleSpace Z]
        [Nonempty (Sphere n)] (j : C(Z,Y)) (m : C(Sphere n,Z))
        (hm : ∀ x, j (m x) = a x mid) :
        ∃ k : C(Disk n,Y), ∀ x, k (boundary n x) = a x mid := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.CylinderRetention.mid