Theorems · Theorem · algebraic geometry
AlgebraicGeometry.isAffineOpen_opensRange
∀ {X Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine X] (f : X ⟶ Y) [H : AlgebraicGeometry.IsOpenImmersion f],
AlgebraicGeometry.IsAffineOpen (AlgebraicGeometry.Scheme.Hom.opensRange f)- Defined in
- Mathlib.AlgebraicGeometry.AffineScheme
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 144 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Quiver.Homstatement and proof · cited by 32,603
- CategoryTheory.Iso.invproof · cited by 6,514
- AlgebraicGeometry.Schemestatement and proof · cited by 2,540
- AlgebraicGeometry.IsOpenImmersionstatement and proof · cited by 476
- AlgebraicGeometry.IsAffineOpenstatement · cited by 222
- AlgebraicGeometry.IsAffinestatement and proof · cited by 159
- AlgebraicGeometry.Scheme.Hom.opensRangestatement and proof · cited by 113
- Subtype.range_valproof · cited by 41
- AlgebraicGeometry.IsOpenImmersion.isoOfRangeEqproof · cited by 16
- AlgebraicGeometry.IsAffine.of_isIsoproof · cited by 11
- AlgebraicGeometry.Scheme.ofRestrictproof · cited by 9
Cited by13
Results whose statement or proof uses this declaration.
- AlgebraicGeometry.Scheme.isBasis_affineOpensproof · cited by 37
- AlgebraicGeometry.isAffineOpen_topproof · cited by 26
- AlgebraicGeometry.IsAffineOpen.basicOpenproof · cited by 19
- AlgebraicGeometry.HasAffineProperty.of_openCoverproof · cited by 3
- AlgebraicGeometry.isLocallyNoetherian_iff_of_affine_openCoverproof · cited by 2
- AlgebraicGeometry.HasRingHomProperty.of_source_openCoverproof · cited by 2
- AlgebraicGeometry.of_targetAffineLocally_of_isPullbackproof · cited by 2
- AlgebraicGeometry.HasAffineProperty.iff_of_openCoverproof · cited by 1
- AlgebraicGeometry.diagonal_isAffine_iff_forall_isAffineOpen_infproof · cited by 0
- AlgebraicGeometry.exists_isAffineOpen_mem_and_subsetproof · cited by 0
- AlgebraicGeometry.Proj.isAffineOpen_basicOpenproof · cited by 0