inverts — Mathlib

English

For a localizer morphism Φ: W1 → W2, the composed functor Φ.functor ⋅ L2 inverts W1-morphisms after localization.

Русский

Для локализующего морфизмa Φ: W1 → W2 композиция Φ.functor ⋅ L2 обращает W1-морфизмы после локализации.

LaTeX

$$$W_1.IsInvertedBy(Φ.functor\,⋅\,L_2)$$$

Lean4

theorem inverts : W₁.IsInvertedBy (Φ.functor ⋙ L₂) := fun _ _ _ hf => Localization.inverts L₂ W₂ _ (Φ.map _ hf)

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