Documentation Verification Report

Fpqc

📁 Source: Mathlib/AlgebraicGeometry/Sites/Fpqc.lean

Statistics

Metric	Count
Definitions `fppfPrecoverage`, `fppfTopology`, `fpqcPrecoverage`, `fpqcTopology`, `instHasIsosFpqcPrecoverage`, `instIsStableUnderBaseChangeFppfPrecoverage`, `instIsStableUnderBaseChangeFpqcPrecoverage`, `instIsStableUnderCompositionFppfPrecoverage`, `instIsStableUnderCompositionFpqcPrecoverage`	9
Theorems `singleton_mem_fppfPrecoverage`, `singleton_mem_fpqcPrecoverage`, `fppfPrecoverage_eq_inf`, `fppfPrecoverage_le_fpqcPrecoverage`, `fppfTopology_le_fpqcTopology`, `fpqcTopology_eq_propQCTopology`, `instEffectiveEpiOfLocallyOfFinitePresentationOfSurjectiveOfFlat`, `instEffectiveEpiOfQuasiCompactOfSurjectiveOfFlat`, `instSubcanonicalFppfTopology`, `instSubcanonicalFpqcTopology`, `zariskiPrecoverage_le_fppfPrecoverage`, `zariskiPrecoverage_le_fpqcPrecoverage`, `zariskiTopology_le_fpqcTopology`	13
Total	22

AlgebraicGeometry.Scheme

Definitions

