resLE_preimage — Mathlib

English

Composition of successive restriction maps is compatible with the restriction to the composed morphism: the associativity of resLE with respect to the outer morphisms holds.

Русский

Сочетание последовательных ограничений совместимо с ограничением по композиции морфизмов: ассоциативность ограничений сохраняется при композице внешних морфизмов.

LaTeX

$$$f.resLE U V e \;\gg\; g.resLE W U e' = (f\,\gg\, g).resLE W V (e\.trans (\mathrm{Hom}(...).le))$$$

Lean4

theorem resLE_preimage (f : X ⟶ Y) {U : Y.Opens} {V : X.Opens} (e : V ≤ f ⁻¹ᵁ U) (O : U.toScheme.Opens) :
    f.resLE U V e ⁻¹ᵁ O = V.ι ⁻¹ᵁ (f ⁻¹ᵁ U.ι ''ᵁ O) := by
  rw [← preimage_comp, ← resLE_comp_ι f e, preimage_comp, preimage_image_eq]

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