instIsGEObjSingleFunctor — Mathlib

English

For any object X in C and any integer n, the object ((singleFunctor C n).obj X) is GE in degree n.

Русский

Для любого объекта X в C и любого целого числа n объект ((singleFunctor C n).obj X) является GE в степени n.

LaTeX

$$$\forall X \in C,\; \forall n \in \mathbb{Z},\; ((\text{singleFunctor } C n).obj X).IsGE n$$$

Lean4

instance (X : C) (n : ℤ) : ((singleFunctor C n).obj X).IsGE n :=
  by
  let e := (singleFunctorIsoCompQ C n).app X
  dsimp only [Functor.comp_obj] at e
  exact TStructure.t.isGE_of_iso e.symm n

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