Commit 2026-06-18 11:17 028b72cd

View on Github →

feat(AlgebraicGeometry): points of the small étale site (#35136) The main definition in this PR is Scheme.pointSmallEtale. Given a morphism Spec (.of Ω) ⟶ S where Ω is a separably closed field, we define the corresponding point of the small étale site of S. We show that these points form a conservative family. (This PR also removes the definition Scheme.geometricFiber which was not correct.)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/AlgebraicGeometry/Fiber.lean

added theorem AlgebraicGeometry.Scheme.Hom.fiber_fac

Modified Mathlib/AlgebraicGeometry/Morphisms/Etale.lean

added theorem AlgebraicGeometry.Scheme.Etale.forget_mk

added theorem AlgebraicGeometry.Scheme.Etale.forget_obj_hom

added theorem AlgebraicGeometry.Scheme.Etale.forget_obj_left

added def AlgebraicGeometry.Scheme.Etale.rec

Modified Mathlib/AlgebraicGeometry/Sites/Etale.lean

added theorem AlgebraicGeometry.Scheme.ofArrows_mem_smallEtaleTopology_iff

Created Mathlib/AlgebraicGeometry/Sites/EtalePoint.lean

added theorem AlgebraicGeometry.Scheme.exists_fac_of_etale_of_isSepClosed

added theorem AlgebraicGeometry.Scheme.isConservativeFamilyOfPoints_pointSmallEtale'

added theorem AlgebraicGeometry.Scheme.isConservative_pointSmallEtale

added theorem AlgebraicGeometry.Scheme.pointSmallEtaleFiberObjToPreimage_surjective

Modified Mathlib/CategoryTheory/Elements.lean

added def CategoryTheory.Functor.Elements.precomp

Modified Mathlib/CategoryTheory/EssentialImage.lean

added theorem CategoryTheory.ObjectProperty.map_top

Modified Mathlib/CategoryTheory/Limits/FinallySmall.lean

added theorem CategoryTheory.initiallySmall_of_essentiallySmall_weakly_initial_objectProperty

Modified Mathlib/CategoryTheory/Limits/MorphismProperty.lean

Modified Mathlib/CategoryTheory/MorphismProperty/Comma.lean

Modified Mathlib/CategoryTheory/MorphismProperty/CommaSites.lean

Modified Mathlib/CategoryTheory/ObjectProperty/Small.lean