glueDataObjHom — Mathlib

English

Given I ≤ J, glueDataObjHom h U is the map J.glueDataObjU → I.glueDataObjU induced by quotienting.

Русский

При заданном I ≤ J отображение glueDataObjHom h U индуцировано факторизацией: J.glueDataObjU → I.glueDataObjU.

LaTeX

$$$\text{glueDataObjHom}(h,U) : J.glueDataObj U \to I.glueDataObj U$$$

Lean4

/-- Given `I ≤ J`, this is the map `Spec(Γ(X, U)/J(U)) ⟶ Spec(Γ(X, U)/I(U))`. -/
noncomputable def glueDataObjHom {I J : IdealSheafData X} (h : I ≤ J) (U) : J.glueDataObj U ⟶ I.glueDataObj U :=
  Spec.map (CommRingCat.ofHom (Ideal.Quotient.factor (h U)))

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