Theorems · Theorem · algebraic geometry

CategoryTheory.MorphismProperty.pretopology_inf

∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  (P Q : CategoryTheory.MorphismProperty C) [inst_2 : P.IsMultiplicative] [inst_3 : P.IsStableUnderBaseChange]
  [inst_4 : Q.IsMultiplicative] [inst_5 : Q.IsStableUnderBaseChange],
  (P ⊓ Q).pretopology = P.pretopology ⊓ Q.pretopology

Defined in: Mathlib.CategoryTheory.Sites.MorphismProperty
Cited by: 0 results in Mathlib
Foundations: Depth 67 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CategoryTheory.Category CategoryTheory.Limits.HasPullbacks CategoryTheory.MorphismProperty.IsMultiplicative CategoryTheory.MorphismProperty.IsStableUnderBaseChange CategoryTheory.MorphismProperty.IsMultiplicative CategoryTheory.MorphismProperty.IsStableUnderBaseChange

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites13

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

CategoryTheory.Categorystatement and proof · cited by 32,673
CategoryTheory.MorphismPropertystatement and proof · cited by 2,179
CategoryTheory.Limits.HasPullbacksstatement and proof · cited by 439
CategoryTheory.MorphismProperty.IsMultiplicativestatement and proof · cited by 332
CategoryTheory.Precoverage.coveringsproof · cited by 194
CategoryTheory.MorphismProperty.IsStableUnderBaseChangestatement and proof · cited by 131
CategoryTheory.Pretopology.toPrecoverageproof · cited by 34
CategoryTheory.Pretopologystatement · cited by 32
CategoryTheory.MorphismProperty.precoverageproof · cited by 23
CategoryTheory.MorphismProperty.pretopologystatement and proof · cited by 8
CategoryTheory.Pretopology.extproof · cited by 3
CategoryTheory.MorphismProperty.precoverage_infproof · cited by 1

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.