Mathlib Map

Theorems · Definition · algebraic geometry

AlgebraicGeometry.Scheme.IdealSheafData.glueDataObj

{X : AlgebraicGeometry.Scheme} → X.IdealSheafData → ↑X.affineOpens → AlgebraicGeometry.Scheme

Spec (𝒪ₓ(U)/I(U)), the object to be glued into the closed subscheme.

Defined in
Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Cited by
24 results in Mathlib
Foundations
Depth 140 from the axioms · uses propext, Classical.choice, Quot.sound

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjι · cited by 20IdealSheafData.glueDataOb…AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjHom · cited by 10IdealSheafData.glueDataOb…AlgebraicGeometry.Scheme.IdealSheafData.glueData · cited by 8IdealSheafData.glueDataAlgebraicGeometry.Scheme.IdealSheafData.glueDataObjMap · cited by 5IdealSheafData.glueDataOb…AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjHom_ι · cited by 3IdealSheafData.glueDataOb…AlgebraicGeometry.Scheme.IdealSheafData.subSchemeCover_map_inclusion · cited by 3IdealSheafData.subSchemeC…AlgebraicGeometry.Scheme.IdealSheafData.subschemeCover_map_subschemeι · cited by 3IdealSheafData.subschemeC…AlgebraicGeometry.Scheme.IdealSheafData.subSchemeCover_map_inclusion_assoc · cited by 2IdealSheafData.subSchemeC…AlgebraicGeometry.Scheme.IdealSheafData.glueDataT'Aux · cited by 2IdealSheafData.glueDataT'…AlgebraicGeometry.Scheme.IdealSheafData.opensRange_glueDataObjMap · cited by 1IdealSheafData.opensRange…AlgebraicGeometry.Scheme.IdealSheafData.range_glueDataObjι · cited by 1IdealSheafData.range_glue…AlgebraicGeometry.Scheme.IdealSheafData.range_glueDataObjι_ι · cited by 1IdealSheafData.range_glue…AlgebraicGeometry.Scheme.IdealSheafData.range_glueDataObjι_ι_eq_support_inter · cited by 1IdealSheafData.range_glue…AlgebraicGeometry.Scheme.IdealSheafData.ker_glueDataObjι_appTop · cited by 1IdealSheafData.ker_glueDa…AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjHom_comp · cited by 1IdealSheafData.glueDataOb…CategoryTheory.Functor.obj · cited by 19642Functor.objSet.Elem · cited by 7166Set.ElemAlgebraicGeometry.Scheme · cited by 2540AlgebraicGeometry.SchemeHasQuotient.Quotient · cited by 2301HasQuotient.QuotientAlgebraicGeometry.SheafedSpace.toPresheafedSpace · cited by 1988SheafedSpace.toPresheafed…AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace · cited by 1892LocallyRingedSpace.toShea…AlgebraicGeometry.Scheme.toLocallyRingedSpace · cited by 1734Scheme.toLocallyRingedSpa…AlgebraicGeometry.Scheme.Opens · cited by 1149Scheme.OpensAlgebraicGeometry.PresheafedSpace.presheaf · cited by 1104PresheafedSpace.presheafCommRingCat.carrier · cited by 1096CommRingCat.carrierAlgebraicGeometry.Spec · cited by 626AlgebraicGeometry.SpecAlgebraicGeometry.Scheme.affineOpens · cited by 220Scheme.affineOpensAlgebraicGeometry.Scheme.IdealSheafData · cited by 192Scheme.IdealSheafDataAlgebraicGeometry.Scheme.IdealSheafData.ideal · cited by 88IdealSheafData.idealIdealSheafData.glueDataObjCITED BYCITES

Cites14

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by30

Results whose statement or proof uses this declaration.