Commit 2026-06-09 19:37 e82fa2a5

View on Github →

feat(AlgebraicGeometry/Morphisms/UniversallyInjective): equivalent criteria for universally injective morphisms (#39910) We prove stacks 01S4, which gives two new equivalent criteria for being universally injective.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/UniversallyInjective.lean

added theorem AlgebraicGeometry.tfae_universallyInjective

Modified Mathlib/AlgebraicGeometry/ResidueField.lean

added theorem AlgebraicGeometry.Scheme.Hom.residueFieldMap_congr'

added theorem AlgebraicGeometry.Scheme.descResidueField_stalkClosedPointTo_comp

Modified Mathlib/FieldTheory/PurelyInseparable/Basic.lean

added theorem isPurelyInseparable_iff_subsingleton_emb

Created Mathlib/RingTheory/RingHom/PurelyInseparable.lean

added theorem RingHom.IsPurelyInseparable.comp

added theorem RingHom.IsPurelyInseparable.containsIdentities

added theorem RingHom.IsPurelyInseparable.id

added theorem RingHom.isPurelyInseparable_algebraMap_iff