Scheme morphisms and big-Zariski stack presentation data

This file starts the algebraicity layer with two pieces of data that retain their geometric content:

• a scheme morphism induces a pullback-compatible morphism between the corresponding representable big-Zariski stacks;
• a property of a representable stack morphism is required on the actual structure morphism of every representing scheme.

The presentation structure at the end of this file is deliberately named for the big Zariski topology. It is useful geometric data, but it is not the standard definition of an algebraic stack: no fppf or étale descent theorem is proved here, and the diagonal is represented by schemes rather than algebraic spaces. No Artin representability theorem or opaque algebraicity proposition is introduced.

The fppf and étale descent level lives in DerivedAlgGeo.AlgebraicGeometry.Stacks.Descent, which also shows that a smooth surjection is an fppf covering family. That module does not change anything here: the diagonal below is still represented by schemes, and the presentations below are still big-Zariski presentations.

Which declarations here fix the topology, and which do not

The representability vocabulary -- StackMorphism.HasRepresentableProperty with its IsLocallyOfFinitePresentation, IsSmoothSurjective and IsOpenImmersion specializations, and StackInGroupoids.HasRepresentableDiagonal with its fiber representation -- says nothing about which covering families the stack condition quantifies over. Each is a statement about the representing scheme morphisms of a stack morphism's fibers, so each is stated for an arbitrary Grothendieck topology J on Scheme and reads identically at Zariski, étale and fppf.

What genuinely is Zariski is everything named for it: the representableZariski* constructions, whose descent comes from Scheme.zariskiTopology being subcanonical, and ZariskiStackPresentation and ZariskiStackPresentationOver, whose names record exactly the gap between what they supply and an algebraic stack.

The split is deliberate. Raising the presentations to fppf is SF9.2 (#522) work, and it should not also have to widen the vocabulary it is stated in.

def AlgebraicGeometry.representableZariskiStackMap {X Y : Scheme} (f : X ⟶ Y) : CategoryTheory.StackMorphism (representableZariskiStack X) (representableZariskiStack Y)

A scheme morphism induces the corresponding morphism between representable big-Zariski stacks by postcomposition on every test scheme.

Equations

• AlgebraicGeometry.representableZariskiStackMap f = CategoryTheory.StackInGroupoids.representableMap AlgebraicGeometry.Scheme.zariskiTopology f

@[simp]

theorem AlgebraicGeometry.representableZariskiStackMap_obj {X Y T : Scheme} (f : X ⟶ Y) (g : T ⟶ X) : ((representableZariskiStackMap f).app T).obj (representableZariskiObject g) = representableZariskiObject (CategoryTheory.CategoryStruct.comp g f)

@[simp]

theorem AlgebraicGeometry.representableZariskiStackMap_tripleComp_obj {W X Y Z T : Scheme} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z) (x : T ⟶ W) : ((((representableZariskiStackMap f).comp (representableZariskiStackMap g)).comp (representableZariskiStackMap h)).app T).obj (representableZariskiObject x) = representableZariskiObject (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp x f) g) h)

Three scheme-induced stack morphisms compose through Mathlib's strong transformation composition, with the expected pointwise action. The associator and unitors for this composition are the ones supplied by the pseudofunctor bicategory.

noncomputable def AlgebraicGeometry.RepresentableZariskiStackMap.fiberProduct {X Y S : Scheme} (f : X ⟶ Y) (y : CategoryTheory.Discrete (S ⟶ Y)) : CategoryTheory.Over S

The ordinary scheme fiber product representing the fiber of a representable-stack morphism over y : S ⟶ Y.

Equations

• AlgebraicGeometry.RepresentableZariskiStackMap.fiberProduct f y = CategoryTheory.Over.mk (CategoryTheory.Limits.pullback.snd f y.as)

noncomputable def AlgebraicGeometry.RepresentableZariskiStackMap.fiberFunctor {X Y S : Scheme} (f : X ⟶ Y) (y : CategoryTheory.Discrete (S ⟶ Y)) (T : CategoryTheory.Over S) : CategoryTheory.Functor (CategoryTheory.Discrete (T ⟶ fiberProduct f y)) ((representableZariskiStackMap f).FiberCategory y T)

