Theorems · Inductive type · algebraic geometry

AlgebraicGeometry.Scheme.IdealSheafData

AlgebraicGeometry.Scheme → Type u

A structure that contains the data to uniquely define an ideal sheaf, consisting of 1. an ideal I(U) ≤ Γ(X, U) for every affine open U 2. a proof that I(D(f)) = I(U)_f for every affine open U and every section f : Γ(X, U) 3. a subset of X equal to the support. Also see Scheme.IdealSheafData.mkOfMemSupportIff for a constructor with the condition on the support being (usually) easier to prove.

Defined in

Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Cited by

192 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 2 definitions · uses no axioms