CoverTopology.lean`

77 declarations, 0 contain sorry, 0 declared as axioms

def OAI.EilenbergGanea.CWCover.diskContraction line 16
theorem OAI.EilenbergGanea.CWCover.diskContraction_zero line 23
theorem OAI.EilenbergGanea.CWCover.diskContraction_one line 27
abbrev OAI.EilenbergGanea.CWCover.CellPullback line 32
def OAI.EilenbergGanea.CWCover.cellPullbackHomotopy line 35
def OAI.EilenbergGanea.CWCover.cellPullbackStart line 40
theorem OAI.EilenbergGanea.CWCover.cellPullbackHomotopy_zero line 43
def OAI.EilenbergGanea.CWCover.cellEndpoint line 49
theorem OAI.EilenbergGanea.CWCover.cellEndpoint_project line 53
def OAI.EilenbergGanea.CWCover.cellSheet line 63
Source documentation
The sheet-coordinate of a point on a lifted characteristic disk is continuous, including along the disk's nonembedded attaching boundary.
```
def cellSheet {n : ℕ} (i : Cell (X := X) n) :
…
```
Mentions: OAI.EilenbergGanea.CWCover.Cell
theorem OAI.EilenbergGanea.CWCover.cellSheet_lift line 69
Source documentation
Sheet coordinates identify the actual origin of the unique lifted disk.
```
theorem cellSheet_lift {n : ℕ} (c : LiftedCell (p := p) n) (z : Disk n) :
…
```
Mentions: OAI.EilenbergGanea.CWCover.LiftedCell, OAI.EilenbergGanea.CWCover.Disk
theorem OAI.EilenbergGanea.CWCover.finite_touchingSheets line 106
Source documentation
A compact subset meets only finitely many sheets over each fixed closed characteristic disk. Boundary points are included; the cell need not be regular.
```
theorem finite_touchingSheets {n : ℕ} (i : Cell (X := X) n) {K : Set E} (hK : IsCompact K) :
…
```
Mentions: OAI.EilenbergGanea.CWCover.Cell
theorem OAI.EilenbergGanea.CWCover.liftedMap_image_disk line 144
theorem OAI.EilenbergGanea.CWCover.liftedMap_image_ball line 154
theorem OAI.EilenbergGanea.CWCover.lifted_mapsTo line 160
Source documentation
Compactness of the lifted boundary supplies the actual closure-finiteness axiom, without assuming a locally finite or finite-cell classifying complex.
```
theorem lifted_mapsTo (n : ℕ) (c : LiftedCell (p := p) n) :
…
```
Mentions: OAI.EilenbergGanea.CWCover.LiftedCell
def OAI.EilenbergGanea.CWCover.cwComplex line 195
Source documentation
Every ordinary CW structure lifts through any covering, with exactly the actual sheets times the base cells as cell indices.
```
@[instance_reducible] def cwComplex : CWComplex (univ : Set E) where
…
```
theorem OAI.EilenbergGanea.CWCover.cwComplex_cell_isEmpty line 235
Source documentation
Covering lifts preserve the literal absence of cells in each dimension.
```
theorem cwComplex_cell_isEmpty (n : ℕ) [IsEmpty (Topology.CWComplex.cell (univ : Set X) n)] :
    @IsEmpty (@Topology.CWComplex.cell E _ (univ : Set E) (cwComplex cov) n) := by
…
```
Mentions: OAI.EilenbergGanea.CWCover.cwComplex

theorem OAI.EilenbergGanea.CWCover.cwComplex_dimension_le line 241

Source documentation

No cardinality restriction is made in this dimension comparison.

theorem cwComplex_dimension_le (d : ℕ)
    (h : ∀ n, d < n → IsEmpty (Topology.CWComplex.cell (univ : Set X) n)) :
    ∀ n, d < n → @IsEmpty (@Topology.CWComplex.cell E _ (univ : Set E) (cwComplex cov) n) := by
…

Mentions: OAI.EilenbergGanea.CWCover.cwComplex

theorem OAI.EilenbergGanea.CoverTopology.existsUnique_lift_contractible line 261
Source documentation
A contractible domain admits based covering lifts without a separate local path-connectivity hypothesis: lift a contraction and reverse its base path.
```
theorem existsUnique_lift_contractible [ContractibleSpace A]
    (f : C(A,X)) (a₀ : A) (e₀ : E) (he : p e₀ = f a₀) :
    ∃! g : C(A,E), g a₀ = e₀ ∧ p ∘ g = f := by
