English
Let F,G : (Nat)ᵒᵖ ⥤ C be functors and let app_n: F.obj ⟨n⟩ ⟶ G.obj ⟨n⟩ for every n ∈ ℕ, satisfying F.map (homOfLE (n.le_add_right 1)).op ≫ app_n = app_(n+1) ≫ G.map (homOfLE (n.le_add_right 1)).op for all n. Then there exists a natural transformation η : F ⟶ G whose components satisfy η.app n = app_n for all n.
Русский
Пусть F,G : (Nat)ᵒᵖ ⥤ C — уравнения последовательности натуральных отображений. Для каждого n существует морфизм app_n : F.obj ⟨n⟩ ⟶ G.obj ⟨n⟩, удовлетворяющее условиям натурализованности для морфизмов вида n ⟶ n+1: F.map (homOfLE (n.le_add_right 1)).op ≫ app_n = app_(n+1) ≫ G.map (homOfLE (n.le_add_right 1)).op. Тогда существует естественное преобразование η : F ⟶ G, которое на каждом n имеет компоненту app_n.
LaTeX
$$$\\exists \\eta : F ⟶ G, \\forall n, \\eta.naturality.app n = app n$$$
Lean4
/-- Constructor for natural transformations `F ⟶ G` in `ℕᵒᵖ ⥤ C` which takes as inputs
the morphisms `F.obj ⟨n⟩ ⟶ G.obj ⟨n⟩` for all `n : ℕ` and the naturality condition only
for morphisms of the form `n ⟶ n + 1`. -/
@[simps!]
def ofOpSequence : F ⟶ G where
app n := app n.unop
naturality _ _
f :=
by
let φ : G.rightOp ⟶ F.rightOp := ofSequence (fun n ↦ (app n).op) (fun n ↦ Quiver.Hom.unop_inj (naturality n).symm)
exact Quiver.Hom.op_inj (φ.naturality f.unop).symm
