Cover.lean`

31 declarations, 0 contain sorry, 0 declared as axioms

Actual characteristic-cell lifts for an ordinary Whitehead CW complex. This is a dependency toward (not an assumption replacing) the arbitrary-CW presentation and cellular-cycle bridge.

abbrev OAI.EilenbergGanea.CWCover.Disk line 20
def OAI.EilenbergGanea.CWCover.diskCenter line 22
instance OAI.EilenbergGanea.CWCover.diskContractible line 24
instance OAI.EilenbergGanea.CWCover.diskLocallyPathConnected line 27
abbrev OAI.EilenbergGanea.CWCover.Cell line 33
def OAI.EilenbergGanea.CWCover.characteristic line 35
abbrev OAI.EilenbergGanea.CWCover.LiftedCell line 39
def OAI.EilenbergGanea.CWCover.cellLift line 41
theorem OAI.EilenbergGanea.CWCover.cellLift_center line 44
theorem OAI.EilenbergGanea.CWCover.cellLift_project line 48
def OAI.EilenbergGanea.CWCover.liftedOpenCell line 52
theorem OAI.EilenbergGanea.CWCover.cellLift_injOn line 55
theorem OAI.EilenbergGanea.CWCover.projection_liftedOpenCell line 66
theorem OAI.EilenbergGanea.CWCover.cellLift_unique line 77
abbrev OAI.EilenbergGanea.CWCover.CellDisks line 98
def OAI.EilenbergGanea.CWCover.characteristicSum line 101
theorem OAI.EilenbergGanea.CWCover.characteristicSum_continuous line 104
theorem OAI.EilenbergGanea.CWCover.characteristicSum_surjective line 108
theorem OAI.EilenbergGanea.CWCover.characteristicSum_quotient line 117
Source documentation
The ordinary CW topology is exactly the quotient topology of the disjoint union of its closed characteristic disks.
```
theorem characteristicSum_quotient : IsQuotientMap (characteristicSum (X := X)) := by
…
```
Mentions: OAI.EilenbergGanea.CWCover.characteristicSum
theorem OAI.EilenbergGanea.CWCover.exists_cellLift_through line 141
Source documentation
Every point over a characteristic disk is hit by exactly one lift of that disk with the specified base cell.
```
theorem exists_cellLift_through {n : ℕ} (i : Cell (X := X) n) (z : Disk n)
…
```
Mentions: OAI.EilenbergGanea.CWCover.Cell, OAI.EilenbergGanea.CWCover.Disk
theorem OAI.EilenbergGanea.CWCover.isOpen_of_cellLift_preimages line 157
Source documentation
The pulled-back weak topology can be proved before constructing the lifted CW structure: openness is detected by the actual lifted disks.
```
theorem isOpen_of_cellLift_preimages {A : Set E}
    (hA : ∀ n (c : LiftedCell (p := p) n), IsOpen (cellLift cov c ⁻¹' A)) : IsOpen A := by
…
```
Mentions: OAI.EilenbergGanea.CWCover.LiftedCell, OAI.EilenbergGanea.CWCover.cellLift
theorem OAI.EilenbergGanea.CWCover.isOpen_iff_cellLift_preimages line 201
def OAI.EilenbergGanea.CWCover.liftedMapFun line 214
Source documentation
Extend the genuine lifted characteristic disk outside its domain only so that it can be used in Mathlib's ordinary PartialEquiv CW convention.
```
def liftedMapFun {n : ℕ} (c : LiftedCell (p := p) n) (z : Fin n → ℝ) : E :=
…
```
Mentions: OAI.EilenbergGanea.CWCover.LiftedCell
theorem OAI.EilenbergGanea.CWCover.liftedMapFun_disk line 217
theorem OAI.EilenbergGanea.CWCover.liftedMapFun_continuousOn line 221
def OAI.EilenbergGanea.CWCover.liftedMap line 230
Source documentation
The real inverse chart is obtained by projecting to the ordinary base chart. It is not chosen by an abstract set-theoretic inverse.
```
def liftedMap {n : ℕ} (c : LiftedCell (p := p) n) : PartialEquiv (Fin n → ℝ) E where
…
```
Mentions: OAI.EilenbergGanea.CWCover.LiftedCell
theorem OAI.EilenbergGanea.CWCover.liftedMap_source line 259
theorem OAI.EilenbergGanea.CWCover.liftedMap_target line 262
theorem OAI.EilenbergGanea.CWCover.liftedMap_continuousOn_symm line 265
theorem OAI.EilenbergGanea.CWCover.liftedOpenCells_disjoint line 274
theorem OAI.EilenbergGanea.CWCover.t2Space line 306
Source documentation
The total space of an ordinary covering of a Hausdorff space is Hausdorff; no Hausdorff hypothesis is added to the source's definition of K(G,1).
```
theorem t2Space [T2Space X] : T2Space E := by
…
```