English
Given bicomplexes K and L, a graded-object morphism f: K.toGradedObject ⟶ L.toGradedObject together with horizontal and vertical compatibility data yields a morphism K ⟶ L in the bicomplex category.
Русский
Дано биокомплексах K, L и морфизм градуированного объекта f: K.toGradedObject ⟶ L.toGradedObject вместе с данными совместимости по горизонтальным и вертикальным дифференциалам, получаем морфизм K ⟶ L в категории биокомплексoв.
LaTeX
$$$\mathrm{homMk}(f,\text{comm}_1,\text{comm}_2): K \to L$ при условии, что \\ c_1.Rel(i_1,i_1') \Rightarrow f_{i_1,i_2} \circ (L.d i_1 i_1').f i_2 = (K.d i_1 i_1').f i_2 \circ f_{i_1',i_2}$ и аналогично для вертикального дифференциала.$$
Lean4
/-- Constructor for a morphism `K ⟶ L` in the category `HomologicalComplex₂ C c₁ c₂` which
takes as inputs a morphism `f : K.toGradedObject ⟶ L.toGradedObject` and
the compatibilites with both horizontal and vertical differentials. -/
@[simps!]
def homMk {K L : HomologicalComplex₂ C c₁ c₂} (f : K.toGradedObject ⟶ L.toGradedObject)
(comm₁ : ∀ i₁ i₁' i₂, c₁.Rel i₁ i₁' → f ⟨i₁, i₂⟩ ≫ (L.d i₁ i₁').f i₂ = (K.d i₁ i₁').f i₂ ≫ f ⟨i₁', i₂⟩)
(comm₂ : ∀ i₁ i₂ i₂', c₂.Rel i₂ i₂' → f ⟨i₁, i₂⟩ ≫ (L.X i₁).d i₂ i₂' = (K.X i₁).d i₂ i₂' ≫ f ⟨i₁, i₂'⟩) : K ⟶ L
where
f
i₁ :=
{ f := fun i₂ => f ⟨i₁, i₂⟩
comm' := comm₂ i₁ }
comm' i₁ i₁'
h₁ := by
ext i₂
exact comm₁ i₁ i₁' i₂ h₁
