Comparing the big Zariski, étale, fppf and fpqc sites

Mathlib defines Scheme.zariskiTopology, Scheme.etaleTopology, Scheme.fppfTopology and Scheme.fpqcTopology, proves the fpqc topology subcanonical, and derives the fppf case from it. At the pin it records the comparisons zariskiTopology ≤ etaleTopology, zariskiPrecoverage ≤ fppfPrecoverage and fppfTopology ≤ fpqcTopology, but not the étale-to-fppf comparison, so the étale site has no Subcanonical instance and the Zariski-to-fppf comparison is available only at the precoverage level.

This file supplies the missing edges of that square. Every étale morphism is smooth, hence flat and locally of finite presentation, so an étale covering family is an fppf covering family; subcanonicity then descends along that inequality by GrothendieckTopology.Subcanonical.of_le. No new descent theorem is proved here: the content is Mathlib's fpqc descent for representables, transported along topology inequalities.

These are direct extensions of Mathlib's site API, stated about Mathlib's own topologies. Nothing here is about stacks, moduli, or algebraicity.

The fppf and étale precoverages also agree with their quasi-compact property precoverages: flat morphisms locally of finite presentation, and étale morphisms, are open maps. The resulting topology equalities extend Mathlib's AlgebraicGeometry/Sites/Fpqc.lean and AlgebraicGeometry/Sites/Etale.lean, their respective upstream owners.

theorem AlgebraicGeometry.Scheme.fppfPrecoverage_eq_propQCPrecoverage : fppfPrecoverage = propQCPrecoverage (@Flat ⊓ @LocallyOfFinitePresentation)

Flat morphisms locally of finite presentation are open, so the generic open-map criterion supplies the finite local refinements required by quasi-compact covers.

theorem AlgebraicGeometry.Scheme.fppfTopology_eq_propQCTopology : fppfTopology = propQCTopology (@Flat ⊓ @LocallyOfFinitePresentation)

Compare precoverages before generating the topology, using openness of flat, locally finitely presented morphisms rather than a new descent theorem.

theorem AlgebraicGeometry.Scheme.etalePrecoverage_eq_propQCPrecoverage : etalePrecoverage = propQCPrecoverage @Etale

Étale morphisms are open, so their jointly surjective covering families satisfy the quasi-compact covering condition without requiring each arrow to be quasi-compact.

theorem AlgebraicGeometry.Scheme.etaleTopology_eq_propQCTopology : etaleTopology = propQCTopology @Etale

Generate both topologies from the equal precoverages; the comparison requires no additional finiteness hypothesis beyond étaleness.

theorem AlgebraicGeometry.Scheme.etalePrecoverage_le_fppfPrecoverage : etalePrecoverage ≤ fppfPrecoverage

Every étale covering family is an fppf covering family: an étale morphism is smooth, hence flat and locally of finite presentation.

theorem AlgebraicGeometry.Scheme.etaleTopology_le_fppfTopology : etaleTopology ≤ fppfTopology

The étale topology is coarser than the fppf topology.

theorem AlgebraicGeometry.Scheme.etaleTopology_le_fpqcTopology : etaleTopology ≤ fpqcTopology

The étale topology is coarser than the fpqc topology.

theorem AlgebraicGeometry.Scheme.zariskiTopology_le_fppfTopology : zariskiTopology ≤ fppfTopology

The big Zariski topology is coarser than the fppf topology. Mathlib has this comparison at the level of precoverages only.

instance AlgebraicGeometry.Scheme.subcanonical_etaleTopology : etaleTopology.Subcanonical

The étale site is subcanonical, because the fppf site is and the étale topology is coarser. This is Mathlib's fpqc descent theorem for representables restricted along etaleTopology_le_fppfTopology; it is not a new descent result.