homMk — Mathlib

English

There is a construction that, given a family of component morphisms app, returns a morphism in the category of ComposableArrows with the required naturality condition.

Русский

Существует конструктор, который по заданной семье компонент app порождает морфизм в категории ComposableArrows с требуемой натуральностью.

LaTeX

$$$\text{homMk} : (\forall i, F.obj i \to G.obj i) \to (\forall i \ (hi

Lean4

/-- Constructor for morphisms `F ⟶ G` in `ComposableArrows C n` which takes as inputs
a family of morphisms `F.obj i ⟶ G.obj i` and the naturality condition only for the
maps in `Fin (n + 1)` given by inequalities of the form `i ≤ i + 1`. -/
@[simps]
def homMk {F G : ComposableArrows C n} (app : ∀ i, F.obj i ⟶ G.obj i)
    (w : ∀ (i : ℕ) (hi : i < n), F.map' i (i + 1) ≫ app _ = app _ ≫ G.map' i (i + 1)) : F ⟶ G
    where
  app := app
  naturality :=
    by
    suffices ∀ (k i j : ℕ) (hj : i + k = j) (hj' : j ≤ n), F.map' i j ≫ app _ = app _ ≫ G.map' i j
      by
      rintro ⟨i, hi⟩ ⟨j, hj⟩ hij
      have hij' := leOfHom hij
      simp only [Fin.mk_le_mk] at hij'
      obtain ⟨k, hk⟩ := Nat.le.dest hij'
      exact this k i j hk (by valid)
    intro k
    induction k with intro i j hj hj'
    | zero =>
      simp only [add_zero] at hj
      obtain rfl := hj
      rw [F.map'_self i, G.map'_self i, id_comp, comp_id]
    | succ k hk =>
      rw [← add_assoc] at hj
      subst hj
      rw [F.map'_comp i (i + k) (i + k + 1), G.map'_comp i (i + k) (i + k + 1), assoc, w (i + k) (by valid),
        reassoc_of% (hk i (i + k) rfl (by valid))]

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