Theorems · Theorem · algebraic geometry
AlgebraicGeometry.Spec.map_inj
∀ {R S : CommRingCat} {φ ψ : R ⟶ S}, AlgebraicGeometry.Spec.map φ = AlgebraicGeometry.Spec.map ψ ↔ φ = ψ- Cited by
- 3 results in Mathlib
- Foundations
- Depth 141 from the axioms · uses propext, Classical.choice, Quot.sound
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 and proof · cited by 32,603
- AlgebraicGeometry.Schemestatement · cited by 2,540
- CommRingCatstatement and proof · cited by 2,333
- AlgebraicGeometry.Specstatement · cited by 626
- AlgebraicGeometry.Spec.mapstatement and proof · cited by 332
- CategoryTheory.Functor.map_injectiveproof · cited by 91
- AlgebraicGeometry.Scheme.Specproof · cited by 57
- Quiver.Hom.op_injproof · cited by 45
Cited by3
Results whose statement or proof uses this declaration.
- AlgebraicGeometry.Spec.map_injectiveproof · cited by 9
- AlgebraicGeometry.FormallyUnramified.of_hom_extproof · cited by 0