Commit 2025-01-25 16:37 773fd70b

View on Github →

feat(RingTheory): the smooth locus of an algebra (#20953)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Module/FinitePresentation.lean

added theorem Module.finitePresentation_of_projective_of_exact

added theorem Module.finitePresentation_of_split_exact

Modified Mathlib/RingTheory/Extension.lean

added theorem Algebra.Extension.Cotangent.finite

Modified Mathlib/RingTheory/Kaehler/CotangentComplex.lean

added def Algebra.H1Cotangent.mapEquiv

Modified Mathlib/RingTheory/Presentation.lean

added def Algebra.Presentation.ofFinitePresentation

Created Mathlib/RingTheory/Smooth/Locus.lean

added theorem Algebra.basicOpen_subset_smoothLocus_iff

added theorem Algebra.basicOpen_subset_smoothLocus_iff_smooth

added theorem Algebra.isOpen_smoothLocus

added def Algebra.smoothLocus

added theorem Algebra.smoothLocus_comap_of_isLocalization

added theorem Algebra.smoothLocus_eq_compl_support_inter

added theorem Algebra.smoothLocus_eq_univ_iff