English
Construct a natural transformation between functors F,G: Nat ⥤ C using a family of components app n: F.obj n ⟶ G.obj n that satisfy a naturality condition for consecutive indices.
Русский
Построить нативное преобразование между функторaми F,G: Nat ⥤ C, используя семейство компонент app n: F.obj n ⟶ G.obj n и условие натурализности для последовательных индексов.
LaTeX
$$$\\text{ofSequence} : F ⟶ G\\ \\text{with } app: \\forall n, F.obj n ⟶ G.obj n \\text{ and } \\text{naturality}: ...$$$
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 app]
def ofSequence : F ⟶ G where
app := app
naturality := by
intro i j φ
obtain ⟨k, hk⟩ := Nat.exists_eq_add_of_le (leOfHom φ)
obtain rfl := Subsingleton.elim φ (homOfLE (by omega))
revert i j
induction k with
| zero =>
intro i j hk
obtain rfl : j = i := by omega
simp
| succ k hk =>
intro i j hk'
obtain rfl : j = i + k + 1 := by omega
simp only [← homOfLE_comp (show i ≤ i + k by omega) (show i + k ≤ i + k + 1 by omega), Functor.map_comp, assoc,
naturality, reassoc_of% (hk rfl)]
