isoRestrict_hom_ofRestrict — Mathlib

English

For an open immersion f, the morphism restriction interacts with Y.ofRestrict so that the restricting isomorphism aligns with the restricted target map.

Русский

Для открытого вложения f отображение ограничения согласуется с Y.ofRestrict так, что ограничивающий изоморфизм совпадает с целевым отображением ограниченного объекта.

LaTeX

$$Eq ((categoryOfPresheafedSpaces C).comp (IsOpenImmersion.isoRestrict f).hom (Y.ofRestrict ⋯)) f$$

Lean4

@[reassoc (attr := simp)]
theorem isoRestrict_hom_ofRestrict : (isoRestrict f).hom ≫ Y.ofRestrict _ = f := by
  -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11041): `ext` did not pick up `NatTrans.ext`

  refine PresheafedSpace.Hom.ext _ _ rfl <| NatTrans.ext <| funext fun x => ?_
  simp only [eqToHom_refl, Functor.whiskerRight_id']
  erw [Category.comp_id, comp_c_app, f.c.naturality_assoc, ← X.presheaf.map_comp]
  trans f.c.app x ≫ X.presheaf.map (𝟙 _)
  · congr 1
  · simp

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