CubicalCover.lean`

75 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.EilenbergGanea.DescendingCube.Data.cellComm line 22
theorem OAI.EilenbergGanea.DescendingCube.Data.ones_eq_filter line 27
theorem OAI.EilenbergGanea.DescendingCube.Data.normalize_fullCoord line 38
def OAI.EilenbergGanea.DescendingCube.Data.interpolation line 45
theorem OAI.EilenbergGanea.DescendingCube.Data.active_characteristic_subset line 48
theorem OAI.EilenbergGanea.DescendingCube.Data.interpolation_characteristic line 56
theorem OAI.EilenbergGanea.DescendingCube.Data.interpolation_continuous line 70
theorem OAI.EilenbergGanea.DescendingCube.Data.interpolation_vertex_pos line 80
theorem OAI.EilenbergGanea.DescendingCube.Data.descending_operator_delta_zero line 88
theorem OAI.EilenbergGanea.DescendingCube.Data.interpolation_vertex_zero line 110
theorem OAI.EilenbergGanea.DescendingCube.Data.interpolation_top_eq line 115
theorem OAI.EilenbergGanea.DescendingCube.Data.interpolation_exponent line 138
theorem OAI.EilenbergGanea.DescendingCube.Data.interpolation_injective line 153
theorem OAI.EilenbergGanea.DescendingCube.Data.point_t2 line 173

def OAI.WeakRealization.homeomorph line 185

Source documentation

A homeomorphism is induced by point-separating coordinates and actual continuous lifts on each characteristic disk, in both directions.

def homeomorph {ι κ X Y Z : Type*} {E : ι → Type*} {F : κ → Type*}
    [TopologicalSpace X] [TopologicalSpace Y]
    [∀ i, TopologicalSpace (E i)] [∀ j, TopologicalSpace (F j)]
    (e : ((i : ι) × E i) → X) (f : ((j : κ) × F j) → Y)
    (he : IsQuotientMap e) (hf : IsQuotientMap f)
    (J : X → Z) (K : Y → Z) (hJ : Function.Injective J) (hK : Function.Injective K)
    (hxy : ∀ i, ∃ φ : C(E i,Y), ∀ t, K (φ t) = J (e ⟨i,t⟩))
    (hyx : ∀ j, ∃ φ : C(F j,X), ∀ t, J (φ t) = K (f ⟨j,t⟩)) : X ≃ₜ Y := by
…

def OAI.EilenbergGanea.CubeInterpolation.listed line 243
Source documentation
Interpolation in a listed cube, independent of any topological model.
```
def listed (f : V → G) (w : List V) (x : V → ℝ) : Module.End ℝ (G → ℝ) :=
…
```
theorem OAI.EilenbergGanea.CubeInterpolation.listed_nil line 246
theorem OAI.EilenbergGanea.CubeInterpolation.listed_cons line 247
theorem OAI.EilenbergGanea.CubeInterpolation.operator_listed line 250

theorem OAI.EilenbergGanea.CubeInterpolation.listed_reorientation line 256

Source documentation

Literal multilinear invariance under reversing selected cube directions.

theorem listed_reorientation (f : V → G) (w : List (Signed V))
    (hw : w.Pairwise (fun a b => Commute (f a.1) (f b.1)))
    (x : Signed V → ℝ) (z : V → ℝ)
    (hx : ∀ a ∈ w, x a = if a.2 then 1-z a.1 else z a.1) (φ : G → ℝ) (g : G) :
    listed (step f) w x φ g = listed f (w.map Prod.fst) z φ (origin f g w) := by
…

Mentions: OAI.EilenbergGanea.CubeInterpolation.listed

abbrev OAI.EilenbergGanea.ArtinCubicalTopology.f line 286
abbrev OAI.EilenbergGanea.ArtinCubicalTopology.comm line 287
abbrev OAI.EilenbergGanea.ArtinCubicalTopology.D line 288
abbrev OAI.EilenbergGanea.ArtinCubicalTopology.Positive line 289
abbrev OAI.EilenbergGanea.ArtinCubicalTopology.Descending line 290
theorem OAI.EilenbergGanea.ArtinCubicalTopology.step_eq line 293
def OAI.EilenbergGanea.ArtinCubicalTopology.exponent line 296
theorem OAI.EilenbergGanea.ArtinCubicalTopology.exponent_generator line 301
theorem OAI.EilenbergGanea.ArtinCubicalTopology.height_generator line 306
def OAI.EilenbergGanea.ArtinCubicalTopology.signedExponent line 309
theorem OAI.EilenbergGanea.ArtinCubicalTopology.signedExponent_step line 314
theorem OAI.EilenbergGanea.ArtinCubicalTopology.positive_interp_inj line 327
theorem OAI.EilenbergGanea.ArtinCubicalTopology.descending_interp_inj line 332
def OAI.EilenbergGanea.ArtinCubicalTopology.flip line 338
theorem OAI.EilenbergGanea.ArtinCubicalTopology.flip_flip line 341
theorem OAI.EilenbergGanea.ArtinCubicalTopology.flip_continuous line 344
def OAI.EilenbergGanea.ArtinCubicalTopology.vertexEquiv line 349
theorem OAI.EilenbergGanea.ArtinCubicalTopology.vertexEquiv_val line 363
def OAI.EilenbergGanea.ArtinCubicalTopology.toPositiveCoords line 366
theorem OAI.EilenbergGanea.ArtinCubicalTopology.toPositiveCoords_apply line 371
theorem OAI.EilenbergGanea.ArtinCubicalTopology.toPositiveCoords_continuous line 377
def OAI.EilenbergGanea.ArtinCubicalTopology.toDescendingCoords line 381
theorem OAI.EilenbergGanea.ArtinCubicalTopology.toDescendingCoords_continuous line 386
theorem OAI.EilenbergGanea.ArtinCubicalTopology.toPositive_toDescending line 391
def OAI.EilenbergGanea.ArtinCubicalTopology.positiveCell line 398
def OAI.EilenbergGanea.ArtinCubicalTopology.descendingCell line 404
theorem OAI.EilenbergGanea.ArtinCubicalTopology.interpolation_reorientation line 410
theorem OAI.EilenbergGanea.ArtinCubicalTopology.descendingCell_rep line 440
theorem OAI.EilenbergGanea.ArtinCubicalTopology.positiveCell_rep line 461
theorem OAI.EilenbergGanea.ArtinCubicalTopology.descending_local_lift line 480
theorem OAI.EilenbergGanea.ArtinCubicalTopology.positive_local_lift line 493
def OAI.EilenbergGanea.ArtinCubicalTopology.reorient line 511
Source documentation
Reorientation preserves the actual weak topologies, not only cellular chains.
```
def reorient : Descending L ≃ₜ Positive L :=
…
```
Mentions: OAI.EilenbergGanea.ArtinCubicalTopology.Descending, OAI.EilenbergGanea.ArtinCubicalTopology.Positive
theorem OAI.EilenbergGanea.ArtinCubicalTopology.positive_contractible line 522
Source documentation
The ordinary positive-cube CW realization is genuinely contractible.
```
theorem positive_contractible : ContractibleSpace (Positive L) := by
…
```
Mentions: OAI.EilenbergGanea.ArtinCubicalTopology.Positive

theorem OAI.CompactChart.continuousOn_symm line 534

Source documentation

A characteristic map which has singleton fibers over its open cell has a continuous inverse there. Compactness is used only on the closed disk; no regularity of the attaching sphere is required.

theorem continuousOn_symm {A X : Type*} [TopologicalSpace A] [TopologicalSpace X]
    [T2Space X] (e : PartialEquiv A X) (K : Set A) (hK : IsCompact K)
    (hsub : e.source ⊆ K) (hc : ContinuousOn e K)
    (hboundary : ∀ a ∈ K, e a ∈ e.target → a ∈ e.source) :
    ContinuousOn e.symm e.target := by
…

theorem OAI.EilenbergGanea.CubeRealization.chartInverse_continuousOn_of_t2 line 572
def OAI.EilenbergGanea.CubeRealization.cwComplexOfT2 line 589
Source documentation
The ordinary CW structure follows from the genuine normalized-cube gluing; only Hausdorffness and compact characteristic disks are used.
```
@[instance_reducible] def cwComplexOfT2 [T2Space (Point (G := G) L f comm)] : CWComplex (univ : Set (Point (G := G) L f comm)) where
…
```
Mentions: OAI.EilenbergGanea.CubeRealization.Point
theorem OAI.EilenbergGanea.CubeRealization.mappedComm line 639
def OAI.EilenbergGanea.CubeRealization.mapPoint line 643
Source documentation
Applying a group homomorphism only to the initial vertices of cubes.
```
def mapPoint (p : Point (G := G) L f comm) : Point (G := Q) L (q ∘ f) (mappedComm f comm q) where
…
```
Mentions: OAI.EilenbergGanea.CubeRealization.Point, OAI.EilenbergGanea.CubeRealization.mappedComm
def OAI.EilenbergGanea.CubeRealization.mapCell line 650
theorem OAI.EilenbergGanea.CubeRealization.mapPoint_base line 656
theorem OAI.EilenbergGanea.CubeRealization.mapPoint_coord line 660
theorem OAI.EilenbergGanea.CubeRealization.mapPoint_characteristic line 664
theorem OAI.EilenbergGanea.CubeRealization.mapPoint_continuous line 675
theorem OAI.EilenbergGanea.CubeRealization.mapCell_surjective line 684
theorem OAI.EilenbergGanea.CubeRealization.mapPoint_surjective line 690
theorem OAI.EilenbergGanea.CubeRealization.mapPoint_quotient line 697
Source documentation
The base-label quotient is a genuine topological quotient for the weak cubical topologies, proved by lifting each actual characteristic disk.
```
theorem mapPoint_quotient (hq : Function.Surjective q) : IsQuotientMap (mapPoint f comm q) := by
…
```
Mentions: OAI.EilenbergGanea.CubeRealization.mapPoint
theorem OAI.EilenbergGanea.CubeRealization.mapPoint_eq_iff_orbit line 716
Source documentation
The literal group-kernel orbits are exactly the fibers of the cube map.
```
theorem mapPoint_eq_iff_orbit (p r : Point (G := G) L f comm) :
…
```
Mentions: OAI.EilenbergGanea.CubeRealization.Point
def OAI.EilenbergGanea.CubeRealization.kernelQuotientHomeomorph line 736
Source documentation
The quotient homeomorphism respects the actual weak topologies.
```
def kernelQuotientHomeomorph (hq : Function.Surjective q) :
    Quotient (MulAction.orbitRel q.ker (Point (G := G) L f comm)) ≃ₜ
