inv_naturality — Mathlib

English

A general categorical identity about associativity of composition in a functor.

Русский

Общее категориальное тождество об ассоциации композиции в функторе.

LaTeX

$$Eq (inst.comp (X.presheaf.map f) (X.presheaf.map g)) (X.presheaf.map (f ≫ g))$$

Lean4

@[simp, reassoc]
theorem inv_naturality {U V : (Opens X)ᵒᵖ} (i : U ⟶ V) :
    X.presheaf.map i ≫ H.invApp _ (unop V) = invApp f (unop U) ≫ Y.presheaf.map (opensFunctor f |>.op.map i) :=
  by
  simp only [invApp, ← Category.assoc]
  rw [IsIso.comp_inv_eq]
  simp only [Functor.op_obj, op_unop, ← X.presheaf.map_comp, Functor.op_map, Category.assoc, NatTrans.naturality,
    Quiver.Hom.unop_op, IsIso.inv_hom_id_assoc, TopCat.Presheaf.pushforward_obj_map]
  congr 1

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