Complementary embeddings #
Given two embeddings e₁ : c₁.Embedding c and e₂ : c₂.Embedding c
of complex shapes, we introduce a property e₁.AreComplementary e₂
saying that the image subsets of the indices of c₁ and c₂ form
a partition of the indices of c.
If e₁.IsTruncLE and e₂.IsTruncGE, and K : HomologicalComplex C c,
we construct a quasi-isomorphism shortComplexTruncLEX₃ToTruncGE between
the cokernel of K.ιTruncLE e₁ : K.truncLE e₁ ⟶ K and K.truncGE e₂.
structure
ComplexShape.Embedding.AreComplementary
{ι : Type u_1}
{ι₁ : Type u_2}
{ι₂ : Type u_3}
{c : ComplexShape ι}
{c₁ : ComplexShape ι₁}
{c₂ : ComplexShape ι₂}
(e₁ : c₁.Embedding c)
(e₂ : c₂.Embedding c)
:
Two embedding e₁ and e₂ into a complex shape c : ComplexShape ι
are complementary when the range of e₁.f and e₂.f form a partition of ι.
Instances For
theorem
ComplexShape.Embedding.AreComplementary.symm
{ι : Type u_1}
{ι₁ : Type u_2}
{ι₂ : Type u_3}
{c : ComplexShape ι}
{c₁ : ComplexShape ι₁}
{c₂ : ComplexShape ι₂}
{e₁ : c₁.Embedding c}
{e₂ : c₂.Embedding c}
(ac : e₁.AreComplementary e₂)
:
e₂.AreComplementary e₁
theorem
ComplexShape.Embedding.AreComplementary.exists_i₁
{ι : Type u_1}
{ι₁ : Type u_2}
{ι₂ : Type u_3}
{c : ComplexShape ι}
{c₁ : ComplexShape ι₁}
{c₂ : ComplexShape ι₂}
{e₁ : c₁.Embedding c}
{e₂ : c₂.Embedding c}
(ac : e₁.AreComplementary e₂)
(i : ι)
(hi : ∀ (i₂ : ι₂), e₂.f i₂ ≠ i)
:
theorem
ComplexShape.Embedding.AreComplementary.exists_i₂
{ι : Type u_1}
{ι₁ : Type u_2}
{ι₂ : Type u_3}
{c : ComplexShape ι}
{c₁ : ComplexShape ι₁}
{c₂ : ComplexShape ι₂}
{e₁ : c₁.Embedding c}
{e₂ : c₂.Embedding c}
(ac : e₁.AreComplementary e₂)
(i : ι)
(hi : ∀ (i₁ : ι₁), e₁.f i₁ ≠ i)
:
def
ComplexShape.Embedding.AreComplementary.fromSum
{ι : Type u_1}
{ι₁ : Type u_2}
{ι₂ : Type u_3}
{c : ComplexShape ι}
{c₁ : ComplexShape ι₁}
{c₂ : ComplexShape ι₂}
(e₁ : c₁.Embedding c)
(e₂ : c₂.Embedding c)
:
ι₁ ⊕ ι₂ → ι
Given complementary embeddings of complex shapes
e₁ : Embedding c₁ c and e₂ : Embedding c₂ c, this is
the obvious map ι₁ ⊕ ι₂ → ι from the sum of the index
types of c₁ and c₂ to the index type of c.
Equations
Instances For
theorem
ComplexShape.Embedding.AreComplementary.fromSum_bijective
{ι : Type u_1}
{ι₁ : Type u_2}
{ι₂ : Type u_3}
{c : ComplexShape ι}
{c₁ : ComplexShape ι₁}
{c₂ : ComplexShape ι₂}
{e₁ : c₁.Embedding c}
{e₂ : c₂.Embedding c}
(ac : e₁.AreComplementary e₂)
:
Function.Bijective (fromSum e₁ e₂)
noncomputable def
ComplexShape.Embedding.AreComplementary.equiv
{ι : Type u_1}
{ι₁ : Type u_2}
{ι₂ : Type u_3}
{c : ComplexShape ι}
{c₁ : ComplexShape ι₁}
{c₂ : ComplexShape ι₂}
{e₁ : c₁.Embedding c}
{e₂ : c₂.Embedding c}
(ac : e₁.AreComplementary e₂)
:
Given complementary embeddings of complex shapes
e₁ : Embedding c₁ c and e₂ : Embedding c₂ c, this is
the obvious bijection ι₁ ⊕ ι₂ ≃ ι from the sum of the index
types of c₁ and c₂ to the index type of c.
Equations
Instances For
@[simp]
theorem
ComplexShape.Embedding.AreComplementary.equiv_inl
{ι : Type u_1}
{ι₁ : Type u_2}
{ι₂ : Type u_3}
{c : ComplexShape ι}
{c₁ : ComplexShape ι₁}
{c₂ : ComplexShape ι₂}
{e₁ : c₁.Embedding c}
{e₂ : c₂.Embedding c}
(ac : e₁.AreComplementary e₂)
(i₁ : ι₁)
:
@[simp]
theorem
ComplexShape.Embedding.AreComplementary.equiv_inr
{ι : Type u_1}
{ι₁ : Type u_2}
{ι₂ : Type u_3}
{c : ComplexShape ι}
{c₁ : ComplexShape ι₁}
{c₂ : ComplexShape ι₂}
{e₁ : c₁.Embedding c}
{e₂ : c₂.Embedding c}
(ac : e₁.AreComplementary e₂)
(i₂ : ι₂)
:
def
ComplexShape.Embedding.AreComplementary.desc'
{ι : Type u_1}
{ι₁ : Type u_2}
{ι₂ : Type u_3}
{c : ComplexShape ι}
{c₁ : ComplexShape ι₁}
{c₂ : ComplexShape ι₂}
{e₁ : c₁.Embedding c}
{e₂ : c₂.Embedding c}
(ac : e₁.AreComplementary e₂)
{X : ι → Type u_5}
(x₁ : (i₁ : ι₁) → X (e₁.f i₁))
(x₂ : (i₂ : ι₂) → X (e₂.f i₂))
(i : ι₁ ⊕ ι₂)
:
X (ac.equiv i)
Auxiliary definition for desc.
Equations
Instances For
theorem
ComplexShape.Embedding.AreComplementary.desc'_inl
{ι : Type u_1}
{ι₁ : Type u_2}
{ι₂ : Type u_3}
{c : ComplexShape ι}
{c₁ : ComplexShape ι₁}
{c₂ : ComplexShape ι₂}
{e₁ : c₁.Embedding c}
{e₂ : c₂.Embedding c}
(ac : e₁.AreComplementary e₂)
{X : ι → Type u_5}
(x₁ : (i₁ : ι₁) → X (e₁.f i₁))
(x₂ : (i₂ : ι₂) → X (e₂.f i₂))
(i : ι₁ ⊕ ι₂)
(i₁ : ι₁)
(h : Sum.inl i₁ = i)
:
theorem
ComplexShape.Embedding.AreComplementary.desc'_inr
{ι : Type u_1}
{ι₁ : Type u_2}
{ι₂ : Type u_3}
{c : ComplexShape ι}
{c₁ : ComplexShape ι₁}
{c₂ : ComplexShape ι₂}
{e₁ : c₁.Embedding c}
{e₂ : c₂.Embedding c}
(ac : e₁.AreComplementary e₂)
{X : ι → Type u_5}
(x₁ : (i₁ : ι₁) → X (e₁.f i₁))
(x₂ : (i₂ : ι₂) → X (e₂.f i₂))
(i : ι₁ ⊕ ι₂)
(i₂ : ι₂)
(h : Sum.inr i₂ = i)
:
noncomputable def
ComplexShape.Embedding.AreComplementary.desc
{ι : Type u_1}
{ι₁ : Type u_2}
{ι₂ : Type u_3}
{c : ComplexShape ι}
{c₁ : ComplexShape ι₁}
{c₂ : ComplexShape ι₂}
{e₁ : c₁.Embedding c}
{e₂ : c₂.Embedding c}
(ac : e₁.AreComplementary e₂)
{X : ι → Type u_5}
(x₁ : (i₁ : ι₁) → X (e₁.f i₁))
(x₂ : (i₂ : ι₂) → X (e₂.f i₂))
(i : ι)
:
X i
If ι₁ and ι₂ are the index types of complementary embeddings into a
complex shape of index type ι, this is a constructor for (dependent) maps from ι,
which takes as inputs the "restrictions" to ι₁ and ι₂.
Equations
Instances For
theorem
ComplexShape.Embedding.AreComplementary.desc_inl
{ι : Type u_1}
{ι₁ : Type u_2}
{ι₂ : Type u_3}
{c : ComplexShape ι}
{c₁ : ComplexShape ι₁}
{c₂ : ComplexShape ι₂}
{e₁ : c₁.Embedding c}
{e₂ : c₂.Embedding c}
(ac : e₁.AreComplementary e₂)
{X : ι → Type u_5}
(x₁ : (i₁ : ι₁) → X (e₁.f i₁))
(x₂ : (i₂ : ι₂) → X (e₂.f i₂))
(i₁ : ι₁)
:
theorem
ComplexShape.Embedding.AreComplementary.desc_inr
{ι : Type u_1}
{ι₁ : Type u_2}
{ι₂ : Type u_3}
{c : ComplexShape ι}
{c₁ : ComplexShape ι₁}
{c₂ : ComplexShape ι₂}
{e₁ : c₁.Embedding c}
{e₂ : c₂.Embedding c}
(ac : e₁.AreComplementary e₂)
{X : ι → Type u_5}
(x₁ : (i₁ : ι₁) → X (e₁.f i₁))
(x₂ : (i₂ : ι₂) → X (e₂.f i₂))
(i₂ : ι₂)
:
theorem
ComplexShape.Embedding.AreComplementary.isStrictlySupportedOutside₁_iff
{ι : Type u_1}
{ι₁ : Type u_2}
{ι₂ : Type u_3}
{c : ComplexShape ι}
{c₁ : ComplexShape ι₁}
{c₂ : ComplexShape ι₂}
{C : Type u_4}
[CategoryTheory.Category.{u_5, u_4} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{e₁ : c₁.Embedding c}
{e₂ : c₂.Embedding c}
(ac : e₁.AreComplementary e₂)
(K : HomologicalComplex C c)
:
theorem
ComplexShape.Embedding.AreComplementary.isStrictlySupportedOutside₂_iff
{ι : Type u_1}
{ι₁ : Type u_2}
{ι₂ : Type u_3}
{c : ComplexShape ι}
{c₁ : ComplexShape ι₁}
{c₂ : ComplexShape ι₂}
{C : Type u_4}
[CategoryTheory.Category.{u_5, u_4} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{e₁ : c₁.Embedding c}
{e₂ : c₂.Embedding c}
(ac : e₁.AreComplementary e₂)
(K : HomologicalComplex C c)
:
theorem
ComplexShape.Embedding.AreComplementary.isSupportedOutside₁_iff
{ι : Type u_1}
{ι₁ : Type u_2}
{ι₂ : Type u_3}
{c : ComplexShape ι}
{c₁ : ComplexShape ι₁}
{c₂ : ComplexShape ι₂}
{C : Type u_4}
[CategoryTheory.Category.{u_5, u_4} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{e₁ : c₁.Embedding c}
{e₂ : c₂.Embedding c}
(ac : e₁.AreComplementary e₂)
(K : HomologicalComplex C c)
:
theorem
ComplexShape.Embedding.AreComplementary.isSupportedOutside₂_iff
{ι : Type u_1}
{ι₁ : Type u_2}
{ι₂ : Type u_3}
{c : ComplexShape ι}
{c₁ : ComplexShape ι₁}
{c₂ : ComplexShape ι₂}
{C : Type u_4}
[CategoryTheory.Category.{u_5, u_4} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{e₁ : c₁.Embedding c}
{e₂ : c₂.Embedding c}
(ac : e₁.AreComplementary e₂)
(K : HomologicalComplex C c)
:
theorem
ComplexShape.Embedding.AreComplementary.hom_ext'
{ι : Type u_1}
{ι₁ : Type u_2}
{ι₂ : Type u_3}
{c : ComplexShape ι}
{c₁ : ComplexShape ι₁}
{c₂ : ComplexShape ι₂}
{C : Type u_4}
[CategoryTheory.Category.{u_5, u_4} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{e₁ : c₁.Embedding c}
{e₂ : c₂.Embedding c}
(ac : e₁.AreComplementary e₂)
{K L : HomologicalComplex C c}
(φ : K ⟶ L)
(hK : K.IsStrictlySupportedOutside e₂)
(hL : L.IsStrictlySupportedOutside e₁)
:
Variant of hom_ext.
theorem
ComplexShape.Embedding.AreComplementary.hom_ext
{ι : Type u_1}
{ι₁ : Type u_2}
{ι₂ : Type u_3}
{c : ComplexShape ι}
{c₁ : ComplexShape ι₁}
{c₂ : ComplexShape ι₂}
{C : Type u_4}
[CategoryTheory.Category.{u_5, u_4} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{e₁ : c₁.Embedding c}
{e₂ : c₂.Embedding c}
(ac : e₁.AreComplementary e₂)
{K L : HomologicalComplex C c}
[K.IsStrictlySupported e₁]
[L.IsStrictlySupported e₂]
(φ : K ⟶ L)
:
def
ComplexShape.Embedding.AreComplementary.Boundary
{ι : Type u_1}
{ι₁ : Type u_2}
{ι₂ : Type u_3}
{c : ComplexShape ι}
{c₁ : ComplexShape ι₁}
{c₂ : ComplexShape ι₂}
{e₁ : c₁.Embedding c}
{e₂ : c₂.Embedding c}
:
e₁.AreComplementary e₂ → (i₁ : ι₁) → (i₂ : ι₂) → Prop
If e₁ and e₂ are complementary embeddings into a complex shape c,
indices i₁ and i₂ are at the boundary if c.Rel (e₁.f i₁) (e₂.f i₂).
Equations
Instances For
theorem
ComplexShape.Embedding.AreComplementary.Boundary.fst
{ι : Type u_1}
{ι₁ : Type u_2}
{ι₂ : Type u_3}
{c : ComplexShape ι}
{c₁ : ComplexShape ι₁}
{c₂ : ComplexShape ι₂}
{e₁ : c₁.Embedding c}
{e₂ : c₂.Embedding c}
{ac : e₁.AreComplementary e₂}
{i₁ : ι₁}
{i₂ : ι₂}
(h : ac.Boundary i₁ i₂)
:
e₁.BoundaryLE i₁
theorem
ComplexShape.Embedding.AreComplementary.Boundary.snd
{ι : Type u_1}
{ι₁ : Type u_2}
{ι₂ : Type u_3}
{c : ComplexShape ι}
{c₁ : ComplexShape ι₁}
{c₂ : ComplexShape ι₂}
{e₁ : c₁.Embedding c}
{e₂ : c₂.Embedding c}
{ac : e₁.AreComplementary e₂}
{i₁ : ι₁}
{i₂ : ι₂}
(h : ac.Boundary i₁ i₂)
:
e₂.BoundaryGE i₂
theorem
ComplexShape.Embedding.AreComplementary.Boundary.fst_inj
{ι : Type u_1}
{ι₁ : Type u_2}
{ι₂ : Type u_3}
{c : ComplexShape ι}
{c₁ : ComplexShape ι₁}
{c₂ : ComplexShape ι₂}
{e₁ : c₁.Embedding c}
{e₂ : c₂.Embedding c}
{ac : e₁.AreComplementary e₂}
{i₁ i₁' : ι₁}
{i₂ : ι₂}
(h : ac.Boundary i₁ i₂)
(h' : ac.Boundary i₁' i₂)
:
theorem
ComplexShape.Embedding.AreComplementary.Boundary.snd_inj
{ι : Type u_1}
{ι₁ : Type u_2}
{ι₂ : Type u_3}
{c : ComplexShape ι}
{c₁ : ComplexShape ι₁}
{c₂ : ComplexShape ι₂}
{e₁ : c₁.Embedding c}
{e₂ : c₂.Embedding c}
{ac : e₁.AreComplementary e₂}
{i₁ : ι₁}
{i₂ i₂' : ι₂}
(h : ac.Boundary i₁ i₂)
(h' : ac.Boundary i₁ i₂')
:
theorem
ComplexShape.Embedding.AreComplementary.Boundary.exists₁
{ι : Type u_1}
{ι₁ : Type u_2}
{ι₂ : Type u_3}
{c : ComplexShape ι}
{c₁ : ComplexShape ι₁}
{c₂ : ComplexShape ι₂}
{e₁ : c₁.Embedding c}
{e₂ : c₂.Embedding c}
(ac : e₁.AreComplementary e₂)
{i₁ : ι₁}
(h : e₁.BoundaryLE i₁)
:
∃ (i₂ : ι₂), ac.Boundary i₁ i₂
theorem
ComplexShape.Embedding.AreComplementary.Boundary.exists₂
{ι : Type u_1}
{ι₁ : Type u_2}
{ι₂ : Type u_3}
{c : ComplexShape ι}
{c₁ : ComplexShape ι₁}
{c₂ : ComplexShape ι₂}
{e₁ : c₁.Embedding c}
{e₂ : c₂.Embedding c}
(ac : e₁.AreComplementary e₂)
{i₂ : ι₂}
(h : e₂.BoundaryGE i₂)
:
∃ (i₁ : ι₁), ac.Boundary i₁ i₂
noncomputable def
ComplexShape.Embedding.AreComplementary.Boundary.indexOfBoundaryLE
{ι : Type u_1}
{ι₁ : Type u_2}
{ι₂ : Type u_3}
{c : ComplexShape ι}
{c₁ : ComplexShape ι₁}
{c₂ : ComplexShape ι₂}
{e₁ : c₁.Embedding c}
{e₂ : c₂.Embedding c}
(ac : e₁.AreComplementary e₂)
{i₁ : ι₁}
(h : e₁.BoundaryLE i₁)
:
ι₂
If ac : AreComplementary e₁ e₂ (with e₁ : ComplexShape.Embedding c₁ c and
e₂ : ComplexShape.Embedding c₂ c), and i₁ belongs to e₁.BoundaryLE,
then this is the (unique) index i₂ of c₂ such that ac.Boundary i₁ i₂.
Equations
Instances For
theorem
ComplexShape.Embedding.AreComplementary.Boundary.of_boundaryLE
{ι : Type u_1}
{ι₁ : Type u_2}
{ι₂ : Type u_3}
{c : ComplexShape ι}
{c₁ : ComplexShape ι₁}
{c₂ : ComplexShape ι₂}
{e₁ : c₁.Embedding c}
{e₂ : c₂.Embedding c}
(ac : e₁.AreComplementary e₂)
{i₁ : ι₁}
(h : e₁.BoundaryLE i₁)
:
ac.Boundary i₁ (indexOfBoundaryLE ac h)
noncomputable def
ComplexShape.Embedding.AreComplementary.Boundary.indexOfBoundaryGE
{ι : Type u_1}
{ι₁ : Type u_2}
{ι₂ : Type u_3}
{c : ComplexShape ι}
{c₁ : ComplexShape ι₁}
{c₂ : ComplexShape ι₂}
{e₁ : c₁.Embedding c}
{e₂ : c₂.Embedding c}
(ac : e₁.AreComplementary e₂)
{i₂ : ι₂}
(h : e₂.BoundaryGE i₂)
:
ι₁
If ac : AreComplementary e₁ e₂ (with e₁ : ComplexShape.Embedding c₁ c and
e₂ : ComplexShape.Embedding c₂ c), and i₂ belongs to e₂.BoundaryGE,
then this is the (unique) index i₁ of c₁ such that ac.Boundary i₁ i₂.
Equations
Instances For
theorem
ComplexShape.Embedding.AreComplementary.Boundary.of_boundaryGE
{ι : Type u_1}
{ι₁ : Type u_2}
{ι₂ : Type u_3}
{c : ComplexShape ι}
{c₁ : ComplexShape ι₁}
{c₂ : ComplexShape ι₂}
{e₁ : c₁.Embedding c}
{e₂ : c₂.Embedding c}
(ac : e₁.AreComplementary e₂)
{i₂ : ι₂}
(h : e₂.BoundaryGE i₂)
:
ac.Boundary (indexOfBoundaryGE ac h) i₂
noncomputable def
ComplexShape.Embedding.AreComplementary.Boundary.equiv
{ι : Type u_1}
{ι₁ : Type u_2}
{ι₂ : Type u_3}
{c : ComplexShape ι}
{c₁ : ComplexShape ι₁}
{c₂ : ComplexShape ι₂}
{e₁ : c₁.Embedding c}
{e₂ : c₂.Embedding c}
(ac : e₁.AreComplementary e₂)
:
The bijection Subtype e₁.BoundaryLE ≃ Subtype e₂.BoundaryGE when
e₁ and e₂ are complementary embeddings of complex shapes.
Equations
Instances For
theorem
ComplexShape.Embedding.embeddingUpInt_areComplementary
(n₀ n₁ : ℤ)
(h : n₀ + 1 = n₁)
:
(embeddingUpIntLE n₀).AreComplementary (embeddingUpIntGE n₁)
noncomputable def
HomologicalComplex.shortComplexTruncLEX₃ToTruncGE
{ι : Type u_1}
{ι₁ : Type u_2}
{ι₂ : Type u_3}
{c : ComplexShape ι}
{c₁ : ComplexShape ι₁}
{c₂ : ComplexShape ι₂}
{C : Type u_4}
[CategoryTheory.Category.{u_5, u_4} C]
[CategoryTheory.Abelian C]
(K : HomologicalComplex C c)
{e₁ : c₁.Embedding c}
{e₂ : c₂.Embedding c}
[e₁.IsTruncLE]
[e₂.IsTruncGE]
(ac : e₁.AreComplementary e₂)
:
When e₁ and e₂ are complementary embeddings of complex shapes, with
e₁.IsTruncLE and e₂.IsTruncGE, then this is the canonical quasi-isomorphism
(K.shortComplexTruncLE e₁).X₃ ⟶ K.truncGE e₂ where
(K.shortComplexTruncLE e₁).X₃ is the cokernel of K.ιTruncLE e₁ : K.truncLE e₁ ⟶ K.
Equations
Instances For
@[simp]
theorem
HomologicalComplex.g_shortComplexTruncLEX₃ToTruncGE
{ι : Type u_1}
{ι₁ : Type u_2}
{ι₂ : Type u_3}
{c : ComplexShape ι}
{c₁ : ComplexShape ι₁}
{c₂ : ComplexShape ι₂}
{C : Type u_4}
[CategoryTheory.Category.{u_5, u_4} C]
[CategoryTheory.Abelian C]
(K : HomologicalComplex C c)
{e₁ : c₁.Embedding c}
{e₂ : c₂.Embedding c}
[e₁.IsTruncLE]
[e₂.IsTruncGE]
(ac : e₁.AreComplementary e₂)
:
CategoryTheory.CategoryStruct.comp (K.shortComplexTruncLE e₁).g (K.shortComplexTruncLEX₃ToTruncGE ac) = K.πTruncGE e₂
@[simp]
theorem
HomologicalComplex.g_shortComplexTruncLEX₃ToTruncGE_assoc
{ι : Type u_1}
{ι₁ : Type u_2}
{ι₂ : Type u_3}
{c : ComplexShape ι}
{c₁ : ComplexShape ι₁}
{c₂ : ComplexShape ι₂}
{C : Type u_4}
[CategoryTheory.Category.{u_5, u_4} C]
[CategoryTheory.Abelian C]
(K : HomologicalComplex C c)
{e₁ : c₁.Embedding c}
{e₂ : c₂.Embedding c}
[e₁.IsTruncLE]
[e₂.IsTruncGE]
(ac : e₁.AreComplementary e₂)
{Z : HomologicalComplex C c}
(h : K.truncGE e₂ ⟶ Z)
:
instance
HomologicalComplex.instQuasiIsoShortComplexTruncLEX₃ToTruncGE
{ι : Type u_1}
{ι₁ : Type u_2}
{ι₂ : Type u_3}
{c : ComplexShape ι}
{c₁ : ComplexShape ι₁}
{c₂ : ComplexShape ι₂}
{C : Type u_4}
[CategoryTheory.Category.{u_5, u_4} C]
[CategoryTheory.Abelian C]
(K : HomologicalComplex C c)
{e₁ : c₁.Embedding c}
{e₂ : c₂.Embedding c}
[e₁.IsTruncLE]
[e₂.IsTruncGE]
(ac : e₁.AreComplementary e₂)
: