Low Dim Topology

Results named in Tau Ceti's TauCeti.LowDimTopology modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

TheoremLi's theorem refutes Waldhausen's conjecture#

some closed orientable 3-manifold has Heegaard genus different from the rank of its fundamental group.

TauCeti.LiRankGenusTheorem.not_rankGenusConjecture.{u} (h : TauCeti.LiRankGenusTheorem) :
  ¬TauCeti.RankGenusConjecture

Lean

Formalized in Tau Ceti as TauCeti.LiRankGenusTheorem.not_rankGenusConjecture, assuming TauCeti.LiRankGenusTheorem, a proposition Tau Ceti defines.

Sources

• Tau Ceti documentation: TauCeti.LiRankGenusTheorem.not_rankGenusConjecture
• Source of TauCeti.LiRankGenusTheorem.not_rankGenusConjecture in TauCeti/LowDimTopology/Heegaard/RankGenus.lean

LeanTauCeti.LiRankGenusTheorem.not_rankGenusConjecture

Uses 1

Proof usesThe Koszul formula

TheoremUnder Gabai's theorem, a generator of H₂(S¹ × S²; ℤ) has minimal genus 0#

S¹ × S² is the 0-surgery on the unknot, which has Seifert genus 0.

TauCeti.GabaiZeroSurgeryGenusTheorem.minimalGenus_circle_prod_sphere
  (hG : TauCeti.GabaiZeroSurgeryGenusTheorem)
  {c : ↑(TauCeti.secondHomology (Circle × ↑(Metric.sphere 0 1)))} (hc : ℤ ∙ c = ⊤) :
  TauCeti.minimalGenus c = 0

Lean

Formalized in Tau Ceti as TauCeti.GabaiZeroSurgeryGenusTheorem.minimalGenus_circle_prod_sphere, assuming TauCeti.GabaiZeroSurgeryGenusTheorem, a proposition Tau Ceti defines.

Sources

• Tau Ceti documentation: TauCeti.GabaiZeroSurgeryGenusTheorem.minimalGenus_circle_prod_sphere
• Source of TauCeti.GabaiZeroSurgeryGenusTheorem.minimalGenus_circle_prod_sphere in TauCeti/LowDimTopology/DehnSurgery/ZeroSurgeryGenus.lean

LeanTauCeti.GabaiZeroSurgeryGenusTheorem.minimalGenus_circle_prod_sphere

Uses 5

Statement usesThe Hurewicz theorem · TauCeti.IsSolidTorusNeighborhood.framingNumber · TauCeti.knotExterior

Proof usesThe Mayer–Vietoris isomorphism of a sphere · The relative small-chain theorem

TheoremYasui's theorem spelled out#

there are knots K K' : S¹ → S³ with 0-surgeries Y, Y', oriented compatibly with an orientation of S³, and an orientation-preserving homeomorphism Y ≃ₜ Y', such that K is smoothly concordant neither to K' nor to its reverse.

TauCeti.yasuiTheorem_iff :
  TauCeti.YasuiTheorem ↔
    ∃ o K K' Φ Φ',
      ∃ (h : TauCeti.IsSolidTorusNeighborhood (⇑K) Φ) (h' :
        TauCeti.IsSolidTorusNeighborhood (⇑K') Φ'),
        ∃ Y Y' x,
          ∃ (x_1 : T2Space Y),
            ∃ x_2 x_3,
              ∃ (x_4 : T2Space Y'),
                ∃ x_5 F F' oY oY' e,
                  F.IsOrientationCompatible o oY ∧
                    F'.IsOrientationCompatible o oY' ∧
                      oY'.comap ⋯ = oY ∧
                        ¬TauCeti.SmoothEmbedding.Concordant K K' ∧
                          ¬TauCeti.SmoothEmbedding.Concordant K K'.reverse

Lean

Formalized in Tau Ceti as TauCeti.yasuiTheorem_iff.

Sources

• Tau Ceti documentation: TauCeti.yasuiTheorem_iff
• Source of TauCeti.yasuiTheorem_iff in TauCeti/LowDimTopology/DehnSurgery/AkbulutKirby.lean

LeanTauCeti.yasuiTheorem_iff

Uses 5

Statement usesThe Hurewicz theorem · TauCeti.IsSolidTorusNeighborhood.framingNumber · TauCeti.knotExterior

Proof usesThe Mayer–Vietoris isomorphism of a sphere · The relative small-chain theorem

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.