Theorems · Inductive type · algebraic geometry
AlgebraicGeometry.IsReduced
AlgebraicGeometry.Scheme → Prop
A scheme X is reduced if all 𝒪ₓ(U) are reduced.
- Defined in
- Mathlib.AlgebraicGeometry.Properties
- Cited by
- 38 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- AlgebraicGeometry.Schemestatement · cited by 2,540
Cited by43
Results whose statement or proof uses this declaration.
- AlgebraicGeometry.isReduced_of_isOpenImmersionstatement and proof · cited by 5
- AlgebraicGeometry.isIntegral_of_irreducibleSpace_of_isReducedstatement and proof · cited by 3
- AlgebraicGeometry.ext_of_isDominant_of_isSeparatedstatement and proof · cited by 3
- AlgebraicGeometry.Scheme.RationalMap.toPartialMapstatement and proof · cited by 3
- AlgebraicGeometry.isIntegral_iff_irreducibleSpace_and_isReducedstatement and proof · cited by 2
- AlgebraicGeometry.Scheme.IdealSheafData.support_eq_top_iffstatement and proof · cited by 2
- AlgebraicGeometry.IsReduced.of_openCoverstatement and proof · cited by 2
- AlgebraicGeometry.GeometricallyReduced.isReduced_of_flat_of_isLocallyNoetherianstatement and proof · cited by 2
- AlgebraicGeometry.Scheme.PartialMap.equiv_iff_of_isSeparated_of_lestatement and proof · cited by 2
- AlgebraicGeometry.basicOpen_eq_bot_iffstatement and proof · cited by 1
- AlgebraicGeometry.isField_stalk_of_closure_mem_irreducibleComponentsstatement and proof · cited by 1
- AlgebraicGeometry.isFinite_iff_locallyOfFiniteType_of_jacobsonSpacestatement and proof · cited by 1