Yoneda's fiber-product comparison as a functor into the actual groupoid fiber of the induced stack morphism.

Equations

• One or more equations did not get rendered due to their size.

instance AlgebraicGeometry.RepresentableZariskiStackMap.fiberFunctor_faithful {X Y S : Scheme} (f : X ⟶ Y) (y : CategoryTheory.Discrete (S ⟶ Y)) (T : CategoryTheory.Over S) : (fiberFunctor f y T).Faithful

instance AlgebraicGeometry.RepresentableZariskiStackMap.fiberFunctor_full {X Y S : Scheme} (f : X ⟶ Y) (y : CategoryTheory.Discrete (S ⟶ Y)) (T : CategoryTheory.Over S) : (fiberFunctor f y T).Full

instance AlgebraicGeometry.RepresentableZariskiStackMap.fiberFunctor_essSurj {X Y S : Scheme} (f : X ⟶ Y) (y : CategoryTheory.Discrete (S ⟶ Y)) (T : CategoryTheory.Over S) : (fiberFunctor f y T).EssSurj

noncomputable def AlgebraicGeometry.RepresentableZariskiStackMap.fiberRepresentation {X Y S : Scheme} (f : X ⟶ Y) (y : CategoryTheory.Discrete (S ⟶ Y)) : (representableZariskiStackMap f).FiberRepresentation y

The fiber of a morphism between representable stacks is represented by the ordinary scheme fiber product, with its full Yoneda universal property.

Equations

• One or more equations did not get rendered due to their size.

instance AlgebraicGeometry.representableZariskiStackMap_isRepresentable {X Y : Scheme} (f : X ⟶ Y) : (representableZariskiStackMap f).IsRepresentable

Every scheme-induced morphism of representable stacks is representable, and its representing schemes are the actual fiber products.

structure AlgebraicGeometry.StackMorphism.FiberRepresentationWithProperty {J : CategoryTheory.GrothendieckTopology Scheme} {F G : CategoryTheory.StackInGroupoids Scheme J} (f : CategoryTheory.StackMorphism F G) (P : CategoryTheory.MorphismProperty Scheme) {S : Scheme} (y : ↑(G.presheaf.obj { as := Opposite.op S })) extends f.FiberRepresentation y : Type (max (u + 1) u_1)

A represented fiber together with a property of its actual structure morphism to the test scheme.

• representing : Over S
• fiberEquivalence (T : Over S) : Discrete (T ⟶ self.representing) ≌ f.FiberCategory y T
• property : P self.representing.hom

  The geometric property is asserted on the representing scheme morphism, not on an abstract stack-level token.

class AlgebraicGeometry.StackMorphism.HasRepresentableProperty {J : CategoryTheory.GrothendieckTopology Scheme} {F G : CategoryTheory.StackInGroupoids Scheme J} (P : CategoryTheory.MorphismProperty Scheme) (f : CategoryTheory.StackMorphism F G) : Prop

A stack morphism is representable with property P when every one of its fibers has a representing scheme whose structure morphism satisfies P.

• representation {S : Scheme} (y : ↑(G.presheaf.obj { as := Opposite.op S })) : Nonempty (FiberRepresentationWithProperty f P y)

theorem AlgebraicGeometry.StackMorphism.isRepresentable_of_hasRepresentableProperty {J : CategoryTheory.GrothendieckTopology Scheme} {F G : CategoryTheory.StackInGroupoids Scheme J} {P : CategoryTheory.MorphismProperty Scheme} {f : CategoryTheory.StackMorphism F G} [HasRepresentableProperty P f] : f.IsRepresentable

Forgetting the geometric property recovers ordinary representability.

theorem AlgebraicGeometry.StackMorphism.hasRepresentableProperty_mono {J : CategoryTheory.GrothendieckTopology Scheme} {F G : CategoryTheory.StackInGroupoids Scheme J} {P Q : CategoryTheory.MorphismProperty Scheme} {f : CategoryTheory.StackMorphism F G} (hPQ : P ≤ Q) [HasRepresentableProperty P f] : HasRepresentableProperty Q f

Representable properties are monotone under implication of the underlying scheme-morphism properties.

