Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.smallPretopology.congr_simp

∀ (P P_1 : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) (e_P : P = P_1)
  (Q : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) {S : AlgebraicGeometry.Scheme}
  [inst : P.IsStableUnderBaseChange] [inst_1 : P.IsMultiplicative] [inst_2 : P.RespectsIso]
  [inst_3 : Q.IsStableUnderComposition] [inst_4 : Q.IsStableUnderBaseChange] [inst_5 : Q.HasOfPostcompProperty Q],
  AlgebraicGeometry.Scheme.smallPretopology P Q = AlgebraicGeometry.Scheme.smallPretopology P_1 Q

Defined in

Mathlib.AlgebraicGeometry.Sites.Small

Cited by

0 results in Mathlib

Foundations

Depth 198 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.MorphismProperty.IsStableUnderBaseChangeCategoryTheory.MorphismProperty.IsMultiplicativeCategoryTheory.MorphismProperty.RespectsIsoCategoryTheory.MorphismProperty.IsStableUnderCompositionCategoryTheory.MorphismProperty.IsStableUnderBaseChangeCategoryTheory.MorphismProperty.HasOfPostcompProperty