Geometric topology and the solved Kirby-list problems
The declarations the status of Tau Ceti's roadmap names, and the other results named in the modules where only this status names declarations, or in folders below the areas where only it names 2 or more, as Tau Ceti has them at commit ace60277.
TheoremPreAbstractSimplicialComplex.IsCombinatorialManifold.exists_chartedSpace_hasGroupoid_PLGroupoid#
The weak realization of a positive-dimensional combinatorial manifold is a PL manifold,
possibly with boundary: it has an atlas modelled on the half-space in (Fin n → ℝ) × ℝ whose
chart transitions lie in the PL groupoid. No finiteness or countability of the complex is
assumed.
PreAbstractSimplicialComplex.IsCombinatorialManifold.exists_chartedSpace_hasGroupoid_PLGroupoid.{u_1}
{ι : Type u_1} [DecidableEq ι] {K : AbstractSimplicialComplex ι} {n : ℕ}
(h : K.IsCombinatorialManifold (n + 1)) :
∃ C,
have this := C;
HasGroupoid K.Realization (TauCeti.PLGroupoid (TauCeti.modelWithCornersHalfSpace (Fin n → ℝ)))
Lean
Formalized in Tau Ceti as PreAbstractSimplicialComplex.IsCombinatorialManifold.exists_chartedSpace_hasGroupoid_PLGroupoid.
Sources
- Tau Ceti documentation:
PreAbstractSimplicialComplex.IsCombinatorialManifold.exists_chartedSpace_hasGroupoid_PLGroupoid - Source of
PreAbstractSimplicialComplex.IsCombinatorialManifold.exists_chartedSpace_hasGroupoid_PLGroupoidin TauCeti/AlgebraicTopology/SimplicialComplex/CombinatorialManifold/PL.lean - Tau Ceti roadmap status: Geometric topology and the solved Kirby-list problems
TheoremThe HOMFLY polynomial is a link invariant on braid closures#
Markov-equivalent braids have the same HOMFLY polynomial.
TauCeti.MarkovEquiv.homfly_eq.{u_1} (K : Type u_1) [Field K] {β γ : TauCeti.MarkovBraid}
(h : TauCeti.MarkovEquiv β γ) : TauCeti.MarkovBraid.homfly K β = TauCeti.MarkovBraid.homfly K γ
TheoremDiffeomorph.isTopologicalGroup#
Self-diffeomorphisms of a compact Hausdorff manifold with a locally compact model space form a topological group for the weak Whitney topology.
Diffeomorph.isTopologicalGroup.{u_1, u_2, u_3, u_4} {𝕜 : Type u_1} [NontriviallyNormedField 𝕜]
{E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M]
{n : WithTop ℕ∞} [CompactSpace M] [LocallyCompactSpace E] [IsManifold I n M] [T2Space M] :
IsTopologicalGroup (Diffeomorph I I M M n)
DefinitionTauCeti.Nil.semidirectProductIsomMulEquiv#
The full Riemannian isometry group of Nil is Nil ⋊ O(2), with its canonical
translation and orthogonal actions. This is an isomorphism of groups.
TauCeti.Nil.semidirectProductIsomMulEquiv :
TauCeti.Nil ⋊[TauCeti.Nil.orthogonalMulAut] ↥(Matrix.orthogonalGroup (Fin 2) ℝ) ≃*
TauCeti.Isom (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) TauCeti.Nil
DefinitionTauCeti.UpperHalfSpace.hyperbolicMetric#
The standard complete metric of constant curvature -1 on upper half-space.
TauCeti.UpperHalfSpace.hyperbolicMetric.{u_1} {E : Type u_1} [NormedAddCommGroup E]
[InnerProductSpace ℝ E] [FiniteDimensional ℝ E] : TauCeti.HyperbolicMetric
Uses 1
DefinitionTauCeti.knotExterior#
The closed exterior of a solid-torus neighbourhood: the complement of its open solid-torus image.
TauCeti.knotExterior.{u_1} {X : Type u_1} {Φ : TauCeti.SolidTorus → X} : Set X
DefinitionTauCeti.IsSolidTorusNeighborhood.framingNumber#
The framing number of the solid torus neighbourhood Φ: the longitude of Φ is
homologous in the knot complement to framingNumber times the meridian. Equivalently, the
longitude of Φ is λ₀ + n · μ for the preferred longitude λ₀
(TauCeti.IsSolidTorusNeighborhood.preferredFramedBoundaryTorus_basis_one). For a knot in S³
it is the linking number of the longitude of Φ with the knot.
TauCeti.IsSolidTorusNeighborhood.framingNumber {X : Type} [TopologicalSpace X] {f : Circle → X}
{Φ : TauCeti.SolidTorus → X} [T2Space X]
(h₁ : CategoryTheory.Limits.IsZero ((TauCeti.reducedSingularHomologyFunctor (↧ℤ) 1).obj ↧X))
(h₂ : CategoryTheory.Limits.IsZero ((TauCeti.reducedSingularHomologyFunctor (↧ℤ) 2).obj ↧X))
(h : TauCeti.IsSolidTorusNeighborhood f Φ) : ℤ
Uses 1 · Used by 2
DefinitionTauCeti.Foliation.eulerClass#
The Euler class Hᵏ(TF, TF₀) ⟶ Hᵏ(M) of the tangent field of a foliation of rank k:
TauCeti.eulerClass, restriction to the total space followed by pullback along the zero
section, read in degree k.
TauCeti.Foliation.eulerClass.{w, v, u, u_1, u_2} {E : Type w} [NormedAddCommGroup E]
[NormedSpace ℝ E] {H : Type u_1} [TopologicalSpace H] {I : ModelWithCorners ℝ E H}
{n : WithTop ℕ∞} {M : Type w} [TopologicalSpace M] [ChartedSpace H M] {k : ℕ}
[IsManifold I (n + 1) M] (F : TauCeti.Foliation I n M k) {C : Type u}
[CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C]
[CategoryTheory.Abelian C] (R : C) (K : Type u_2) [Ring K] [CategoryTheory.Linear K C] (N : C) :
F.thomPair.singularCohomology R K N (Module.finrank ℝ (Fin k → ℝ)) ⟶
TopCat.singularCohomology R K N (↧M) k
DefinitionThurston's Euler class inequality#
on a closed orientable hyperbolic 3-manifold M,
that is a compact connected orientable smooth 3-manifold without boundary admitting a complete
Riemannian metric of constant curvature -1, every Euler class of a smooth taut codimension-one
foliation satisfies the Euler class inequality.
TauCeti.ThurstonEulerClassInequality : Prop
Uses 4
TheoremYazdi's theorem refutes the Euler class one conjecture#
TauCeti.YazdiEulerClassOneTheorem.not_eulerClassOneConjecture
(h : TauCeti.YazdiEulerClassOneTheorem) : ¬TauCeti.EulerClassOneConjecture
Lean
Formalized in Tau Ceti as TauCeti.YazdiEulerClassOneTheorem.not_eulerClassOneConjecture, assuming TauCeti.YazdiEulerClassOneTheorem, a proposition Tau Ceti defines.
Sources
Uses 4
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.