English
The carrier ideal produced in FromSpec is prime when f is homogeneous and the relevant disjointness condition holds.
Русский
Идеал carrier, полученный через FromSpec, прост, если f однороден и соблюдается требование о disjointness.
LaTeX
$$$\text{carrier is prime}$$$
Lean4
/-- Pretty printer defined by `notation3` command. -/
@[local delab✝ app.HomogeneousLocalization.Away]
public meta def
«_aux_Mathlib_AlgebraicGeometry_ProjectiveSpectrum_Scheme___delab_app__private_Mathlib_AlgebraicGeometry_ProjectiveSpectrum_Scheme_0_AlgebraicGeometry_termA⁰___1» :
Delab✝ :=
whenPPOption✝ getPPNotation✝ <|
whenNotPPOption✝ getPPExplicit✝ <|
withOverApp✝ 8
(getExpr✝ >>= fun e✝ =>
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `HomogeneousLocalization.Away))
(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✝¹))))
(matchVar✝ `f) >=>
pure✝)
MatchState.empty✝ >>=
fun s✝ => MatchState.delabVar✝ s✝ `f (some✝ e✝) >>= fun f => withHeadRefIfTagAppFns✝ `(A⁰_ $f))
