sheafHasCoeToFun — Mathlib

English

There is a canonical CoeFun instance from the sheaf's sections to the corresponding functions on opens.

Русский

Существует каноническое отображение типа функций из секций к соответствующим функциям на открытых множествах.

LaTeX

$$StructureGroupoid.LocalInvariantProp.sheafHasCoeToFun hG U : CoeFun ((hG.sheaf M M').val.obj U) (fun _ => ↑(unop U) → M')$$

Lean4

instance sheafHasCoeToFun (hG : LocalInvariantProp G G' P) (U : (Opens (TopCat.of M))ᵒᵖ) :
    CoeFun ((hG.sheaf M M').val.obj U) fun _ => ↑(unop U) → M' where coe a := a.1

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