Naive category theory question

Stream: new members

[Vlad Tsyrklevich]

I'm trying to get started playing with singular homology and I am totally new to category theory in mathlib. I wanted to start off proving something absolutely trivial, e.g. that the empty space has trivial homology. We already have the result that a totally disconnected space has trivial homology >0, and it's zeroth homology is a coproduct in the number of components so this isn't much of a stretch. However, I found even this trivial result fairly painful. I'm new to this part of mathlib so that's partly to be expected, but I think that having to work with isomorphisms instead of equality was part of the difficulty since rw? was useless. I really had to rely on loogle and found it harder to find the necessary pieces. Is there a better way to find isomorphisms using familiar automation? And is there some obvious way to golf it down? e.g. it seems surprising that coproductOfIsEmpty doesn't exist in some form and I'm guessing I just missed it.

import Mathlib

namespace AlgebraicTopology

open CategoryTheory Limits

universe w v u

variable (C : Type u) [Category.{v} C] [HasCoproducts.{w} C]
variable [Preadditive C] [CategoryWithHomology C] (n : ℕ)
variable (R : C) (X : TopCat)

noncomputable
def coproductOfIsEmpty {B C : Type*} [Category* C] [HasCoproducts C] [I : HasInitial C]
    [IsEmpty B] (f : B → C) : ∐ f ≅ initial C :=
  HasColimit.isoOfEquivalence (equivalenceOfIsEmpty _ _) <|
    ((equivalenceOfIsEmpty _ _).functor ⋙ Functor.empty C).isEmptyExt _

lemma empty [IsEmpty X] (n : ℕ) : IsZero (((singularHomologyFunctor C n).obj R).obj X) := by
  have := hasCoproducts_shrink.{0, w} (C := C)
  have : HasZeroObject C := ⟨_, initialIsInitial.isZero⟩
  by_cases h : n = 0
  · have := singularHomologyFunctorZeroOfTotallyDisconnectedSpace C R X ≪≫ (coproductOfIsEmpty _)
    exact h ▸ CategoryTheory.Limits.IsZero.of_iso (IsZero.of_mono_zero _ R) this
  · exact isZero_singularHomologyFunctor_of_totallyDisconnectedSpace _ _ _ _ h

[Andrew Yang]

I think the relavent lemma is docs#CategoryTheory.Limits.isColimitEquivIsInitialOfIsEmpty. I found it via loogling CategoryTheory.Functor ?A ?B, IsEmpty ?A

[Vlad Tsyrklevich]

Thank you for the pointer! I was able to golf it down to

lemma empty [IsEmpty X] (n : ℕ) : IsZero (((singularHomologyFunctor C n).obj R).obj X) := by
  by_cases h : n = 0
  · exact h ▸ (IsInitial.isZero <|
      isColimitEquivIsInitialOfIsEmpty _ _ (colimit.isColimit _) |>.ofIso
        (singularHomologyFunctorZeroOfTotallyDisconnectedSpace ..).symm)
  · exact isZero_singularHomologyFunctor_of_totallyDisconnectedSpace _ _ _ _ h

[Joël Riou]

The following proof is more direct as it uses the fact that the whole complex is zero:

import Mathlib.AlgebraicTopology.SingularHomology.Basic

open CategoryTheory Limits AlgebraicTopology Simplicial Opposite

variable (X : TopCat) {C : Type*} [Category* C] [HasCoproducts C] [Preadditive C]
  [CategoryWithHomology C] (R : C)

lemma empty [IsEmpty X] (n : ℕ) :
    IsZero (((singularHomologyFunctor C n).obj R).obj X) :=
  have : IsEmpty ((TopCat.toSSet.obj X _⦋n⦌)) := ⟨fun f ↦
    IsEmpty.false (X.toSSetObjEquiv (op ⦋n⦌) f (Classical.arbitrary _))⟩
  ShortComplex.isZero_homology_of_isZero_X₂ _
    (IsInitial.isZero (isColimitEquivIsInitialOfIsEmpty _ _ (colimit.isColimit _)))

[Vlad Tsyrklevich]

Thanks! I wanted to look at actually dealing with complexes next