Commit 2025-05-04 20:18 758a2cdd

View on Github →

feat(AlgebraicGeometry): the small étale site (#24568) Upstreamed from Pi1.

Estimated changes

Modified Mathlib/AlgebraicGeometry/Morphisms/Etale.lean

deleted def AlgebraicGeometry.Etale.forget

deleted def AlgebraicGeometry.Etale.forgetFullyFaithful

deleted def AlgebraicGeometry.Etale

added theorem AlgebraicGeometry.IsEtale.of_comp

added def AlgebraicGeometry.Scheme.Etale.forget

added def AlgebraicGeometry.Scheme.Etale.forgetFullyFaithful

added def AlgebraicGeometry.Scheme.Etale

Modified Mathlib/AlgebraicGeometry/Morphisms/FinitePresentation.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/FormallyUnramified.lean

deleted theorem AlgebraicGeometry.FormallyUnramified.AlgebraicGeometry.FormallyUnramified.isOpenImmersion_diagonal

Modified Mathlib/AlgebraicGeometry/Sites/Etale.lean

added def AlgebraicGeometry.Scheme.smallEtalePretopology

added def AlgebraicGeometry.Scheme.smallEtaleTopology