theorem AlgebraicGeometry.representableZariskiStackMap_hasRepresentableProperty (P : CategoryTheory.MorphismProperty Scheme) [P.IsStableUnderBaseChange] {X Y : Scheme} (f : X ⟶ Y) (hf : P f) : StackMorphism.HasRepresentableProperty P (representableZariskiStackMap f)

A base-change-stable scheme-morphism property passes to the induced morphism of representable stacks because each representing morphism is the corresponding scheme-theoretic pullback.

@[reducible, inline]

abbrev AlgebraicGeometry.StackMorphism.IsLocallyOfFinitePresentation {J : CategoryTheory.GrothendieckTopology Scheme} {F G : CategoryTheory.StackInGroupoids Scheme J} (f : CategoryTheory.StackMorphism F G) : Prop

Local finite presentation for stack morphisms is measured on the actual representing scheme morphisms of all fibers.

Equations

• AlgebraicGeometry.StackMorphism.IsLocallyOfFinitePresentation f = AlgebraicGeometry.StackMorphism.HasRepresentableProperty (@AlgebraicGeometry.LocallyOfFinitePresentation) f

@[reducible, inline]

abbrev AlgebraicGeometry.StackMorphism.IsSmoothSurjective {J : CategoryTheory.GrothendieckTopology Scheme} {F G : CategoryTheory.StackInGroupoids Scheme J} (f : CategoryTheory.StackMorphism F G) : Prop

A smooth-surjective stack cover is representable and every representing scheme morphism is both smooth and surjective.

Equations

• AlgebraicGeometry.StackMorphism.IsSmoothSurjective f = AlgebraicGeometry.StackMorphism.HasRepresentableProperty (@AlgebraicGeometry.Smooth ⊓ @AlgebraicGeometry.Surjective) f

@[reducible, inline]

abbrev AlgebraicGeometry.StackMorphism.IsOpenImmersion {J : CategoryTheory.GrothendieckTopology Scheme} {F G : CategoryTheory.StackInGroupoids Scheme J} (f : CategoryTheory.StackMorphism F G) : Prop

An open immersion of stacks is representable and is an open immersion on every actual scheme representing one of its fibers.

Equations

• AlgebraicGeometry.StackMorphism.IsOpenImmersion f = AlgebraicGeometry.StackMorphism.HasRepresentableProperty AlgebraicGeometry.IsOpenImmersion f

theorem AlgebraicGeometry.representableZariskiStackMap_id_isSmoothSurjective (X : Scheme) : StackMorphism.IsSmoothSurjective (representableZariskiStackMap (CategoryTheory.CategoryStruct.id X))

The identity atlas of every representable stack is an actual smooth-surjective representable morphism.

theorem AlgebraicGeometry.representableZariskiStackMap_id_isLocallyOfFinitePresentation (X : Scheme) : StackMorphism.IsLocallyOfFinitePresentation (representableZariskiStackMap (CategoryTheory.CategoryStruct.id X))

The identity structural morphism of every representable stack is locally of finite presentation on all actual fiber schemes.

theorem AlgebraicGeometry.representableZariskiStackMap_isOpenImmersion {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] : StackMorphism.IsOpenImmersion (representableZariskiStackMap f)

A scheme-theoretic open immersion induces an open immersion of its representable big-Zariski stacks, checked on the actual pullback schemes.

Diagonal representability and big-Zariski presentations

structure AlgebraicGeometry.StackInGroupoids.DiagonalFiberRepresentation {J : CategoryTheory.GrothendieckTopology Scheme} (F : CategoryTheory.StackInGroupoids Scheme J) {S : Scheme} (x y : ↑(F.presheaf.obj { as := Opposite.op S })) : Type (max (u + 1) u_1)

A scheme representing the isomorphisms between the pullbacks of two objects of a stack. The equivalence is the pointwise Yoneda universal property of the representing object over the test scheme.

• representing : CategoryTheory.Over S

  The scheme of isomorphisms over S.

• isomorphismEquiv (T : CategoryTheory.Over S) : (T ⟶ self.representing) ≃ ((F.presheaf.map T.hom.op.toLoc).toFunctor.obj x ≅ (F.presheaf.map T.hom.op.toLoc).toFunctor.obj y)

  Arrows to the representing scheme classify actual isomorphisms after pullback.

