Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.Cover.Over.congr_simp

∀ (S : AlgebraicGeometry.Scheme) {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme}
  [inst : P.IsStableUnderBaseChange] [inst_1 : AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P]
  {X : AlgebraicGeometry.Scheme} [inst_2 : X.Over S]
  (𝒰 𝒰_1 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X),
  𝒰 = 𝒰_1 → AlgebraicGeometry.Scheme.Cover.Over S 𝒰 = AlgebraicGeometry.Scheme.Cover.Over S 𝒰_1

Defined in

Mathlib.AlgebraicGeometry.Sites.EtalePoint

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.MorphismProperty.IsStableUnderBaseChangeAlgebraicGeometry.Scheme.IsJointlySurjectivePreservingAlgebraicGeometry.Scheme.Over