toSheafify_app_apply' — Mathlib

English

A simp-normal form of toSheafify application on X and x.

Русский

Симп-нормальная форма применения toSheafify на X и x.

LaTeX

$$$(toSheafify(\alpha, \varphi)).app X .hom x = \varphi_{X}(x).$$$

Lean4

/-- `@[simp]`-normal form of `toSheafify_app_apply`. -/
@[simp]
theorem toSheafify_app_apply' (X : Cᵒᵖ) (x : M₀.obj X) :
    DFunLike.coe (F := (_ →ₗ[_] ↑((ModuleCat.restrictScalars (α.app X).hom).obj _))) ((toSheafify α φ).app X).hom x =
      φ.app X x :=
  rfl

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