Moment-angle complexes and total integral homology

import Mathlib

/-!
# Concrete objects for the moment-angle-manifold theorem

This file gives transparent definitions for every object occurring in the
headline existence theorem of Han--Li.  Mathlib's
`AbstractSimplicialComplex` records all nonempty faces and requires every
singleton to be a face.  The helper `IsFaceOrEmpty` restores the conventional
empty face when defining the moment-angle complex.
-/

noncomputable section

open CategoryTheory

namespace MomentAngle

/-- A face in the usual convention: either the empty face or one of the
nonempty faces stored by Mathlib's `AbstractSimplicialComplex`. -/
def IsFaceOrEmpty {m : ℕ} (L : AbstractSimplicialComplex (Fin m))
    (sigma : Finset (Fin m)) : Prop :=
  sigma = ∅ ∨ sigma ∈ L

/-- The standard barycentric-coordinate geometric realization of a finite
abstract simplicial complex. -/
abbrev GeometricRealization {m : ℕ} (L : AbstractSimplicialComplex (Fin m)) : Type :=
  {x : Fin m → ℝ //
    (∀ i, 0 ≤ x i) ∧
      (∑ i, x i) = 1 ∧
      (Finset.univ.filter fun i => x i ≠ 0) ∈ L}

/-- The ordinary topological four-sphere, realized as the unit sphere in
five-dimensional Euclidean space. -/
abbrev FourSphere : Type :=
  Metric.sphere (0 : EuclideanSpace ℝ (Fin 5)) 1

/-- A finite abstract simplicial complex is a simplicial four-sphere when its
standard geometric realization is homeomorphic to `S⁴`. -/
def IsSimplicialFourSphere {m : ℕ}
    (L : AbstractSimplicialComplex (Fin m)) : Prop :=
  Nonempty (GeometricRealization L ≃ₜ FourSphere)

/-- Membership in the moment-angle complex associated with `L`.  A coordinate
belonging to the chosen face lies in `D²`; every other coordinate lies in
`S¹`. -/
def IsInMomentAngle {m : ℕ} (L : AbstractSimplicialComplex (Fin m))
    (z : Fin m → ℂ) : Prop :=
  ∃ sigma : Finset (Fin m),
    IsFaceOrEmpty L sigma ∧
      ∀ i, if i ∈ sigma then ‖z i‖ ≤ 1 else ‖z i‖ = 1

/-- The moment-angle complex `Z_L` as the corresponding subspace of
`(D²)^m`. -/
abbrev Complex {m : ℕ} (L : AbstractSimplicialComplex (Fin m)) : Type :=
  {z : Fin m → ℂ // IsInMomentAngle L z}

/-- The all-ones point, used as the canonical basepoint of `Z_L`. -/
def basepoint {m : ℕ} (L : AbstractSimplicialComplex (Fin m)) : Complex L := by
  refine ⟨fun _ => 1, ∅, Or.inl rfl, ?_⟩
  simp

/-- The based loop space of `Z_L`.  Mathlib equips `Path` with the topology
induced from the compact-open topology on continuous maps. -/
abbrev BasedLoopSpace {m : ℕ} (L : AbstractSimplicialComplex (Fin m)) : Type :=
  Path (basepoint L) (basepoint L)

/-- Integral singular homology in degree `q`, using Mathlib's singular
homology functor with coefficients in the rank-one module `ℤ`. -/
abbrev IntegralHomology (q : ℕ) (X : Type) [TopologicalSpace X] : Type :=
  (((AlgebraicTopology.singularHomologyFunctor (ModuleCat ℤ) q).obj
      (ModuleCat.of ℤ ℤ)).obj (TopCat.of X))

/-- Total integral singular homology, regarded as the direct sum of its
nonnegative-degree homology groups. -/
abbrev TotalIntegralHomology (X : Type) [TopologicalSpace X] : Type :=
  DirectSum ℕ (fun q => IntegralHomology q X)

/-- `G` occurs as an additive subgroup of `H`. -/
def AdditivelyEmbeds (G H : Type*) [AddZero G] [AddZero H] : Prop :=
  ∃ f : G →+ H, Function.Injective f

end MomentAngle