…
```
def OAI.EilenbergGanea.CoverTopology.deckGroup line 322
Source documentation
The actual group of self-homeomorphisms over a covering projection.
```
def deckGroup : Subgroup (E ≃ₜ E) where
…
```
instance OAI.EilenbergGanea.CoverTopology.deckMulAction line 330
theorem OAI.EilenbergGanea.CoverTopology.deck_smul line 336
theorem OAI.EilenbergGanea.CoverTopology.deck_project line 338
instance OAI.EilenbergGanea.CoverTopology.deckContinuous line 340
theorem OAI.EilenbergGanea.CoverTopology.deck_ext line 346
theorem OAI.EilenbergGanea.CoverTopology.existsUnique_deck line 355
Source documentation
Every two points in a fiber of a contractible covering are related by a unique genuine deck homeomorphism. No local-connectivity hypothesis is added.
```
theorem existsUnique_deck [ContractibleSpace E] (x y : E) (hxy : p x = p y) :
    ∃! d : deckGroup p, d • x = y := by
…
```
Mentions: OAI.EilenbergGanea.CoverTopology.deckGroup
theorem OAI.EilenbergGanea.CoverTopology.isQuotientCoveringMap_deck line 387
Source documentation
A surjective contractible covering is literally a quotient covering by its deck group, with a free properly discontinuous action.
```
theorem isQuotientCoveringMap_deck [ContractibleSpace E] (hs : Function.Surjective p) :
    IsQuotientCoveringMap p (deckGroup p) where
…
```
Mentions: OAI.EilenbergGanea.CoverTopology.deckGroup
instance OAI.EilenbergGanea.CWCover.liftedCellAction line 415
Source documentation
Deck transformations act on the actual lifted cells through their centers.
```
instance liftedCellAction (n : ℕ) : MulAction (deckGroup p) (LiftedCell (p := p) n) where
…
```
Mentions: OAI.EilenbergGanea.CWCover.LiftedCell
theorem OAI.EilenbergGanea.CWCover.liftedCell_smul_base line 420
theorem OAI.EilenbergGanea.CWCover.liftedCell_smul_center line 423
theorem OAI.EilenbergGanea.CWCover.cellLift_smul line 427
Source documentation
Compatibility includes the full closed disk, not only cell interiors.
```
theorem cellLift_smul {n : ℕ} (d : deckGroup p) (c : LiftedCell (p := p) n) (z : Disk n) :
…
```
Mentions: OAI.EilenbergGanea.CWCover.LiftedCell, OAI.EilenbergGanea.CWCover.Disk
def OAI.EilenbergGanea.CWCover.chosenCell line 442
Source documentation
An arbitrary choice of one disk lift per base cell; no finiteness is needed.
```
def chosenCell {n : ℕ} (i : Cell (X := X) n) : LiftedCell (p := p) n :=
…
```
Mentions: OAI.EilenbergGanea.CWCover.Cell, OAI.EilenbergGanea.CWCover.LiftedCell
def OAI.EilenbergGanea.CWCover.cellOrbitEquiv line 448
Source documentation
Every lifted ordinary cell is uniquely a deck translate of the chosen lift of its base cell. This is the actual free-module coefficient indexing.
```
def cellOrbitEquiv (n : ℕ) : LiftedCell (p := p) n ≃ Cell (X := X) n × deckGroup p where
…
```
Mentions: OAI.EilenbergGanea.CWCover.LiftedCell, OAI.EilenbergGanea.CWCover.Cell
theorem OAI.EilenbergGanea.CWCover.cellOrbitEquiv_symm line 468

theorem OAI.EilenbergGanea.PathTransport.path_cover_induction line 481

Source documentation

A finite-mesh local-to-global principle for actual paths, preserving their homotopy classes rather than only abelianized chains.

theorem path_cover_induction (U : Set (Set X)) (hU : ∀ V ∈ U, IsOpen V)
    (hc : ⋃₀ U = univ) (P : ∀ {x y : X}, Path x y → Prop)
    (hhom : ∀ {x y} {p s : Path x y}, Path.Homotopic p s → P s → P p)
    (htrans : ∀ {x y z} (p : Path x y) (s : Path y z), P p → P s → P (p.trans s))
    (hsmall : ∀ {x y} (p : Path x y), p.toContinuousMap ∈ CubicalMesh.small U → P p)
    {x y} (p : Path x y) : P p := by
…

Mentions: OAI.EilenbergGanea.CubicalMesh.small

def OAI.EilenbergGanea.PathTransport.subpath line 511
structure OAI.EilenbergGanea.PathTransport.Compression line 518
def OAI.EilenbergGanea.PathTransport.Compression.Represents line 528
theorem OAI.EilenbergGanea.PathTransport.Compression.represents_homotopic line 532
theorem OAI.EilenbergGanea.PathTransport.Compression.represents_trans line 538
theorem OAI.EilenbergGanea.PathTransport.Compression.represents_left line 548
theorem OAI.EilenbergGanea.PathTransport.Compression.represents_right line 561
theorem OAI.EilenbergGanea.PathTransport.Compression.represents line 589
Source documentation
Removing the centers of attached cells of dimension at least two does not lose any path class, provided the actual punctured-cell components are joined.
```
theorem represents (hU : IsOpen U) (hV : IsOpen V) (hc : U ∪ V = univ)
    (hthin : ForestCover.ThinPaths V) {x y : X} (p : Path x y) : c.Represents p :=