Name	Category	Theorems
`fppfPrecoverage` 📖	CompOp	4 math math: `fppfPrecoverage_le_fpqcPrecoverage`, `zariskiPrecoverage_le_fppfPrecoverage`, `Hom.singleton_mem_fppfPrecoverage`, `fppfPrecoverage_eq_inf`
`fppfTopology` 📖	CompOp	2 math math: `instSubcanonicalFppfTopology`, `fppfTopology_le_fpqcTopology`
`fpqcPrecoverage` 📖	CompOp	4 math math: `Hom.singleton_mem_fpqcPrecoverage`, `fppfPrecoverage_le_fpqcPrecoverage`, `proetalePrecoverage_le_fpqcPrecoverage`, `zariskiPrecoverage_le_fpqcPrecoverage`
`fpqcTopology` 📖	CompOp	7 math math: `zariskiTopology_le_fpqcTopology`, `AlgebraicGeometry.isSheaf_fpqcTopology_continuousMapPresheafAb`, `instSubcanonicalFpqcTopology`, `fppfTopology_le_fpqcTopology`, `fpqcTopology_eq_propQCTopology`, `AlgebraicGeometry.isSheaf_fpqcTopology_continuousMapPresheaf`, `proetaleTopology_le_fpqcTopology`
`instHasIsosFpqcPrecoverage` 📖	CompOp	—
`instIsStableUnderBaseChangeFppfPrecoverage` 📖	CompOp	—
`instIsStableUnderBaseChangeFpqcPrecoverage` 📖	CompOp	—
`instIsStableUnderCompositionFppfPrecoverage` 📖	CompOp	—
`instIsStableUnderCompositionFpqcPrecoverage` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fppfPrecoverage_eq_inf` 📖	mathematical	—	`fppfPrecoverage` `CategoryTheory.Precoverage` `AlgebraicGeometry.Scheme` `instCategory` `CategoryTheory.Precoverage.instMin` `precoverage` `AlgebraicGeometry.Flat` `AlgebraicGeometry.LocallyOfFinitePresentation`	—	—
`fppfPrecoverage_le_fpqcPrecoverage` 📖	mathematical	—	`CategoryTheory.Precoverage` `AlgebraicGeometry.Scheme` `instCategory` `Preorder.toLE` `PartialOrder.toPreorder` `CategoryTheory.Precoverage.instPartialOrder` `fppfPrecoverage` `fpqcPrecoverage`	—	`fpqcPrecoverage.eq_1` `propQCPrecoverage.eq_1` `le_inf_iff` `precoverage_le_qcPrecoverage_of_isOpenMap` `Hom.isOpenMap` `AlgebraicGeometry.UniversallyOpen.of_flat` `precoverage_mono`
`fppfTopology_le_fpqcTopology` 📖	mathematical	—	`CategoryTheory.GrothendieckTopology` `AlgebraicGeometry.Scheme` `instCategory` `CategoryTheory.GrothendieckTopology.instLEGrothendieckTopology` `fppfTopology` `fpqcTopology`	—	`CategoryTheory.Precoverage.toGrothendieck_mono` `fppfPrecoverage_le_fpqcPrecoverage`
`fpqcTopology_eq_propQCTopology` 📖	mathematical	—	`fpqcTopology` `propQCTopology` `AlgebraicGeometry.Flat`	—	—
`instEffectiveEpiOfLocallyOfFinitePresentationOfSurjectiveOfFlat` 📖	mathematical	—	`CategoryTheory.EffectiveEpi` `AlgebraicGeometry.Scheme` `instCategory`	—	`CategoryTheory.Sieve.effectiveEpimorphic_singleton` `CategoryTheory.Presieve.EffectiveEpimorphic.iff_forall_isSheafFor_yoneda` `CategoryTheory.Presieve.IsSheaf.isSheafFor` `CategoryTheory.GrothendieckTopology.Subcanonical.isSheaf_of_isRepresentable` `instSubcanonicalFppfTopology` `CategoryTheory.Functor.instIsRepresentableObjOppositeTypeYoneda` `CategoryTheory.Precoverage.generate_mem_toGrothendieck` `Hom.singleton_mem_fppfPrecoverage`
`instEffectiveEpiOfQuasiCompactOfSurjectiveOfFlat` 📖	mathematical	—	`CategoryTheory.EffectiveEpi` `AlgebraicGeometry.Scheme` `instCategory`	—	`CategoryTheory.Sieve.effectiveEpimorphic_singleton` `CategoryTheory.Presieve.EffectiveEpimorphic.iff_forall_isSheafFor_yoneda` `CategoryTheory.Presieve.IsSheaf.isSheafFor` `CategoryTheory.GrothendieckTopology.Subcanonical.isSheaf_of_isRepresentable` `instSubcanonicalFpqcTopology` `CategoryTheory.Functor.instIsRepresentableObjOppositeTypeYoneda` `CategoryTheory.Precoverage.generate_mem_toGrothendieck` `Hom.singleton_mem_fpqcPrecoverage`
`instSubcanonicalFppfTopology` 📖	mathematical	—	`CategoryTheory.GrothendieckTopology.Subcanonical` `AlgebraicGeometry.Scheme` `instCategory` `fppfTopology`	—	`CategoryTheory.GrothendieckTopology.Subcanonical.of_le` `fppfTopology_le_fpqcTopology` `instSubcanonicalFpqcTopology`
`instSubcanonicalFpqcTopology` 📖	mathematical	—	`CategoryTheory.GrothendieckTopology.Subcanonical` `AlgebraicGeometry.Scheme` `instCategory` `fpqcTopology`	—	`CategoryTheory.GrothendieckTopology.Subcanonical.of_isSheaf_yoneda_obj` `fpqcTopology_eq_propQCTopology` `AlgebraicGeometry.isSheaf_type_propQCTopology_iff` `AlgebraicGeometry.Flat.isStableUnderBaseChange` `AlgebraicGeometry.Flat.instIsMultiplicativeScheme` `AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtSource` `AlgebraicGeometry.Flat.instHasRingHomPropertyFlat` `CategoryTheory.GrothendieckTopology.Subcanonical.isSheaf_of_isRepresentable` `subcanonical_zariskiTopology` `CategoryTheory.Functor.instIsRepresentableObjOppositeTypeYoneda` `AlgebraicGeometry.isRegularEpi_of_flat_of_surjective_of_isAffine` `AlgebraicGeometry.isAffine_Spec` `CategoryTheory.Presieve.IsSheafFor.singleton_of_isRepresentable_of_effectiveEpi` `CategoryTheory.instEffectiveEpiOfIsRegularEpi`
`zariskiPrecoverage_le_fppfPrecoverage` 📖	mathematical	—	`CategoryTheory.Precoverage` `AlgebraicGeometry.Scheme` `instCategory` `Preorder.toLE` `PartialOrder.toPreorder` `CategoryTheory.Precoverage.instPartialOrder` `zariskiPrecoverage` `fppfPrecoverage`	—	`precoverage_mono` `AlgebraicGeometry.Flat.instOfIsOpenImmersion` `AlgebraicGeometry.locallyOfFinitePresentation_of_isOpenImmersion`
`zariskiPrecoverage_le_fpqcPrecoverage` 📖	mathematical	—	`CategoryTheory.Precoverage` `AlgebraicGeometry.Scheme` `instCategory` `Preorder.toLE` `PartialOrder.toPreorder` `CategoryTheory.Precoverage.instPartialOrder` `zariskiPrecoverage` `fpqcPrecoverage`	—	`le_trans` `zariskiPrecoverage_le_fppfPrecoverage` `fppfPrecoverage_le_fpqcPrecoverage`
`zariskiTopology_le_fpqcTopology` 📖	mathematical	—	`CategoryTheory.GrothendieckTopology` `AlgebraicGeometry.Scheme` `instCategory` `CategoryTheory.GrothendieckTopology.instLEGrothendieckTopology` `zariskiTopology` `fpqcTopology`	—	`CategoryTheory.Precoverage.toGrothendieck_mono` `zariskiPrecoverage_le_fpqcPrecoverage`

AlgebraicGeometry.Scheme.Hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`singleton_mem_fppfPrecoverage` 📖	mathematical	—	`CategoryTheory.Presieve` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `Set` `Set.instMembership` `CategoryTheory.Precoverage.coverings` `AlgebraicGeometry.Scheme.fppfPrecoverage` `CategoryTheory.Presieve.singleton`	—	`CategoryTheory.Presieve.ofArrows_pUnit` `CategoryTheory.Precoverage.ZeroHypercover.mem₀`
`singleton_mem_fpqcPrecoverage` 📖	mathematical	—	`CategoryTheory.Presieve` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `Set` `Set.instMembership` `CategoryTheory.Precoverage.coverings` `AlgebraicGeometry.Scheme.fpqcPrecoverage` `CategoryTheory.Presieve.singleton`	—	`singleton_mem_propQCPrecoverage`

---

← Back to Index