Morse and Floer homology with DG local coefficients

The declarations the status of Tau Ceti's roadmap names as Tau Ceti has them at commit ace60277.

DefinitionCubical singular homology is naturally isomorphic to singular homology, as functors on topological spaces# 

TauCeti.singularCubicalHomologyNatIso.{u} (k : Type u) [Ring k] (n : ℕ) :
  (TauCeti.singularChains k).comp
      (HomologicalComplex.homologyFunctor (ModuleCat k) (ComplexShape.down ℕ) n) ≅
    (TauCeti.normalizedCubicalChainComplex k).comp
      (HomologicalComplex.homologyFunctor (ModuleCat k) (ComplexShape.down ℕ) n)
Lean

Formalized in Tau Ceti as TauCeti.singularCubicalHomologyNatIso.

Sources
LeanTauCeti.singularCubicalHomologyNatIso

DefinitionCubical and simplicial chains with local coefficients are chain homotopy equivalent# 

TauCeti.LocalCoefficientSystem.twistedCubicalSingularHomotopyEquiv.{u, v} {R : Type u} [Ring R]
  {X : TopCat} (L : TauCeti.LocalCoefficientSystem R X) :
  HomotopyEquiv L.normalizedTwistedCubicalChainComplex L.twistedChainComplex
Lean

Formalized in Tau Ceti as TauCeti.LocalCoefficientSystem.twistedCubicalSingularHomotopyEquiv.

Sources
LeanTauCeti.LocalCoefficientSystem.twistedCubicalSingularHomotopyEquiv
Used by 1
Used byA weak homotopy equivalence induces isomorphisms on singular homology with local coefficients, the local-coefficient form of Hatcher, Proposition 4.21

TheoremCW approximation (Hatcher, Proposition 4.13)#

For a path-connected space X, the map TauCeti.cwApproximationMap X x from the CW complex TauCeti.cwApproximation X x to X is a weak homotopy equivalence.

TauCeti.isWeakHomotopyEquivalence_cwApproximationMap.{u} (X : TopCat) (x : ↑X)
  [PathConnectedSpace ↑X] :
  (TopCat.Hom.hom (TauCeti.cwApproximationMap X x)).IsWeakHomotopyEquivalence
Lean

Formalized in Tau Ceti as TauCeti.isWeakHomotopyEquivalence_cwApproximationMap.

Sources
LeanTauCeti.isWeakHomotopyEquivalence_cwApproximationMap

TheoremA weak homotopy equivalence induces isomorphisms on singular homology with local coefficients, the local-coefficient form of Hatcher, Proposition 4.21#

for every local coefficient system L on Y, the map H_n(X; f⁎L) ⟶ H_n(Y; L) is an isomorphism.

ContinuousMap.IsWeakHomotopyEquivalence.isIso_twistedHomologyMap.{u, v} {X Y : Type v}
  [TopologicalSpace X] [TopologicalSpace Y] {f : C(X, Y)} {R : Type u} [Ring R]
  (hf : f.IsWeakHomotopyEquivalence) (L : TauCeti.LocalCoefficientSystem R ↧Y) (n : ℕ) :
  CategoryTheory.IsIso (TauCeti.LocalCoefficientSystem.twistedHomologyMap (TopCat.ofHom f) L n)
Lean

Formalized in Tau Ceti as ContinuousMap.IsWeakHomotopyEquivalence.isIso_twistedHomologyMap.

Sources
LeanContinuousMap.IsWeakHomotopyEquivalence.isIso_twistedHomologyMap
Uses 1
Proof usesCubical and simplicial chains with local coefficients are chain homotopy equivalent

TheoremBarraud--Damian--Humilière--Oancea, Lemma 3.41 (Moore singular homology)#

A path-connected space X is aspherical if and only if its double Moore loop space is path connected with vanishing positive-degree integral singular homology.

TauCeti.MooreLoopSpace.isAspherical_iff_double_singularHomology {X : Type} [TopologicalSpace X]
  (x : X) [PathConnectedSpace X] :
  TauCeti.IsAspherical X x ↔
    PathConnectedSpace (TauCeti.MooreLoopSpace (TauCeti.MooreLoopSpace X x) 1) ∧
      ∀ (m : ℕ),
        m ≠ 0 →
          CategoryTheory.Limits.IsZero
            (HomologicalComplex.homology
              ((TauCeti.singularChains ℤ).obj
                ↧(TauCeti.MooreLoopSpace (TauCeti.MooreLoopSpace X x) 1))
              m)
Lean

Formalized in Tau Ceti as TauCeti.MooreLoopSpace.isAspherical_iff_double_singularHomology.

Sources
LeanTauCeti.MooreLoopSpace.isAspherical_iff_double_singularHomology
Uses 2
Proof usesThe Hurewicz theorem · Inductive Hurewicz vanishing criterion (singular homology)

