Support of homological complexes

Given an embedding e : c.Embedding c' of complex shapes, we say that K : HomologicalComplex C c' is supported (resp. strictly supported) on e if K is exact in degree i' (resp. K.X i' is zero) whenever i' is not of the form e.f i. This defines two typeclasses K.IsSupported e and K.IsStrictlySupported e.

We also define predicates K.IsSupportedOutside e and K.IsStrictlySupportedOutside e when the conditions above are satisfied for those i' that are of the form e.f i. (These two predicates are not made typeclasses because in most practical applications, they are equivalent to K.IsSupported e' or K.IsStrictlySupported e' for a complementary embedding e'.)

class HomologicalComplex.IsStrictlySupported {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c') (e : c.Embedding c') : Prop

If K : HomologicalComplex C c', then K.IsStrictlySupported e holds for an embedding e : c.Embedding c' of complex shapes if K.X i' is zero wheneverm i' is not of the form e.f i for some i.

• isZero : ∀ (i' : ι'), (∀ (i : ι), e.f i ≠ i') → CategoryTheory.Limits.IsZero (K.X i')

theorem HomologicalComplex.isZero_X_of_isStrictlySupported {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c') (e : c.Embedding c') [K.IsStrictlySupported e] (i' : ι') (hi' : ∀ (i : ι), e.f i ≠ i') : CategoryTheory.Limits.IsZero (K.X i')

theorem HomologicalComplex.isStrictlySupported_of_iso {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K L : HomologicalComplex C c'} (e' : K ≅ L) (e : c.Embedding c') [K.IsStrictlySupported e] : L.IsStrictlySupported e

class HomologicalComplex.IsSupported {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c') (e : c.Embedding c') : Prop

If K : HomologicalComplex C c', then K.IsStrictlySupported e holds for an embedding e : c.Embedding c' of complex shapes if K is exact at i' whenever i' is not of the form e.f i for some i.

• exactAt : ∀ (i' : ι'), (∀ (i : ι), e.f i ≠ i') → K.ExactAt i'

theorem HomologicalComplex.exactAt_of_isSupported {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c') (e : c.Embedding c') [K.IsSupported e] (i' : ι') (hi' : ∀ (i : ι), e.f i ≠ i') : K.ExactAt i'

theorem HomologicalComplex.isSupported_of_iso {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K L : HomologicalComplex C c'} (e' : K ≅ L) (e : c.Embedding c') [K.IsSupported e] : L.IsSupported e

instance HomologicalComplex.instIsSupportedOfIsStrictlySupported {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c') (e : c.Embedding c') [K.IsStrictlySupported e] : K.IsSupported e

Equations

• ⋯ = ⋯

structure HomologicalComplex.IsStrictlySupportedOutside {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c') (e : c.Embedding c') : Prop

If K : HomologicalComplex C c', then K.IsStrictlySupportedOutside e holds for an embedding e : c.Embedding c' of complex shapes if K.X (e.f i) is zero for all i.

• isZero : ∀ (i : ι), CategoryTheory.Limits.IsZero (K.X (e.f i))

structure HomologicalComplex.IsSupportedOutside {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c') (e : c.Embedding c') : Prop

If K : HomologicalComplex C c', then K.IsSupportedOutside e holds for an embedding e : c.Embedding c' of complex shapes if K is exact at e.f i for all i.

• exactAt : ∀ (i : ι), K.ExactAt (e.f i)

theorem HomologicalComplex.IsStrictlySupportedOutside.isSupportedOutside {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : HomologicalComplex C c'} {e : c.Embedding c'} (h : K.IsStrictlySupportedOutside e) : K.IsSupportedOutside e

instance HomologicalComplex.instIsStrictlySupportedOfNat {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] (e : c.Embedding c') [CategoryTheory.Limits.HasZeroObject C] : HomologicalComplex.IsStrictlySupported 0 e

Equations

• ⋯ = ⋯

theorem HomologicalComplex.isZero_iff_isStrictlySupported_and_isStrictlySupportedOutside {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c') (e : c.Embedding c') : CategoryTheory.Limits.IsZero K ↔ K.IsStrictlySupported e ∧ K.IsStrictlySupportedOutside e

instance HomologicalComplex.instIsStrictlySupportedOppositeOpOp {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c') (e : c.Embedding c') [K.IsStrictlySupported e] : K.op.IsStrictlySupported e.op

Equations

• ⋯ = ⋯

instance HomologicalComplex.map_isStrictlySupported {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3} {D : Type u_4} [CategoryTheory.Category.{u_5, u_3} C] [CategoryTheory.Category.{u_6, u_4} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] (K : HomologicalComplex C c') (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] (e : c.Embedding c') [K.IsStrictlySupported e] : ((F.mapHomologicalComplex c').obj K).IsStrictlySupported e

Equations

• ⋯ = ⋯