…
```
Mentions: OAI.EilenbergGanea.CubeRealization.Point
theorem OAI.EilenbergGanea.CubeRealization.quotientPoint_t2 line 748
theorem OAI.EilenbergGanea.CubeRealization.mapPoint_covering line 755
theorem OAI.EilenbergGanea.ArtinCubicalTopology.height_surjective line 771
def OAI.EilenbergGanea.ArtinCubicalTopology.HeightQuotient line 780
instance OAI.EilenbergGanea.ArtinCubicalTopology.(instance at line 782) line 782
theorem OAI.EilenbergGanea.ArtinCubicalTopology.height_hasClassifyingSpace line 789
Source documentation
An ordinary cubical classifying space for the height kernel, with one cube for every integral level and clique. Contractibility above is the explicit word-length contraction, and the fundamental-group identification reuses Mathlib's checked covering-monodromy equivalence.
```
theorem height_hasClassifyingSpace (d : ℕ)
    (hd : ∀ s : Finset V, (s : Set V).Pairwise L.Adj → s.card ≤ d) :
    HasClassifyingSpace.{u} (height L).ker d := by
…
```
theorem OAI.EilenbergGanea.source_hasClassifyingSpace_three line 816
Source documentation
The fixed source group has an ordinary three-dimensional classifying CW space, with an actually contractible surjective covering.
```
theorem source_hasClassifyingSpace_three : HasClassifyingSpace.{0} SourceGroup 3 :=
…
```
Mentions: OAI.EilenbergGanea.SourceGroup