Site defined by a morphism property

Given a multiplicative morphism property P that is stable under base change, we define the associated precoverage on the category of schemes, where coverings are given by jointly surjective families of morphisms satisfying P.

class AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving (P : CategoryTheory.MorphismProperty Scheme) : Prop

A morphism property of schemes is said to preserve joint surjectivity, if for any pair of morphisms f : X ⟶ S and g : Y ⟶ S where g satisfies P, any pair of points x : X and y : Y with f x = g y can be lifted to a point of X ×[S] Y.

In later files, this will be automatic, since this holds for any morphism g (see AlgebraicGeometry.Scheme.isJointlySurjectivePreserving). But at this early stage in the import tree, we only know it for open immersions.

• exists_preimage_fst_triplet_of_prop {X Y S : Scheme} {f : X ⟶ S} {g : Y ⟶ S} [CategoryTheory.Limits.HasPullback f g] (hg : P g) (x : ↥X) (y : ↥Y) (h : (CategoryTheory.ConcreteCategory.hom f.base) x = (CategoryTheory.ConcreteCategory.hom g.base) y) : ∃ (a : ↥(CategoryTheory.Limits.pullback f g)), (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.fst f g).base) a = x

theorem AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving.exists_preimage_snd_triplet_of_prop {P : CategoryTheory.MorphismProperty Scheme} [IsJointlySurjectivePreserving P] {X Y S : Scheme} {f : X ⟶ S} {g : Y ⟶ S} [CategoryTheory.Limits.HasPullback f g] (hf : P f) (x : ↥X) (y : ↥Y) (h : (CategoryTheory.ConcreteCategory.hom f.base) x = (CategoryTheory.ConcreteCategory.hom g.base) y) : ∃ (a : ↥(CategoryTheory.Limits.pullback f g)), (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.snd f g).base) a = y

instance AlgebraicGeometry.Scheme.instIsJointlySurjectivePreservingIsOpenImmersion : IsJointlySurjectivePreserving IsOpenImmersion

@[reducible, inline]

abbrev AlgebraicGeometry.Scheme.jointlySurjectivePrecoverage : CategoryTheory.Precoverage Scheme

The precoverage on Scheme of jointly surjective families.

Equations

• AlgebraicGeometry.Scheme.jointlySurjectivePrecoverage = CategoryTheory.Precoverage.comap AlgebraicGeometry.Scheme.forget CategoryTheory.Types.jointlySurjectivePrecoverage

def AlgebraicGeometry.Scheme.precoverage (P : CategoryTheory.MorphismProperty Scheme) : CategoryTheory.Precoverage Scheme

The precoverage on Scheme induced by P is given by jointly surjective families of P-morphisms.

Equations

• AlgebraicGeometry.Scheme.precoverage P = AlgebraicGeometry.Scheme.jointlySurjectivePrecoverage ⊓ P.precoverage

@[simp]

theorem AlgebraicGeometry.Scheme.ofArrows_mem_precoverage_iff (P : CategoryTheory.MorphismProperty Scheme) {S : Scheme} {ι : Type u_1} {X : ι → Scheme} {f : (i : ι) → X i ⟶ S} : CategoryTheory.Presieve.ofArrows X f ∈ (precoverage P).coverings S ↔ (∀ (x : ↥S), ∃ (i : ι), x ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom (f i).base)) ∧ ∀ (i : ι), P (f i)

instance AlgebraicGeometry.Scheme.instIsStableUnderCompositionPrecoverageOfIsStableUnderComposition (P : CategoryTheory.MorphismProperty Scheme) [P.IsStableUnderComposition] : (precoverage P).IsStableUnderComposition

instance AlgebraicGeometry.Scheme.instHasIsosPrecoverageOfContainsIdentitiesOfRespectsIso (P : CategoryTheory.MorphismProperty Scheme) [P.ContainsIdentities] [P.RespectsIso] : (precoverage P).HasIsos

instance AlgebraicGeometry.Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange (P : CategoryTheory.MorphismProperty Scheme) [IsJointlySurjectivePreserving P] [P.IsStableUnderBaseChange] : (precoverage P).IsStableUnderBaseChange

@[reducible, inline]

abbrev AlgebraicGeometry.Scheme.zariskiPrecoverage : CategoryTheory.Precoverage Scheme

The Zariski precoverage on the category of schemes is the precoverage defined by jointly surjective families of open immersions.

Equations

• AlgebraicGeometry.Scheme.zariskiPrecoverage = AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion