English
There is a natural identification between the stalks of the structure sheaf on Proj and the corresponding Spec after pushing forward along the relevant maps, providing a concrete description of stalk maps via isomorphisms.
Русский
Существует естественное соответствие между stalk-обобщениями структурной оболочки на Proj и соответствующим Spec после переноса по соответствующим отображениям, предоставляющее конкретное описание stalkMap через изоморфизмы.
LaTeX
$$$$\text{toStalk\_stalkMap\_toSpec: }\text{Stalk}_{Proj}\;\to\;\text{Stalk}_{Spec}$$$$
Lean4
/-- Pretty printer defined by `notation3` command. -/
@[local delab✝ app.HomogeneousLocalization.AtPrime]
public meta def
_aux_Mathlib_AlgebraicGeometry_ProjectiveSpectrum_StructureSheaf___delab_app__private_Mathlib_AlgebraicGeometry_ProjectiveSpectrum_StructureSheaf_0_AlgebraicGeometry_termAt__1 :
Delab✝ :=
whenPPOption✝ getPPNotation✝ <|
whenNotPPOption✝ getPPExplicit✝ <|
withOverApp✝ 9
(getExpr✝ >>= fun e✝ =>
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `HomogeneousLocalization.AtPrime))
(matchExpr✝ (Expr.isConstOf✝ · `Nat)))
(matchFVar✝ `R (matchExpr✝ isType'✝)))
(matchFVar✝ `A (matchExpr✝ isType'✝)))
pure✝)
pure✝)
pure✝)
(matchFVar✝ `𝒜
(matchForall✝ (matchExpr✝ (Expr.isConstOf✝ · `Nat))
(fun n✝ =>
matchApp✝¹
(matchApp✝¹
(matchApp✝¹
(matchApp✝¹
(matchApp✝¹ (matchExpr✝¹ (Expr.isConstOf✝¹ · `Submodule))
(matchFVar✝¹ `R (matchExpr✝¹ isType'✝¹)))
(matchFVar✝¹ `A (matchExpr✝¹ isType'✝¹)))
pure✝¹)
pure✝¹)
pure✝¹))))
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `HomogeneousIdeal.toIdeal))
(matchExpr✝ (Expr.isConstOf✝ · `Nat)))
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝ (matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Submodule)) pure✝)
(matchFVar✝ `A (matchExpr✝ isType'✝)))
pure✝)
pure✝)
pure✝))
(matchFVar✝ `A (matchExpr✝ isType'✝)))
pure✝)
pure✝)
pure✝)
pure✝)
pure✝)
pure✝)
pure✝)
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `ProjectiveSpectrum.asHomogeneousIdeal))
pure✝)
(matchFVar✝ `A (matchExpr✝ isType'✝)))
pure✝)
pure✝)
pure✝)
pure✝)
pure✝)
(matchVar✝ `x))))
pure✝ >=>
pure✝)
MatchState.empty✝ >>=
fun s✝ => MatchState.delabVar✝ s✝ `x (some✝ e✝) >>= fun x => withHeadRefIfTagAppFns✝ `(at $x))
