Lifting properties in cochain complexes #
Let C be an abelian category. Consider a commutative diagram
in the category CochainComplex C ℤ.
t
A ⟶ X
i| |p
v v
B ⟶ Y
b
Assume that there exists a degreewise lifting B.X n ⟶ X.X n for any n : ℤ,
that Q is a cokernel of i, and K is a kernel of p. In this situation,
we construct a cocycle in Cocycle Q K 1 and show that there exists
a lifting B ⟶ X if this cocycle is a coboundary.
@[reducible, inline]
abbrev
CochainComplex.Lifting.cochain₀
{C : Type u_1}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Abelian C]
{A B X Y : CochainComplex C ℤ}
{t : A ⟶ X}
{i : A ⟶ B}
{p : X ⟶ Y}
{b : B ⟶ Y}
(sq : CategoryTheory.CommSq t i p b)
(hsq : (n : ℤ) → ⋯.LiftStruct)
:
HomComplex.Cochain B X 0
The 0-cochain from B to X given by the degreewise liftings.
Instances For
def
CochainComplex.Lifting.cocycle₁'
{C : Type u_1}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Abelian C]
{A B X Y : CochainComplex C ℤ}
{t : A ⟶ X}
{i : A ⟶ B}
{p : X ⟶ Y}
{b : B ⟶ Y}
(sq : CategoryTheory.CommSq t i p b)
(hsq : (n : ℤ) → ⋯.LiftStruct)
:
HomComplex.Cocycle B X 1
A 1-cocycle from B to X obtained as the boundary of
the 0-cochain cochain₀ sq hsq consisting of the degreewise liftings.
This is refined below as a 1-cocycle from Q to K where Q is a
cokernel of i : A ⟶ B and K a kernel of p : X ⟶ Y (see cocycle₁).
Instances For
@[simp]
theorem
CochainComplex.Lifting.coe_cocycle₁'_v_comp_eq_zero
{C : Type u_1}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Abelian C]
{A B X Y : CochainComplex C ℤ}
{t : A ⟶ X}
{i : A ⟶ B}
{p : X ⟶ Y}
{b : B ⟶ Y}
(sq : CategoryTheory.CommSq t i p b)
(hsq : (n : ℤ) → ⋯.LiftStruct)
(n m : ℤ)
(hnm : n + 1 = m := by lia)
:
CategoryTheory.CategoryStruct.comp ((↑(cocycle₁' sq hsq)).v n m hnm) (p.f m) = 0
@[simp]
theorem
CochainComplex.Lifting.coe_cocycle₁'_v_comp_eq_zero_assoc
{C : Type u_1}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Abelian C]
{A B X Y : CochainComplex C ℤ}
{t : A ⟶ X}
{i : A ⟶ B}
{p : X ⟶ Y}
{b : B ⟶ Y}
(sq : CategoryTheory.CommSq t i p b)
(hsq : (n : ℤ) → ⋯.LiftStruct)
(n m : ℤ)
(hnm : n + 1 = m := by lia)
{Z : C}
(h : Y.X m ⟶ Z)
:
CategoryTheory.CategoryStruct.comp ((↑(cocycle₁' sq hsq)).v n m hnm) (CategoryTheory.CategoryStruct.comp (p.f m) h) = CategoryTheory.CategoryStruct.comp 0 h
@[simp]
theorem
CochainComplex.Lifting.comp_coe_cocyle₁'_v_eq_zero
{C : Type u_1}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Abelian C]
{A B X Y : CochainComplex C ℤ}
{t : A ⟶ X}
{i : A ⟶ B}
{p : X ⟶ Y}
{b : B ⟶ Y}
(sq : CategoryTheory.CommSq t i p b)
(hsq : (n : ℤ) → ⋯.LiftStruct)
(n m : ℤ)
(hnm : n + 1 = m := by lia)
:
CategoryTheory.CategoryStruct.comp (i.f n) ((↑(cocycle₁' sq hsq)).v n m hnm) = 0
@[simp]
theorem
CochainComplex.Lifting.comp_coe_cocyle₁'_v_eq_zero_assoc
{C : Type u_1}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Abelian C]
{A B X Y : CochainComplex C ℤ}
{t : A ⟶ X}
{i : A ⟶ B}
{p : X ⟶ Y}
{b : B ⟶ Y}
(sq : CategoryTheory.CommSq t i p b)
(hsq : (n : ℤ) → ⋯.LiftStruct)
(n m : ℤ)
(hnm : n + 1 = m := by lia)
{Z : C}
(h : X.X m ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (i.f n) (CategoryTheory.CategoryStruct.comp ((↑(cocycle₁' sq hsq)).v n m hnm) h) = CategoryTheory.CategoryStruct.comp 0 h
theorem
CochainComplex.Lifting.exists_hom
{C : Type u_1}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Abelian C]
{A B X Y : CochainComplex C ℤ}
{t : A ⟶ X}
{i : A ⟶ B}
{p : X ⟶ Y}
{b : B ⟶ Y}
(sq : CategoryTheory.CommSq t i p b)
(hsq : (n : ℤ) → ⋯.LiftStruct)
{Q : CochainComplex C ℤ}
{π : B ⟶ Q}
{hπ : CategoryTheory.CategoryStruct.comp i π = 0}
(hQ : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ π hπ))
{K : CochainComplex C ℤ}
{ι : K ⟶ X}
{hι : CategoryTheory.CategoryStruct.comp ι p = 0}
(hK : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι ι hι))
(n m : ℤ)
(hnm : n + 1 = m := by lia)
:
∃ (φ : Q.X n ⟶ K.X m),
CategoryTheory.CategoryStruct.comp (π.f n) (CategoryTheory.CategoryStruct.comp φ (ι.f m)) = (↑(cocycle₁' sq hsq)).v n m hnm
noncomputable def
CochainComplex.Lifting.cochain₁
{C : Type u_1}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Abelian C]
{A B X Y : CochainComplex C ℤ}
{t : A ⟶ X}
{i : A ⟶ B}
{p : X ⟶ Y}
{b : B ⟶ Y}
(sq : CategoryTheory.CommSq t i p b)
(hsq : (n : ℤ) → ⋯.LiftStruct)
{Q : CochainComplex C ℤ}
{π : B ⟶ Q}
{hπ : CategoryTheory.CategoryStruct.comp i π = 0}
(hQ : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ π hπ))
{K : CochainComplex C ℤ}
{ι : K ⟶ X}
{hι : CategoryTheory.CategoryStruct.comp ι p = 0}
(hK : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι ι hι))
:
HomComplex.Cochain Q K 1
The 1-cochain from Q to K which refines cocycle₁'.
Instances For
@[simp]
theorem
CochainComplex.Lifting.π_f_cochain₁_v_ι_f
{C : Type u_1}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Abelian C]
{A B X Y : CochainComplex C ℤ}
{t : A ⟶ X}
{i : A ⟶ B}
{p : X ⟶ Y}
{b : B ⟶ Y}
(sq : CategoryTheory.CommSq t i p b)
(hsq : (n : ℤ) → ⋯.LiftStruct)
{Q : CochainComplex C ℤ}
{π : B ⟶ Q}
{hπ : CategoryTheory.CategoryStruct.comp i π = 0}
(hQ : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ π hπ))
{K : CochainComplex C ℤ}
{ι : K ⟶ X}
{hι : CategoryTheory.CategoryStruct.comp ι p = 0}
(hK : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι ι hι))
(n m : ℤ)
(hnm : n + 1 = m)
:
CategoryTheory.CategoryStruct.comp (π.f n)
(CategoryTheory.CategoryStruct.comp ((cochain₁ sq hsq hQ hK).v n m hnm) (ι.f m)) = (↑(cocycle₁' sq hsq)).v n m hnm
@[simp]
theorem
CochainComplex.Lifting.π_f_cochain₁_v_ι_f_assoc
{C : Type u_1}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Abelian C]
{A B X Y : CochainComplex C ℤ}
{t : A ⟶ X}
{i : A ⟶ B}
{p : X ⟶ Y}
{b : B ⟶ Y}
(sq : CategoryTheory.CommSq t i p b)
(hsq : (n : ℤ) → ⋯.LiftStruct)
{Q : CochainComplex C ℤ}
{π : B ⟶ Q}
{hπ : CategoryTheory.CategoryStruct.comp i π = 0}
(hQ : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ π hπ))
{K : CochainComplex C ℤ}
{ι : K ⟶ X}
{hι : CategoryTheory.CategoryStruct.comp ι p = 0}
(hK : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι ι hι))
(n m : ℤ)
(hnm : n + 1 = m)
{Z : C}
(h : X.X m ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (π.f n)
(CategoryTheory.CategoryStruct.comp ((cochain₁ sq hsq hQ hK).v n m hnm)
(CategoryTheory.CategoryStruct.comp (ι.f m) h)) = CategoryTheory.CategoryStruct.comp ((↑(cocycle₁' sq hsq)).v n m hnm) h
noncomputable def
CochainComplex.Lifting.cocycle₁
{C : Type u_1}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Abelian C]
{A B X Y : CochainComplex C ℤ}
{t : A ⟶ X}
{i : A ⟶ B}
{p : X ⟶ Y}
{b : B ⟶ Y}
(sq : CategoryTheory.CommSq t i p b)
(hsq : (n : ℤ) → ⋯.LiftStruct)
{Q : CochainComplex C ℤ}
{π : B ⟶ Q}
{hπ : CategoryTheory.CategoryStruct.comp i π = 0}
(hQ : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ π hπ))
{K : CochainComplex C ℤ}
{ι : K ⟶ X}
{hι : CategoryTheory.CategoryStruct.comp ι p = 0}
(hK : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι ι hι))
:
HomComplex.Cocycle Q K 1
A 1-cocycle from a cokernel Q of i : A ⟶ B to a kernel K of
p : X ⟶ Y. If this is a coboundary, then the square in CochainComplex C ℤ
has a lifting, see the lemma hasLift below.
Instances For
theorem
CochainComplex.Lifting.comp_coe_cocycle₁_comp
{C : Type u_1}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Abelian C]
{A B X Y : CochainComplex C ℤ}
{t : A ⟶ X}
{i : A ⟶ B}
{p : X ⟶ Y}
{b : B ⟶ Y}
(sq : CategoryTheory.CommSq t i p b)
(hsq : (n : ℤ) → ⋯.LiftStruct)
{Q : CochainComplex C ℤ}
{π : B ⟶ Q}
{hπ : CategoryTheory.CategoryStruct.comp i π = 0}
(hQ : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ π hπ))
{K : CochainComplex C ℤ}
{ι : K ⟶ X}
{hι : CategoryTheory.CategoryStruct.comp ι p = 0}
(hK : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι ι hι))
:
(HomComplex.Cochain.ofHom π).comp ((↑(cocycle₁ sq hsq hQ hK)).comp (HomComplex.Cochain.ofHom ι) ⋯) ⋯ = ↑(cocycle₁' sq hsq)
theorem
CochainComplex.Lifting.hasLift
{C : Type u_1}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Abelian C]
{A B X Y : CochainComplex C ℤ}
{t : A ⟶ X}
{i : A ⟶ B}
{p : X ⟶ Y}
{b : B ⟶ Y}
(sq : CategoryTheory.CommSq t i p b)
(hsq : (n : ℤ) → ⋯.LiftStruct)
{Q : CochainComplex C ℤ}
{π : B ⟶ Q}
{hπ : CategoryTheory.CategoryStruct.comp i π = 0}
(hQ : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ π hπ))
{K : CochainComplex C ℤ}
{ι : K ⟶ X}
{hι : CategoryTheory.CategoryStruct.comp ι p = 0}
(hK : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι ι hι))
(α : HomComplex.Cochain Q K 0)
(hα : HomComplex.δ 0 1 α = ↑(cocycle₁ sq hsq hQ hK))
:
sq.HasLift
Consider a commutative square in the category CochainComplex C ℤ
where C is an abelian category.
t
A ⟶ X
i| |p
v v
B ⟶ Y
b
Assume that there exists a degreewise lifting B.X n ⟶ X.X n for any n : ℤ,
that Q is a cokernel of i, and K is a kernel of p.
If the cocycle cocycle₁ sq hsq hQ hK : Cocycle Q K 1 is a coboundary,
we show that the square admits a lifting B ⟶ X.