homOfLE_tAux — Mathlib

English

A formula expressing how homOfLE interacts with tAux in the locally directed setting.

Русский

Формула взаимодействия homOfLE и tAux в локально направленной конфигурации.

LaTeX

$$$$ (F.obj i).homOfLE (\ldots) \;\gg\; tAux F i j = (F.map fi).isoOpensRange.inv \gg F.map fj $$$$

Lean4

@[reassoc]
theorem homOfLE_tAux (i j : J) {k : J} (fi : k ⟶ i) (fj : k ⟶ j) :
    (F.obj i).homOfLE (le_iSup_of_le ⟨k, fi, fj⟩ le_rfl) ≫ tAux F i j = (F.map fi).isoOpensRange.inv ≫ F.map fj :=
  (Scheme.Opens.iSupOpenCover (J := Σ k, (k ⟶ i) × (k ⟶ j)) _).ι_glueMorphisms _ _ ⟨k, fi, fj⟩

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