DefinitionHomologous twisting cocycles give homotopy equivalent twisted complexes#

for every differential graded right module (ℳ, dM), the twisted complexes of mP and mQ are homotopy equivalent.

TauCeti.Homologous.homotopyEquiv.{uR, uA, uM, uP} {R : Type uR} {A : Type uA} {M : Type uM}
  [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [_root_.Module R M] {P Q : Type uP}
  {ind : P → ℤ} {indQ : Q → ℤ} [Fintype P] [Fintype Q] [_root_.Module Aᵐᵒᵖ M]
  [IsScalarTower R Aᵐᵒᵖ M] [SMulCommClass R Aᵐᵒᵖ M] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜]
  {d : A →ₗ[R] A} {h : TauCeti.IsDGAlgebra 𝒜 d} {ℳ : ℤ → Submodule R M} [DirectSum.Decomposition ℳ]
  [SetLike.GradedSMul ((TauCeti.InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) ℳ]
  {dM : M →ₗ[R] M} {mP : TauCeti.TwistingCocycle 𝒜 d P ind}
  {mQ : TauCeti.TwistingCocycle 𝒜 d Q indQ} [DecidableEq P] [DecidableEq Q]
  (H : TauCeti.Homologous h mP mQ) (hM : TauCeti.IsDGRightModule h ℳ dM) :
  HomotopyEquiv (mP.twistedCochainComplex dM hM) (mQ.twistedCochainComplex dM hM)
Lean

Formalized in Tau Ceti as TauCeti.Homologous.homotopyEquiv.

Sources
LeanTauCeti.Homologous.homotopyEquiv

DefinitionThe second page of the index spectral sequence is the cohomology of the classical complex (BDHO, Definition 3.38 and Ch. 3 §4.2)#

the object at (a, b) of the page 3 of the index spectral sequence (the classical E₂ page, in Mathlib's numbering of pages) is the homology in degree b + 1 of the classical complex in coefficient degree a + 2 * b + 1. It is the homology of the first page at (a, b), identified with the homology of the classical complex by indexSecondPageShortComplexIso (see indexSpectralSequenceSecondPageXIso_eq).

TauCeti.TwistingCocycle.indexSpectralSequenceSecondPageXIso.{uR, uA, uM, uP} {R : Type uR}
  {A : Type uA} {M : Type uM} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M]
  [_root_.Module R M] {P : Type uP} {ind : P → ℤ} [Fintype P] [_root_.Module Aᵐᵒᵖ M]
  [IsScalarTower R Aᵐᵒᵖ M] {ℳ : ℤ → Submodule R M} [DirectSum.Decomposition ℳ] {dM : M →ₗ[R] M}
  {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {h : TauCeti.IsDGAlgebra 𝒜 d}
  [SetLike.GradedSMul ((TauCeti.InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) ℳ]
  (m : TauCeti.TwistingCocycle 𝒜 d P ind) (hM : TauCeti.IsDGRightModule h ℳ dM) [DecidableEq P]
  (a b : ℤ) :
  ((TauCeti.TwistingCocycle.indexSpectralSequence dM m hM).page 3
          TauCeti.TwistingCocycle.indexSpectralSequenceSecondPageXIso._proof_2).X
      (a, b) ≅
    HomologicalComplex.homology (m.indexClassicalComplex hM (a + 2 * b + 1)) (b + 1)
Lean

Formalized in Tau Ceti as TauCeti.TwistingCocycle.indexSpectralSequenceSecondPageXIso.

Sources
LeanTauCeti.TwistingCocycle.indexSpectralSequenceSecondPageXIso

TheoremThe unit codisc bundle is a Liouville domain#

For a compact smooth Riemannian manifold M without boundary, the unit codisc bundle D*M is a Liouville domain in T*M for the canonical symplectic form ω = -dλ, with primitive -λ: its Liouville field, the radial field p ∂_p, points strictly outwards along the unit cosphere bundle, the level ‖p‖ = 1 of the norm of covectors.

TauCeti.CotangentBundle.isLiouvilleDomain_codiscBundle.{u_1, u_2, u_3} {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2}
  [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [I.Boundaryless] {M : Type u_3}
  [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M]
  [Bundle.RiemannianBundle fun x => TangentSpace I x]
  [IsContMDiffRiemannianBundle I (↑⊤) E fun x => TangentSpace I x] [CompactSpace M] :
  TauCeti.IsLiouvilleDomain (TauCeti.CotangentBundle.symplecticForm I M)
    (-TauCeti.CotangentBundle.liouvilleForm I M) (TauCeti.CotangentBundle.codiscBundle I M)
Lean

Formalized in Tau Ceti as TauCeti.CotangentBundle.isLiouvilleDomain_codiscBundle.

Sources
LeanTauCeti.CotangentBundle.isLiouvilleDomain_codiscBundle
Uses 4
Statement usesTauCeti.CotangentBundle · TauCeti.IsLiouvilleDomain
Proof usesChart formula for the canonical symplectic form · TauCeti.CotangentBundle.isSymplectic_symplecticForm

AbbreviationTauCeti.loopChainAlgebra#

The chain algebra of the Moore loop space: C_*(Ω_b B; R), the normalized cubical chains of the Moore loops at b, with the Pontryagin product.

TauCeti.loopChainAlgebra.{u_1, u_2} (B : Type u_1) [TopologicalSpace B] (b : B) (R : Type u_2)
  [CommRing R] : Type (max u_2 u_1)
Lean

Formalized in Tau Ceti as TauCeti.loopChainAlgebra.

Sources
LeanTauCeti.loopChainAlgebra
Used by 1
Used byTauCeti.fibrationLocalSystem

AbbreviationTauCeti.fibrationLocalSystem#

The DG local system of a map p : E → B at b: the normalized cubical chains of the fibre F' of the Moore-path replacement, a right DG module over C_*(Ω_b B; R) through the strict action of the Moore loops.

TauCeti.fibrationLocalSystem.{u, u_1} {E B : Type u} [TopologicalSpace E] [TopologicalSpace B]
  (R : Type u_1) [CommRing R] (p : C(E, B)) (b : B) : TauCeti.DGLocalSystem B b R
Lean

Formalized in Tau Ceti as TauCeti.fibrationLocalSystem.

Sources
LeanTauCeti.fibrationLocalSystem
Uses 1
Statement usesTauCeti.loopChainAlgebra

StructureTauCeti.IsLiouvilleDomain#

A subset W of a manifold M is a Liouville domain for the smooth two-form ω, with primitive α, when ω is nondegenerate, dα = ω, W is compact and lies in the interior of M, and the Liouville field of α points strictly outwards along the boundary of W: some smooth vector field Z with ι_Z ω = α and some continuous function f and value c satisfy W = {f ≤ c}, with f smooth and df(Z) > 0 at every point of the level f⁻¹(c). The nondegeneracy of ω makes Z unique, and the condition along f⁻¹(c) makes c a regular value of f, so that W is a compact domain with smooth boundary f⁻¹(c).

TauCeti.IsLiouvilleDomain.{u_1, u_2, u_3} {E : Type u_1} {H : Type u_2} {M : Type u_3}
  [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H}
  [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] (ω : TauCeti.SmoothTwoForm I M)
  (α : TauCeti.SmoothForm I M ℝ 1) (W : Set M) : Prop
Lean

Formalized in Tau Ceti as TauCeti.IsLiouvilleDomain.

Sources
LeanTauCeti.IsLiouvilleDomain
Used by 2
Used byThe boundary of a Liouville domain is of restricted contact type · The unit codisc bundle is a Liouville domain

TheoremThe boundary of a Liouville domain is of restricted contact type#

On a finite-dimensional manifold without boundary, a Liouville domain W is the sublevel set {f ≤ c} of a function f, C¹ along the level f⁻¹(c), of which c is a regular value; the frontier of W is exactly the level; and the level, with its atlas TauCeti.regularLevelChartedSpace, is a hypersurface of restricted contact type for the primitive α.

TauCeti.IsLiouvilleDomain.exists_isRestrictedContactType.{u_1, u_2, u_3} {E : Type u_1}
  {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M]
  {ω : TauCeti.SmoothTwoForm I M} {α : TauCeti.SmoothForm I M ℝ 1} {W : Set M} [I.Boundaryless]
  [FiniteDimensional ℝ E] (h : TauCeti.IsLiouvilleDomain ω α W) :
  ∃ f c,
    ∃ (hf : ∀ (x : M), f x = c → ContMDiffAt I (modelWithCornersSelf ℝ ℝ) 1 f x) (hreg :
      TauCeti.IsRegularValue I (modelWithCornersSelf ℝ ℝ) f c),
      W = {x | f x ≤ c} ∧
        frontier W = {x | f x = c} ∧
          TauCeti.IsRestrictedContactType
            (modelWithCornersSelf ℝ (Fin (Module.finrank ℝ E - 1) → ℝ)) (↑ω) (↑α) Subtype.val
Lean

Formalized in Tau Ceti as TauCeti.IsLiouvilleDomain.exists_isRestrictedContactType.

Sources
LeanTauCeti.IsLiouvilleDomain.exists_isRestrictedContactType
Uses 4
Statement usesTauCeti.IsLiouvilleDomain
Proof usesFermat's theorem on a manifold · Homeomorph.pullbackChartedSpace · Homeomorph.pullbackDiffeomorph

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.