Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjHom.congr_simp

∀ {X : AlgebraicGeometry.Scheme} {I J : X.IdealSheafData} (h : I ≤ J) (U : ↑X.affineOpens),
  AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjHom h U =
    AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjHom h U

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

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites8

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.Scheme.affineOpensstatement and proof · cited by 220
AlgebraicGeometry.Scheme.IdealSheafDatastatement and proof · cited by 192
AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjstatement · cited by 24
AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjHomstatement and proof · cited by 10

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.