class AlgebraicGeometry.StackInGroupoids.HasRepresentableDiagonal {J : CategoryTheory.GrothendieckTopology Scheme} (F : CategoryTheory.StackInGroupoids Scheme J) : Prop

A stack has representable diagonal when every pair of objects has an actual scheme representing its isomorphism functor.

• representation {S : Scheme} (x y : ↑(F.presheaf.obj { as := Opposite.op S })) : Nonempty (DiagonalFiberRepresentation F x y)

noncomputable def AlgebraicGeometry.representableZariskiDiagonalFiberRepresentation {X S : Scheme} (x y : CategoryTheory.Discrete (S ⟶ X)) : StackInGroupoids.DiagonalFiberRepresentation (representableZariskiStack X) x y

For a representable stack, the diagonal fiber over two maps x,y : S ⟶ X is the scheme-theoretic equalizer of those maps.

Equations

• One or more equations did not get rendered due to their size.

instance AlgebraicGeometry.representableZariskiStack_hasRepresentableDiagonal (X : Scheme) : StackInGroupoids.HasRepresentableDiagonal (representableZariskiStack X)

structure AlgebraicGeometry.ZariskiStackPresentation : Type (u + 1)

A provisional big-Zariski stack presentation: effective Zariski descent, a diagonal represented by schemes, and a scheme atlas whose every fiber is represented by a smooth-surjective scheme morphism.

This is not called AlgebraicStack: the standard notion requires fppf descent or an equivalent étale formulation, and usually asks for the diagonal to be representable by algebraic spaces.

• toStackInGroupoids : CategoryTheory.StackInGroupoids Scheme Scheme.zariskiTopology

  The underlying big-Zariski stack in groupoids.

• schemeDiagonal : StackInGroupoids.HasRepresentableDiagonal self.toStackInGroupoids

  The diagonal is represented by schemes via its isomorphism functors. The scheme-level representability is explicit because it is stronger than the usual algebraic-space diagonal condition.

• atlasScheme : Scheme

  The scheme presenting the stack.

• atlas : CategoryTheory.StackMorphism (representableZariskiStack self.atlasScheme) self.toStackInGroupoids

  The atlas morphism from the corresponding representable stack.

• atlasSmoothSurjective : StackMorphism.IsSmoothSurjective self.atlas

  Every base change of the atlas is an actual smooth-surjective scheme morphism.

def AlgebraicGeometry.representableZariskiStackPresentation (X : Scheme) : ZariskiStackPresentation

Every representable big-Zariski stack has a Zariski presentation using its identity atlas and its scheme-theoretic equalizer diagonal.

Equations

• One or more equations did not get rendered due to their size.

structure AlgebraicGeometry.ZariskiStackPresentationOver (S : Scheme) : Type (u + 1)

A big-Zariski stack presentation locally of finite presentation over a base scheme, expressed by an actual stack morphism whose every fiber has a locally-finite-presentation representing scheme morphism.

• toZariskiStackPresentation : ZariskiStackPresentation

  The underlying big-Zariski presentation.

• structureMorphism : CategoryTheory.StackMorphism self.toZariskiStackPresentation.toStackInGroupoids (representableZariskiStack S)

  Its structural morphism to the representable stack of the base.

• locallyOfFinitePresentation : StackMorphism.IsLocallyOfFinitePresentation self.structureMorphism

  Local finite presentation is checked on all scheme representatives of the structural morphism.

def AlgebraicGeometry.representableZariskiStackPresentationOver {X S : Scheme} (p : X ⟶ S) [LocallyOfFinitePresentation p] : ZariskiStackPresentationOver S

A locally finitely presented scheme morphism gives a locally finitely presented big-Zariski presentation over the target. All fiber representatives are the actual scheme fiber products.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AlgebraicGeometry.affineLineZariskiStackPresentationOver (S : Scheme) : ZariskiStackPresentationOver S

A concrete positive-dimensional supported case: the representable affine-line stack has a Zariski presentation locally of finite presentation over every base scheme.

Equations

• AlgebraicGeometry.affineLineZariskiStackPresentationOver S = AlgebraicGeometry.representableZariskiStackPresentationOver (AlgebraicGeometry.AffineSpace (ULift.{?u.1, 0} (Fin 1)) S ↘ S)