map_glueMorphismsOfLocallyDirected

English

The glue morphism with LocallyDirected structure coincides with the left component map for any i.

Русский

Клеевой морфизм для локально-направленного строения совпадает с левым компонентным отображением для любого i.

LaTeX

$$$\mathcal{U}.f i \; \circ \text{glueMorphismsOfLocallyDirected}(i) = g_i$$$

Lean4

@[reassoc (attr := simp)]
theorem map_glueMorphismsOfLocallyDirected {Y : Scheme.{u}} (g : ∀ i, 𝒰.X i ⟶ Y)
    (h : ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), 𝒰.trans hij ≫ g j = g i) (i : 𝒰.I₀) :
    𝒰.f i ≫ 𝒰.glueMorphismsOfLocallyDirected g h = g i := by simp [glueMorphismsOfLocallyDirected]

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