…
```
Mentions: OAI.EilenbergGanea.ForestCover.ThinPaths
theorem OAI.EilenbergGanea.PathTransport.Compression.pathConnected line 608
theorem OAI.EilenbergGanea.PathTransport.Compression.fundamental_surjective line 619
Source documentation
Actual surjectivity on based fundamental groups, not only on H1.
```
theorem fundamental_surjective (r : U) :
    Function.Surjective (FundamentalGroup.map (⟨Subtype.val,continuous_subtype_val⟩ : C(U,X)) r) := by
…
```
def OAI.EilenbergGanea.CWCollar.Attachment.annulusPoint line 654
theorem OAI.EilenbergGanea.CWCollar.Attachment.annulus_inner line 656
def OAI.EilenbergGanea.CWCollar.Attachment.compressionChoice line 659
theorem OAI.EilenbergGanea.CWCollar.Attachment.overlap_join line 681
Source documentation
The punctured-disk overlap is connected inside each open disk, so any inner path joining overlap points can be replaced there.
```
theorem overlap_join (x y : (a.outer ∩ a.inner : Set X))
    (hp : Nonempty (Path (⟨x.val,x.property.2⟩ : a.inner) ⟨y.val,y.property.2⟩)) : Nonempty (Path x y) := by
…
```
def OAI.EilenbergGanea.CWCollar.Attachment.compression line 712
theorem OAI.EilenbergGanea.CWCollar.lifted_characteristic line 729
abbrev OAI.EilenbergGanea.CWCollar.baseAttachment line 735
def OAI.EilenbergGanea.CWCollar.liftedAttachment line 736
theorem OAI.EilenbergGanea.CWCollar.lifted_radius line 743
Source documentation
The radial coordinate is literally preserved by projection, including all lower-skeleton points, not merely open-cell interiors.
```
theorem lifted_radius (e : E) :
    (liftedAttachment cov hd).radius e = (baseAttachment hd).radius (p e) := by
