Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.Cover.toPresieveOverProp.congr_simp

∀ {P Q : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {S : AlgebraicGeometry.Scheme}
  [inst : P.IsStableUnderBaseChange] {X : Q.Over ⊤ S}
  (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X.left)
  [inst_1 : AlgebraicGeometry.Scheme.Cover.Over S 𝒰] (h : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)) ⦃Y : Q.Over ⊤ S⦄ (a a_1 : Y ⟶ X),
  a = a_1 → 𝒰.toPresieveOverProp h a = 𝒰.toPresieveOverProp h a_1

Defined in

Mathlib.AlgebraicGeometry.Sites.EtalePoint

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.MorphismProperty.IsStableUnderBaseChangeAlgebraicGeometry.Scheme.Cover.Over