subsingleton_hom_of_isStrictlyLE_of_isStrictlyGE

English

If a < b and X is strictly LE a while Y is strictly GE b, then there is at most one morphism from Q.obj X to Q.obj Y.

Русский

При a < b и X с строгим LE a, Y с строгим GE b, множество морфизмов из Q.obj X в Q.obj Y пусто или состоит из одного элемента.

LaTeX

$$Subsingleton (Q.obj X ⟶ Q.obj Y)$$

Lean4

theorem subsingleton_hom_of_isStrictlyLE_of_isStrictlyGE (X Y : CochainComplex C ℤ) (a b : ℤ) (h : a < b)
    [X.IsStrictlyLE a] [Y.IsStrictlyGE b] : Subsingleton (Q.obj X ⟶ Q.obj Y) :=
  by
  suffices ∀ (f : Q.obj X ⟶ Q.obj Y), f = 0 from ⟨by simp [this]⟩
  intro f
  obtain ⟨X', _, s, _, g, rfl⟩ := right_fac_of_isStrictlyLE f a
  have : g = 0 := by
    ext i
    by_cases hi : a < i
    · apply (X'.isZero_of_isStrictlyLE a i hi).eq_of_src
    · apply (Y.isZero_of_isStrictlyGE b i (by cutsat)).eq_of_tgt
  rw [this, Q.map_zero, comp_zero]

Похожие утверждения