Theorems · Definition · algebraic geometry
AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjHom
{X : AlgebraicGeometry.Scheme} →
{I J : X.IdealSheafData} → I ≤ J → (U : ↑X.affineOpens) → J.glueDataObj U ⟶ I.glueDataObj UGiven I ≤ J, this is the map Spec(Γ(X, U)/J(U)) ⟶ Spec(Γ(X, U)/I(U)).
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 161 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Quiver.Homstatement · cited by 32,603
- Set.Elemstatement and proof · cited by 7,166
- AlgebraicGeometry.Schemestatement and proof · cited by 2,540
- AlgebraicGeometry.Scheme.Opensstatement · cited by 1,149
- AlgebraicGeometry.Spec.mapproof · cited by 332
- CommRingCat.ofHomproof · cited by 259
- AlgebraicGeometry.Scheme.affineOpensstatement and proof · cited by 220
- AlgebraicGeometry.Scheme.IdealSheafDatastatement and proof · cited by 192
- Ideal.Quotient.factorproof · cited by 33
- AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjstatement · cited by 24
Cited by11
Results whose statement or proof uses this declaration.
- AlgebraicGeometry.Scheme.IdealSheafData.inclusionproof · cited by 12
- AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjHom_ιstatement · cited by 3
- AlgebraicGeometry.Scheme.IdealSheafData.subSchemeCover_map_inclusionstatement and proof · cited by 3
- AlgebraicGeometry.Scheme.IdealSheafData.inclusion_subschemeιproof · cited by 3
- AlgebraicGeometry.Scheme.IdealSheafData.subSchemeCover_map_inclusion_assocstatement and proof · cited by 2
- AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjHom_compstatement and proof · cited by 1
- AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjHom_comp_assocstatement and proof · cited by 1
- AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjHom_idstatement · cited by 1
- AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjHom_ι_assocstatement and proof · cited by 1
- AlgebraicGeometry.Scheme.IdealSheafData.inclusion_compproof · cited by 1
- AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjHom.congr_simpstatement and proof · cited by 0