…
```
Mentions: OAI.EilenbergGanea.CWCollar.liftedAttachment, OAI.EilenbergGanea.CWCollar.baseAttachment
theorem OAI.EilenbergGanea.CWCollar.lifted_outer line 765
theorem OAI.EilenbergGanea.CWCollar.lifted_inner line 769
def OAI.EilenbergGanea.CWCollar.liftedOuterHomeomorph line 774
def OAI.EilenbergGanea.CWCollar.outerProjection line 777
theorem OAI.EilenbergGanea.CWCollar.outerProjection_cover line 783
theorem OAI.EilenbergGanea.CWCollar.lifted_annulus line 788
Source documentation
The same parametrized annulus projects to the base annulus.
```
theorem lifted_annulus (c : LiftedCell (p:=p) m) (z : Annulus m) :
…
```
Mentions: OAI.EilenbergGanea.CWCollar.Annulus
def OAI.EilenbergGanea.CoverKernel.projection line 804
def OAI.EilenbergGanea.CoverKernel.inclusion line 805
def OAI.EilenbergGanea.CoverKernel.totalInclusion line 806
theorem OAI.EilenbergGanea.CoverKernel.lift_loop_closed line 808
def OAI.EilenbergGanea.CoverKernel.toBase line 817
def OAI.EilenbergGanea.CoverKernel.toTotal line 820
theorem OAI.EilenbergGanea.CoverKernel.toBase_injective line 823
theorem OAI.EilenbergGanea.CoverKernel.toBase_range line 829
Source documentation
Closed lifting, proved using homotopy lifting, identifies the full kernel.
```
theorem toBase_range [SimplyConnectedSpace E] : (toBase cov U e).range = (toTotal cov U e).ker := by
…
```
Mentions: OAI.EilenbergGanea.CoverKernel.toBase, OAI.EilenbergGanea.CoverKernel.toTotal
def OAI.EilenbergGanea.CoverKernel.fundamentalKernelEquiv line 873
Source documentation
This is an equivalence with the actual kernel, not an assumed presentation.
```
def fundamentalKernelEquiv [SimplyConnectedSpace E] :
    (FundamentalGroup (p ⁻¹' U) e)ᵐᵒᵖ ≃* (toTotal cov U e).ker :=
…
```
Mentions: OAI.EilenbergGanea.CoverKernel.toTotal
def OAI.EilenbergGanea.PathTransport.anchored line 884
def OAI.EilenbergGanea.PathTransport.difference line 886
theorem OAI.EilenbergGanea.PathTransport.anchored_map line 889
theorem OAI.EilenbergGanea.PathTransport.anchored_conjugate line 897
Source documentation
Changing the path to a circle changes its based relation by conjugacy.
```
theorem anchored_conjugate {r x : X} (q s : Path r x) (p : Path x x) :
    anchored q p = difference q s * anchored s p * (difference q s)⁻¹ := by
…
```
Mentions: OAI.EilenbergGanea.PathTransport.anchored, OAI.EilenbergGanea.PathTransport.difference
theorem OAI.EilenbergGanea.PathTransport.anchored_congr line 912
Source documentation
Pointwise equality of anchored curves handles changes of endpoint proofs.
```
theorem anchored_congr {r x y : X} (q : Path r x) (s : Path r y)
    (p : Path x x) (t : Path y y) (hqs : ∀ z, q z = s z) (hpt : ∀ z, p z = t z) :
    anchored q p = anchored s t := by
…
```
Mentions: OAI.EilenbergGanea.PathTransport.anchored
def OAI.EilenbergGanea.CoverMonodromy.traversalEquiv line 930
theorem OAI.EilenbergGanea.CoverMonodromy.traversalEquiv_loop line 934
Source documentation
Monodromy reads exactly the endpoint of a lifted traversal-order loop.
```
theorem traversalEquiv_loop (d : G) (γ : Path e (d • e)) :
    traversalEquiv hp e (MulOpposite.op (Path.Homotopic.Quotient.mk
      ((γ.map hp.continuous).cast rfl (hp.map_smul d).symm))) = d := by
…
```
Mentions: OAI.EilenbergGanea.CoverMonodromy.traversalEquiv

theorem OAI.EilenbergGanea.CoverMonodromy.traversalEquiv_difference line 950

Source documentation

A pair of lifted anchors differing by a deck translate records that exact translate, independently of all anchor choices.

theorem traversalEquiv_difference (d : G) {z : E}
    (s : Path e (d • z)) (t : Path e z) :
    traversalEquiv hp e (MulOpposite.op (Path.Homotopic.Quotient.mk
      (((s.map hp.continuous).cast rfl (hp.map_smul d).symm).trans
        (t.map hp.continuous).symm))) = d := by
…

Mentions: OAI.EilenbergGanea.CoverMonodromy.traversalEquiv