hasMap_of_iso — Mathlib

English

If X and Y are isomorphic graded objects and p: I → J, then HasMap p holds for Y whenever it holds for X; i.e., isomorphisms preserve the existence of maps with respect to p.

Русский

Если X и Y — изоморфны как градуированные объекты, и p: I → J, то существование HasMap p для X имплицирует HasMap p для Y; изоморфизм сохраняет существование отображений по p.

LaTeX

$$$ X.HasMap p \Rightarrow Y.HasMap p $$$

Lean4

theorem hasMap_of_iso (e : X ≅ Y) (p : I → J) [HasMap X p] : HasMap Y p := fun j =>
  by
  have α : Discrete.functor (X.mapObjFun p j) ≅ Discrete.functor (Y.mapObjFun p j) :=
    Discrete.natIso (fun ⟨i, _⟩ => (GradedObject.eval i).mapIso e)
  exact hasColimit_of_iso α.symm

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