Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.locallyCoverDense_of_le

∀ {P Q : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} (S : AlgebraicGeometry.Scheme)
  [P.IsStableUnderBaseChange] [P.IsMultiplicative] [P.RespectsIso] [Q.IsStableUnderComposition],
  P ≤ Q →
    (CategoryTheory.MorphismProperty.Over.forget Q ⊤ S).LocallyCoverDense
      (AlgebraicGeometry.Scheme.overGrothendieckTopology P S)

Defined in: Mathlib.AlgebraicGeometry.Sites.Small
Cited by: 1 results in Mathlib
Foundations: Depth 201 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CategoryTheory.MorphismProperty.IsStableUnderBaseChange CategoryTheory.MorphismProperty.IsMultiplicative CategoryTheory.MorphismProperty.RespectsIso CategoryTheory.MorphismProperty.IsStableUnderComposition

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites45

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

DFunLike.coeproof · cited by 62,936
Quiver.Homproof · cited by 32,603
CategoryTheory.Functor.objproof · cited by 19,642
Top.topstatement and proof · cited by 9,680
CategoryTheory.Functor.mapproof · cited by 8,698
Set.Elemproof · cited by 7,166
CategoryTheory.CategoryStruct.idproof · cited by 6,235
CategoryTheory.Functor.idstatement · cited by 3,333
AlgebraicGeometry.Schemestatement and proof · cited by 2,540
CategoryTheory.Discretestatement · cited by 2,447
CategoryTheory.MorphismPropertystatement and proof · cited by 2,179
CategoryTheory.Overstatement and proof · cited by 935

Cited by1

Results whose statement or proof uses this declaration.

AlgebraicGeometry.Scheme.smallGrothendieckTopology_eq_toGrothendieck_smallPretopologyproof · cited by 2