map_glueMorphismsOverOfLocallyDirected_left

English

In an OpenCover for a scheme over S, glue morphisms over locally directed cover are open immersions on left charts.

Русский

В открытом покрытии для схемы над S клеевые морфизмы над локально-направленным покрытием являются открытыми вложениями на левых диаграммах.

LaTeX

$$$\text{glueMorphismsOverOfLocallyDirected}$ has open immersion property on left$$

Lean4

@[reassoc (attr := simp)]
theorem map_glueMorphismsOverOfLocallyDirected_left {S : Scheme.{u}} {X : Over S} (𝒰 : X.left.OpenCover) [Category 𝒰.I₀]
    [𝒰.LocallyDirected] {Y : Over S} (g : ∀ i, 𝒰.X i ⟶ Y.left)
    (h : ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), 𝒰.trans hij ≫ g j = g i) (w : ∀ i, g i ≫ Y.hom = 𝒰.f i ≫ X.hom) (i : 𝒰.I₀) :
    𝒰.f i ≫ (𝒰.glueMorphismsOverOfLocallyDirected g h w).left = g i := by simp [glueMorphismsOverOfLocallyDirected]

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