Commit 2024-04-17 10:49 c9ab842e

View on Github →

feat(RingTheory/Etale): add definition of unramified, smooth and etale (#12044) Adds definitions for unramified, smooth and étale algebras and shows basic permanence properties. In a follow-up PR we show that these notions are stable under base change.

Estimated changes

Modified Mathlib/RingTheory/Etale/Basic.lean

added theorem Algebra.Etale.comp

added theorem Algebra.Etale.of_equiv

added theorem Algebra.Etale.of_isLocalization_Away

modified theorem Algebra.FormallyEtale.comp

modified theorem Algebra.FormallyEtale.iff_unramified_and_smooth

modified theorem Algebra.FormallyEtale.localization_base

modified theorem Algebra.FormallyEtale.localization_map

modified theorem Algebra.FormallyEtale.of_equiv

modified theorem Algebra.FormallyEtale.of_isLocalization

modified theorem Algebra.FormallyEtale.of_unramified_and_smooth

Modified Mathlib/RingTheory/Smooth/Basic.lean

modified theorem Algebra.FormallySmooth.comp

modified theorem Algebra.FormallySmooth.comp_lift

modified theorem Algebra.FormallySmooth.comp_liftOfSurjective

modified theorem Algebra.FormallySmooth.exists_lift

modified theorem Algebra.FormallySmooth.iff_split_surjection

modified theorem Algebra.FormallySmooth.liftOfSurjective_apply

modified theorem Algebra.FormallySmooth.localization_base

modified theorem Algebra.FormallySmooth.localization_map

modified theorem Algebra.FormallySmooth.mk_lift

modified theorem Algebra.FormallySmooth.of_equiv

modified theorem Algebra.FormallySmooth.of_isLocalization

modified theorem Algebra.FormallySmooth.of_split

added theorem Algebra.Smooth.comp

added theorem Algebra.Smooth.of_equiv

added theorem Algebra.Smooth.of_isLocalization_Away

Modified Mathlib/RingTheory/Unramified/Basic.lean

modified theorem Algebra.FormallyUnramified.comp

modified theorem Algebra.FormallyUnramified.ext'

modified theorem Algebra.FormallyUnramified.ext

modified theorem Algebra.FormallyUnramified.lift_unique'

modified theorem Algebra.FormallyUnramified.lift_unique

modified theorem Algebra.FormallyUnramified.lift_unique_of_ringHom

modified theorem Algebra.FormallyUnramified.localization_base

modified theorem Algebra.FormallyUnramified.localization_map

modified theorem Algebra.FormallyUnramified.of_comp

modified theorem Algebra.FormallyUnramified.of_equiv

modified theorem Algebra.FormallyUnramified.of_isLocalization

added theorem Algebra.Unramified.comp

added theorem Algebra.Unramified.of_equiv

added theorem Algebra.Unramified.of_isLocalization_Away