shiftFunctor_comp_inverts — Mathlib

English

If W is a compatible morphism property relative to shift, then for any a in A, the functor shiftFunctor C a composed with L inverts W-morphisms, i.e., becomes inverted by localization.

Русский

Если свойство морфизмов W совместимо со сдвигом, то при любом a∈A композиция shiftFunctor C a с локализацией L разворачивает W-морфизмы.

LaTeX

$$$ W.IsInvertedBy (shiftFunctor C a \;\gg\; L) $$$

Lean4

theorem shiftFunctor_comp_inverts (a : A) : W.IsInvertedBy (shiftFunctor C a ⋙ L) := fun _ _ f hf =>
  Localization.inverts L W _ (by simpa only [iff] using hf)

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