English
The singleFunctor is full: every morphism in the target is the image of a morphism from the source.
Русский
Функтор singleFunctor полон: каждый образованный морфизм есть прообраз целевого морфизма.
LaTeX
$$full((singleFunctor C n))$$
Lean4
instance (n : ℤ) : (singleFunctor C n).Full where
map_surjective {A B}
f :=
by
change Q.obj ((CochainComplex.singleFunctor C n).obj A) ⟶ Q.obj ((CochainComplex.singleFunctor C n).obj B) at f
suffices ∃ f', f = Q.map f' by
obtain ⟨f', rfl⟩ := this
obtain ⟨g, rfl⟩ := (CochainComplex.singleFunctor C n).map_surjective f'
exact ⟨g, rfl⟩
obtain ⟨X, _, _, s, _, g, rfl⟩ := right_fac_of_isStrictlyLE_of_isStrictlyGE n n f
obtain ⟨A₀, ⟨e⟩⟩ := X.exists_iso_single n
have ⟨φ, hφ⟩ := (CochainComplex.singleFunctor C n).map_surjective (e.inv ≫ s)
have : IsIso ((singleFunctor C n).map φ) :=
by
change IsIso (Q.map ((CochainComplex.singleFunctor C n).map φ))
rw [hφ, Functor.map_comp]
infer_instance
have : IsIso φ := (NatIso.isIso_map_iff (singleFunctorCompHomologyFunctorIso C n) φ).1 (by dsimp; infer_instance)
have : IsIso (e.inv ≫ s) := by rw [← hφ]; infer_instance
have : IsIso s := IsIso.of_isIso_comp_left e.inv s
exact ⟨inv s ≫ g, by simp⟩
