stableUnderInverse — Mathlib

English

Let F1, F2: C → D be functors and let a family of arrows app_X: F1 X → F2 X define a naturality data. Then the naturality condition is preserved under taking inverses of the component arrows, provided each component is invertible.

Русский

Пусть F1, F2: C → D — функторы, задано семейство отображений app_X: F1 X → F2 X, удовлетворяющее условию естественности. Тогда свойство естественности сохраняется при замене компонент на их обратные, если каждый app_X обратим.

LaTeX

$$$\\mathrm{StableUnderInverse}(\\mathrm{naturalityProperty}(app))$$$

Lean4

theorem stableUnderInverse {F₁ F₂ : C ⥤ D} (app : ∀ X, F₁.obj X ⟶ F₂.obj X) :
    (naturalityProperty app).StableUnderInverse := fun X Y e he =>
  by
  simp only [naturalityProperty] at he ⊢
  rw [← cancel_epi (F₁.map e.hom)]
  slice_rhs 1 2 => rw [he]
  simp only [Category.assoc, ← F₁.map_comp_assoc, ← F₂.map_comp, e.hom_inv_id, Functor.map_id, Category.id_comp,
    Category.comp_id]

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