Commit 2024-07-01 08:43 58877dec

View on Github →

feat(RingTheory): presentations of algebras (#14271) Adds basic API for presentations of algebras and constructors for localization and base change. This contribution was created as part of the AIM workshop "Formalizing algebraic geometry" in June 2024.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/RingTheory/Generators.lean

added def Algebra.Generators.baseChange

added theorem Algebra.Generators.ker_eq_ker_aeval_val

added def Algebra.Generators.localizationAway

Modified Mathlib/RingTheory/Localization/Away/Basic.lean

added theorem IsLocalization.Away.sec_spec

Modified Mathlib/RingTheory/Localization/Basic.lean

added theorem IsLocalization.mk'_pow

Modified Mathlib/RingTheory/MvPolynomial/Localization.lean

added def IsLocalization.Away.auxHom

added def IsLocalization.Away.auxInv

added theorem IsLocalization.Away.mvPolynomialQuotientEquiv_apply

Created Mathlib/RingTheory/Presentation.lean

added theorem Algebra.Presentation.aeval_val_relation

added def Algebra.Presentation.baseChange

added theorem Algebra.Presentation.finitePresentation_of_isFinite

added theorem Algebra.Presentation.ideal_fg_of_isFinite

added theorem Algebra.Presentation.localizationAway_dimension_zero

added def Algebra.Presentation.quotientEquiv

added theorem Algebra.Presentation.quotientEquiv_mk

added theorem Algebra.Presentation.quotientEquiv_symm

added structure Algebra.Presentation