toSheafify_comp_sheafifyCompIso_inv

English

There is a canonical isomorphism relating the plus-construction on a P with the pullback structure over a refinement of covers.

Русский

Существует каноническое изоморфное соответствие между конструкцией “плюс” над P и структурой вытяжки над уточнением покрытий.

LaTeX

$$$(J. Plus).map\,\text{pullback} \sim \text{mk}$$$

Lean4

@[simp, reassoc]
theorem toSheafify_comp_sheafifyCompIso_inv :
    J.toSheafify _ ≫ (J.sheafifyCompIso F P).inv = whiskerRight (J.toSheafify _) _ := by rw [Iso.comp_inv_eq]; simp

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