Theorems · Theorem · algebraic geometry
AlgebraicGeometry.isIso_iff_isOpenImmersion_and_surjective
∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
CategoryTheory.IsIso f ↔ AlgebraicGeometry.IsOpenImmersion f ∧ AlgebraicGeometry.Surjective f- Cited by
- 2 results in Mathlib
- Foundations
- Depth 106 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
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
- AlgebraicGeometry.Schemestatement and proof · cited by 2,540
- CategoryTheory.IsIsostatement and proof · cited by 1,156
- AlgebraicGeometry.PresheafedSpace.Hom.baseproof · cited by 1,135
- AlgebraicGeometry.LocallyRingedSpace.Hom.toHomproof · cited by 995
- AlgebraicGeometry.Scheme.Hom.toLRSHom'proof · cited by 895
- CategoryTheory.Epiproof · cited by 688
- AlgebraicGeometry.IsOpenImmersionstatement and proof · cited by 476
- AlgebraicGeometry.Surjectivestatement · cited by 48
- TopCat.epi_iff_surjectiveproof · cited by 11
- AlgebraicGeometry.surjective_iffproof · cited by 6
- AlgebraicGeometry.isIso_iff_isOpenImmersion_and_epi_baseproof · cited by 3
Cited by2
Results whose statement or proof uses this declaration.
- AlgebraicGeometry.IsFinite.of_isProper_of_locallyQuasiFiniteproof · cited by 2
- AlgebraicGeometry.isomorphisms_eq_isOpenImmersion_inf_surjectiveproof · cited by 1