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')
:
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')
Instances
theorem
HomologicalComplex.IsStrictlySupported.isZero
{ι : 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'}
[self : K.IsStrictlySupported e]
(i' : ι')
(hi' : ∀ (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 : HomologicalComplex C c'}
{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')
:
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'
Instances
theorem
HomologicalComplex.IsSupported.exactAt
{ι : 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'}
[self : K.IsSupported e]
(i' : ι')
(hi' : ∀ (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 : HomologicalComplex C c'}
{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')
:
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))
Instances For
theorem
HomologicalComplex.IsStrictlySupportedOutside.isZero
{ι : 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'}
(self : K.IsStrictlySupportedOutside e)
(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')
:
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)
Instances For
theorem
HomologicalComplex.IsSupportedOutside.exactAt
{ι : 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'}
(self : K.IsSupportedOutside e)
(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]
:
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
- ⋯ = ⋯