inclusion_comp — Mathlib

English

The functor from ideal sheaf data to the associated subscheme object in over Y.

Русский

Функтор от данных идеала к соответствующему объекту подсхемы в Over Y.

LaTeX

$$$\text{subschemeFunctor}(Y): (I.Y)^{op} \to \mathbf{Over}~Y$$$

Lean4

@[reassoc (attr := simp)]
theorem inclusion_comp {I J K : IdealSheafData X} (h₁ : I ≤ J) (h₂ : J ≤ K) :
    inclusion h₂ ≫ inclusion h₁ = inclusion (h₁.trans h₂) :=
  K.subschemeCover.openCover.hom_ext _ _ fun _ ↦ by simp

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