Mathlib Map

Theorems · Inductive type · algebraic geometry

AlgebraicGeometry.IsAffine

AlgebraicGeometry.Scheme → Prop

A Scheme is affine if the canonical map X ⟶ Spec Γ(X) is an isomorphism.

Defined in
Mathlib.AlgebraicGeometry.AffineScheme
Cited by
159 results in Mathlib
Foundations
Depth 1 from the axioms, rests on 2 definitions · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

AlgebraicGeometry.IsAffineOpen · cited by 222AlgebraicGeometry.IsAffin…AlgebraicGeometry.Scheme.isoSpec · cited by 56Scheme.isoSpecAlgebraicGeometry.AffineTargetMorphismProperty · cited by 31AlgebraicGeometry.AffineT…AlgebraicGeometry.isAffineOpen_top · cited by 26AlgebraicGeometry.isAffin…AlgebraicGeometry.HasAffineProperty.iff_of_isAffine · cited by 21HasAffineProperty.iff_of_…AlgebraicGeometry.affineAnd · cited by 21AlgebraicGeometry.affineA…AlgebraicGeometry.isAffineOpen_opensRange · cited by 13AlgebraicGeometry.isAffin…AlgebraicGeometry.IsAffine.of_isIso · cited by 11IsAffine.of_isIsoAlgebraicGeometry.AffineSpace.isoOfIsAffine · cited by 10AffineSpace.isoOfIsAffineAlgebraicGeometry.AffineTargetMorphismProperty.toProperty · cited by 9AffineTargetMorphismPrope…AlgebraicGeometry.HasRingHomProperty.iff_of_isAffine · cited by 9HasRingHomProperty.iff_of…AlgebraicGeometry.isAffine_of_isAffineHom · cited by 9AlgebraicGeometry.isAffin…AlgebraicGeometry.AffineTargetMorphismProperty.cancel_left_of_respectsIso · cited by 8AffineTargetMorphismPrope…AlgebraicGeometry.IsAffineOpen.SpecMap_appLE_fromSpec · cited by 8IsAffineOpen.SpecMap_appL…AlgebraicGeometry.AffineTargetMorphismProperty.diagonal · cited by 7AffineTargetMorphismPrope…AlgebraicGeometry.Scheme · cited by 2540AlgebraicGeometry.SchemeAlgebraicGeometry.IsAffineCITED BYCITES

Cites1

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

Cited by183

Results whose statement or proof uses this declaration.