Commit 2026-02-13 12:38 81b174f9

View on Github →

feat(AlgebraicGeometry): reduced group schemes over algclosed fields are smooth (#35166)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/AlgebraicGeometry/AffineScheme.lean

added def AlgebraicGeometry.IsAffineOpen.arrowStalkMapIso

added theorem AlgebraicGeometry.IsAffineOpen.comap_primeIdealOf_appLE

Created Mathlib/AlgebraicGeometry/AlgClosed/Basic.lean

added theorem AlgebraicGeometry.SpecMap_residueFieldIsoBase_inv

added def AlgebraicGeometry.pointEquivClosedPoint

added def AlgebraicGeometry.pointOfClosedPoint

added theorem AlgebraicGeometry.pointOfClosedPoint_apply

added theorem AlgebraicGeometry.pointOfClosedPoint_comp

added def AlgebraicGeometry.residueFieldIsoBase

Created Mathlib/AlgebraicGeometry/Group/Smooth.lean

added theorem AlgebraicGeometry.smooth_of_grpObj_of_isAlgClosed

Modified Mathlib/AlgebraicGeometry/Morphisms/Smooth.lean

added theorem AlgebraicGeometry.Scheme.Hom.dense_smoothLocus_of_perfectField

added theorem AlgebraicGeometry.Scheme.Hom.genericPoint_mem_smoothLocus_of_perfectField

added theorem AlgebraicGeometry.Scheme.Hom.isOpen_smoothLocus

added theorem AlgebraicGeometry.Scheme.Hom.mem_smoothLocus

added theorem AlgebraicGeometry.Scheme.Hom.preimage_smoothLocus_eq

added def AlgebraicGeometry.Scheme.Hom.smoothLocus

added theorem AlgebraicGeometry.Scheme.Hom.smoothLocus_eq_top

added theorem AlgebraicGeometry.Scheme.Hom.smoothLocus_eq_top_iff

added theorem AlgebraicGeometry.exists_smooth_of_formallySmooth_stalk

added theorem AlgebraicGeometry.formallySmooth_stalkMap_iff

Modified Mathlib/AlgebraicGeometry/Properties.lean

Modified Mathlib/RingTheory/Etale/Basic.lean

added theorem Algebra.FormallyEtale.iff_restrictScalars

added theorem Algebra.FormallySmooth.iff_restrictScalars