res_π — Mathlib

English

The ith component of res composed with the projection to F(U_i) equals the restriction map along U_i ≤ supr(U).

Русский

i-й компонент композиции res с проекцией равен ограничению по U_i ≤ объединению U.

LaTeX

$$$\mathrm{res}\;\;\;_{i} \; ≡ \; F(\mathrm{leSupr}(U,i)).op$$$

Lean4

@[simp, elementwise]
theorem res_π (i : ι) : res F U ≫ limit.π _ ⟨i⟩ = F.map (Opens.leSupr U i).op := by rw [res, limit.lift_π, Fan.mk_π_app]

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