Theorems · Theorem · algebraic geometry
AlgebraicGeometry.IsLocalIso.eq_iInf
@AlgebraicGeometry.IsLocalIso = ⨅ P, ⨅ (_ : P.ContainsIdentities), ⨅ (_ : AlgebraicGeometry.IsZariskiLocalAtSource P), P
IsLocalIso is the weakest source-Zariski-local property containing identities.
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 172 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 · cited by 32,603
- AlgebraicGeometry.Schemestatement and proof · cited by 2,540
- CategoryTheory.MorphismPropertystatement and proof · cited by 2,179
- le_antisymmproof · cited by 2,068
- iInfstatement · cited by 1,690
- iInf_leproof · cited by 104
- CategoryTheory.MorphismProperty.ContainsIdentitiesstatement and proof · cited by 94
- iInf_le_of_leproof · cited by 62
- AlgebraicGeometry.IsZariskiLocalAtSourcestatement and proof · cited by 37
- AlgebraicGeometry.IsLocalIsostatement and proof · cited by 9
- AlgebraicGeometry.IsLocalIso.le_of_isZariskiLocalAtSourceproof · cited by 2
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.