Atiyah and Macdonald definition catalogue

Title: Introduction to Commutative Algebra

Authors: M. F. Atiyah and I. G. Macdonald

Zotero key: XL7FDEDH

Citekey: AM18

Source attachment: local-write-api-1783448143508-XL7FDEDH_extracted.md

Chapter 1. Rings and Ideals

• Ring — Rings and ring homomorphisms, p. 1
  • Mathlib: Ring — Mathlib/Algebra/Ring/Defs.lean
• Zero ring — Rings and ring homomorphisms, p. 1
  • Lean core: Subsingleton R for a ring R — Init/Prelude.lean
• Ring homomorphism — Rings and ring homomorphisms, p. 2
  • Mathlib: RingHom — Mathlib/Algebra/Ring/Hom/Defs.lean
• Subring — Rings and ring homomorphisms, p. 2
  • Mathlib: Subring — Mathlib/Algebra/Ring/Subring/Defs.lean
• Ideal — Ideals. Quotient rings, p. 2
  • Mathlib: Ideal — Mathlib/RingTheory/Ideal/Defs.lean
• Quotient ring — Ideals. Quotient rings, p. 2
  • Mathlib: Ideal.Quotient — Mathlib/RingTheory/Ideal/Quotient/Defs.lean:43
• Residue-class ring — Ideals. Quotient rings, p. 2
  • Mathlib: Ideal.Quotient — Mathlib/RingTheory/Ideal/Quotient/Defs.lean:43
• Kernel of a ring homomorphism — Ideals. Quotient rings, p. 2
  • Mathlib: RingHom.ker — Mathlib/RingTheory/Ideal/Maps.lean:740
• Image of a ring homomorphism — Ideals. Quotient rings, p. 2
  • Mathlib: RingHom.range — Mathlib/Algebra/Ring/Subring/Basic.lean:241
• Zero-divisor — Zero-divisors. Nilpotent elements. Units, p. 2
  • Mathlib: notMem_nonZeroDivisors_iff — Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean
• Nilpotent element — Zero-divisors. Nilpotent elements. Units, p. 2
  • Mathlib: IsNilpotent — Mathlib/RingTheory/Nilpotent/Basic.lean
• Unit — Zero-divisors. Nilpotent elements. Units, p. 2
  • Mathlib: IsUnit — Mathlib/Algebra/Group/Units/Defs.lean:364
• Integral domain — Zero-divisors. Nilpotent elements. Units, p. 2
  • Mathlib: IsDomain — Mathlib/Algebra/Ring/Defs.lean:439
• Principal ideal — Zero-divisors. Nilpotent elements. Units, p. 3
  • Mathlib: Ideal.span — Mathlib/RingTheory/Ideal/Operations.lean
• Field — Zero-divisors. Nilpotent elements. Units, p. 3
  • Mathlib: Field — Mathlib/Algebra/Field/Defs.lean
• Prime ideal — Prime ideals and maximal ideals, p. 3
  • Mathlib: Ideal.IsPrime — Mathlib/RingTheory/Ideal/Prime.lean
• Maximal ideal — Prime ideals and maximal ideals, p. 3
  • Mathlib: Ideal.IsMaximal — Mathlib/RingTheory/Ideal/Operations.lean
• Local ring — Prime ideals and maximal ideals, p. 4
  • Mathlib: IsLocalRing — Mathlib/RingTheory/LocalRing/Basic.lean
• Residue field — Prime ideals and maximal ideals, p. 4
  • Mathlib: Ideal.ResidueField — Mathlib/RingTheory/LocalRing/ResidueField/Basic.lean
• Semi-local ring — Prime ideals and maximal ideals, p. 4
  • Mathlib: Finite (MaximalSpectrum R) — Mathlib/RingTheory/LocalProperties/Semilocal.lean
• Nilradical — Nilradical and Jacobson radical, p. 5
  • Mathlib: nilradical — Mathlib/RingTheory/Nilpotent/Lemmas.lean
• Jacobson radical — Nilradical and Jacobson radical, p. 5
  • Mathlib: Ring.jacobson — Mathlib/RingTheory/LocalRing/MaximalIdeal/Basic.lean
• Radical of an ideal — Nilradical and Jacobson radical, p. 5
  • Mathlib: Ideal.radical — Mathlib/RingTheory/Ideal/Operations.lean:799
• Sum of ideals — Operations on ideals, p. 6
  • Mathlib: Ideal.add — Mathlib/RingTheory/Ideal/Operations.lean
• Intersection of ideals — Operations on ideals, p. 6
  • Mathlib: Ideal.inf — Mathlib/RingTheory/Ideal/Operations.lean
• Product of ideals — Operations on ideals, p. 6
  • Mathlib: Ideal.mul — Mathlib/RingTheory/Ideal/Operations.lean
• Coprime ideals — Operations on ideals, p. 7
  • Mathlib: IsCoprime — Mathlib/RingTheory/Coprime/Basic.lean
• Annihilator ideal — Operations on ideals, p. 8
  • Mathlib: Ideal.annihilator — Mathlib/RingTheory/Ideal/Operations.lean
• Quotient of ideals — Operations on ideals, p. 8
  • Mathlib: Ideal.quotient — Mathlib/RingTheory/Ideal/Operations.lean
• Extension of an ideal — Extension and contraction, p. 9
  • Mathlib: Ideal.map — Mathlib/RingTheory/Ideal/Operations.lean
• Contraction of an ideal — Extension and contraction, p. 9
  • Mathlib: Ideal.comap — Mathlib/RingTheory/Ideal/Operations.lean

Chapter 2. Modules

• Module — Modules and module homomorphisms, p. 17
  • Mathlib: Module — Mathlib/Algebra/Module/Defs.lean
• Module homomorphism — Modules and module homomorphisms, p. 18
  • Mathlib: LinearMap — Mathlib/Algebra/Module/LinearMap/Defs.lean:85
• Kernel of a module homomorphism — Modules and module homomorphisms, p. 18
  • Mathlib: LinearMap.ker — Mathlib/Algebra/Module/Submodule/Ker.lean:60
• Submodule — Submodules and quotient modules, p. 18
  • Mathlib: Submodule — Mathlib/Algebra/Module/Submodule/Defs.lean
• Quotient module — Submodules and quotient modules, p. 18
  • Mathlib: Submodule.Quotient — Mathlib/Algebra/Module/Submodule/Basic.lean
• Sum of submodules — Operations on submodules, p. 19
  • Mathlib: Submodule.sup — Mathlib/Algebra/Module/Submodule/Lattice.lean:197 (⊔ is an operation of the CompleteLattice instance; no standalone def)
• Intersection of submodules — Operations on submodules, p. 19
  • Mathlib: Submodule.inf — Mathlib/Algebra/Module/Submodule/Lattice.lean:197 (⊓ is an operation of the CompleteLattice instance; no standalone def)
• Product of modules — Operations on submodules, p. 19
  • Mathlib: Pi.module — Mathlib/Algebra/Module/Pi.lean
• Direct sum of modules — Direct sum and product, p. 20
  • Mathlib: DirectSum — Mathlib/Algebra/DirectSum/Basic.lean
• Direct product of modules — Direct sum and product, p. 20
  • Mathlib: Pi.module — Mathlib/Algebra/Module/Pi.lean
• Faithful module — Direct sum and product, p. 20
  • Mathlib: FaithfulSMul — Mathlib/Algebra/Module/Defs.lean
• Generating set of a module — Finitely generated modules, p. 20
  • Mathlib: Submodule.span — Mathlib/LinearAlgebra/Span/Defs.lean:48
• Finitely generated module — Finitely generated modules, p. 20
  • Mathlib: Module.Finite — Mathlib/RingTheory/Finiteness/Defs.lean
• Free module — Finitely generated modules, p. 21
  • Mathlib: Module.Free — Mathlib/LinearAlgebra/FreeModule/Basic.lean
• Exact sequence — Exact sequences, p. 22
  • Mathlib: Function.Exact — Mathlib/Algebra/Exact/Basic.lean
• Tensor product of modules — Tensor product of modules, p. 24
  • Mathlib: TensorProduct — Mathlib/LinearAlgebra/TensorProduct/Defs.lean
• Restriction of scalars — Restriction and extension of scalars, p. 27
  • Mathlib: ModuleCat.restrictScalars — Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean
• Extension of scalars — Restriction and extension of scalars, p. 27
  • Mathlib: ModuleCat.extendScalars — Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean
• Flat module — Exactness properties of the tensor product, p. 29
  • Mathlib: Module.Flat — Mathlib/RingTheory/Flat/Basic.lean
• Faithfully flat module — Exactness properties of the tensor product, p. 29
  • Mathlib: Module.FaithfullyFlat — Mathlib/RingTheory/Flat/FaithfullyFlat/Basic.lean
• Algebra over a ring — Algebras, pp. 29–30
  • Mathlib: Algebra — Mathlib/Algebra/Algebra/Basic.lean
• Algebra homomorphism — Algebras, p. 30
  • Mathlib: AlgHom — Mathlib/Algebra/Algebra/Basic.lean
• Finite algebra — Algebras, p. 30
  • Mathlib: Algebra.Finite — Mathlib/RingTheory/Finiteness/Defs.lean
• Algebra of finite type — Algebras, p. 30
  • Mathlib: Algebra.FiniteType — Mathlib/RingTheory/Finiteness/Defs.lean
• Tensor product of algebras — Tensor product of algebras, p. 30
  • Mathlib: Algebra.TensorProduct — Mathlib/RingTheory/TensorProduct/Basic.lean

Chapter 3. Rings and Modules of Fractions

• Multiplicatively closed set — Rings and modules of fractions, p. 36
  • Mathlib: Submonoid — Mathlib/Algebra/Group/Submonoid/Defs.lean
• Ring of fractions — Rings and modules of fractions, p. 36
  • Mathlib: Localization — Mathlib/RingTheory/Localization/Basic.lean
• Localization of a ring — Rings and modules of fractions, pp. 36–39
  • Mathlib: Localization — Mathlib/RingTheory/Localization/Basic.lean
• Module of fractions — Rings and modules of fractions, pp. 36–39
  • Mathlib: LocalizedModule — Mathlib/RingTheory/Localization/Module.lean
• Localization of a module — Rings and modules of fractions, pp. 36–39
  • Mathlib: LocalizedModule — Mathlib/RingTheory/Localization/Module.lean
• Local property — Local properties, p. 40
  • Mathlib: RingHom.PropertyIsLocal — Mathlib/RingTheory/LocalProperties/Basic.lean
• Extended ideal in a ring of fractions — Extended and contracted ideals in rings of fractions, p. 41
  • Mathlib: Ideal.map — Mathlib/RingTheory/Localization/Ideal.lean
• Contracted ideal in a ring of fractions — Extended and contracted ideals in rings of fractions, p. 41
  • Mathlib: Ideal.comap — Mathlib/RingTheory/Localization/Ideal.lean

Chapter 4. Primary Decomposition

• Primary ideal — Primary Decomposition, p. 50
  • Mathlib: Ideal.IsPrimary — Mathlib/RingTheory/Ideal/IsPrimary.lean
• Primary decomposition — Primary Decomposition, p. 51
  • Mathlib: Ideal.IsMinimalPrimaryDecomposition — Mathlib/RingTheory/Lasker.lean
• Minimal primary decomposition — Primary Decomposition, pp. 51–52
  • Mathlib: Ideal.IsMinimalPrimaryDecomposition — Mathlib/RingTheory/Lasker.lean
• Prime ideal associated with a primary decomposition — Primary Decomposition, p. 52
  • Mathlib: IsMinimalPrimaryDecomposition.image_radical_eq_associated_primes — Mathlib/RingTheory/Lasker.lean
• Isolated prime ideal — Primary Decomposition, p. 52
  • LeanCategories: LeanCategories.Algebra.Ideal.isolatedPrime — LeanCategories/Algebra/AtiyahMacdonald/PrimaryDecomposition.lean
• Embedded prime ideal — Primary Decomposition, p. 52
  • LeanCategories: LeanCategories.Algebra.Ideal.embeddedPrime — LeanCategories/Algebra/AtiyahMacdonald/PrimaryDecomposition.lean

Chapter 5. Integral Dependence and Valuations

• Element integral over a ring — Integral dependence, p. 59
  • Mathlib: IsIntegral — Mathlib/RingTheory/IntegralClosure/IsIntegral/Defs.lean:53
• Integral algebra — Integral dependence, p. 60
  • Mathlib: Algebra.IsIntegral — Mathlib/RingTheory/IntegralClosure/Algebra/Defs.lean:36
• Integral closure — Integral dependence, p. 60
  • Mathlib: integralClosure — Mathlib/RingTheory/IntegralClosure/Algebra/Basic.lean:215
• Integrally closed integral domain — Integrally closed integral domains. The going-down theorem, p. 60
  • Mathlib: IsIntegrallyClosed — Mathlib/RingTheory/IntegralClosure/IntegrallyClosed.lean:74
• Valuation ring — Valuation rings, p. 65
  • Mathlib: ValuationSubring — Mathlib/RingTheory/Valuation/ValuationSubring.lean

Chapter 6. Chain Conditions

• Chain of submodules — Chain Conditions, p. 74
  • Mathlib: RelSeries — Mathlib/Order/RelSeries.lean
• Ascending chain condition — Chain Conditions, p. 74
  • Mathlib: IsNoetherian — Mathlib/RingTheory/Noetherian/Basic.lean
• Descending chain condition — Chain Conditions, p. 74
  • Mathlib: IsArtinian — Mathlib/RingTheory/Artinian/Defs.lean
• Noetherian module — Chain Conditions, p. 74
  • Mathlib: IsNoetherian — Mathlib/RingTheory/Noetherian/Basic.lean
• Artinian module — Chain Conditions, p. 74
  • Mathlib: IsArtinian — Mathlib/RingTheory/Artinian/Defs.lean
• Composition series — Chain Conditions, p. 76
  • Mathlib: CompositionSeries — Mathlib/Order/JordanHolder.lean:137
• Length of a module — Chain Conditions, p. 76
  • Mathlib: Module.length — Mathlib/RingTheory/Length.lean
• Noetherian ring — Chain Conditions, p. 76
  • Mathlib: IsNoetherianRing — Mathlib/RingTheory/Noetherian/Basic.lean
• Artinian ring — Chain Conditions, p. 76
  • Mathlib: IsArtinianRing — Mathlib/RingTheory/Artinian/Ring.lean

Chapter 7. Noetherian Rings

Chapter 8. Artin Rings

• Dimension of a ring — Artin Rings, p. 90
  • Mathlib: ringKrullDim — Mathlib/RingTheory/KrullDimension/Basic.lean

Chapter 9. Discrete Valuation Rings and Dedekind Domains

• Discrete valuation ring — Discrete valuation rings, p. 94
  • Mathlib: IsDiscreteValuationRing — Mathlib/RingTheory/DiscreteValuationRing/Basic.lean
• Dedekind domain — Dedekind domains, p. 95
  • Mathlib: IsDedekindDomain — Mathlib/RingTheory/DedekindDomain/Basic.lean
• Fractional ideal — Fractional ideals, p. 96
  • Mathlib: FractionalIdeal — Mathlib/RingTheory/FractionalIdeal/Basic.lean
• Invertible fractional ideal — Fractional ideals, p. 96
  • Mathlib: FractionalIdeal.IsUnit — Mathlib/RingTheory/FractionalIdeal/Basic.lean

Chapter 10. Completions

• Topological ring — Topologies and completions, pp. 101–102
  • Mathlib: TopologicalSpace — Mathlib/Topology/Algebra/Ring/Basic.lean
• Completion — Topologies and completions, p. 102
  • Mathlib: AdicCompletion — Mathlib/RingTheory/AdicCompletion/Basic.lean
• Inverse limit — Topologies and completions, p. 103
  • Mathlib: CategoryTheory.Limits.limit — Mathlib/CategoryTheory/Limits/HasLimits.lean
• Filtration of a ring — Filtrations, p. 105
  • Mathlib: Filtration — Mathlib/RingTheory/Filtration.lean
• Filtration of a module — Filtrations, p. 105
  • Mathlib: Filtration — Mathlib/RingTheory/Filtration.lean
• Adic topology — Filtrations, p. 105
  • Mathlib: adicTopology — Mathlib/RingTheory/AdicCompletion/Basic.lean
• Graded ring — Graded rings and modules, p. 106
  • Mathlib: GradedAlgebra — Mathlib/RingTheory/GradedAlgebra/Basic.lean
• Graded module — Graded rings and modules, p. 106
  • Mathlib: GradedModule — Mathlib/Algebra/Module/GradedModule.lean
• Associated graded ring — The associated graded ring, p. 111
  • Mathlib: associatedGraded — Mathlib/RingTheory/Filtration.lean
• Associated graded module — The associated graded ring, pp. 111–112
  • Mathlib: associatedGraded — Mathlib/RingTheory/Filtration.lean
• Zariski ring — The associated graded ring, p. 114
  • Mathlib: IsZariskiRing — Mathlib/RingTheory/Filtration.lean

Chapter 11. Dimension Theory

• Poincaré series — Hilbert functions, p. 116
  • LeanCategories: LeanCategories.Algebra.PoincareSeries — LeanCategories/Algebra/DimensionTheory.lean
• Hilbert function — Hilbert functions, p. 118
  • Mathlib: hilbertFunction — Mathlib/RingTheory/Polynomial/HilbertPoly.lean:110 (as hilbertPoly)
• Dimension of a Noetherian local ring — Dimension theory of Noetherian local rings, p. 119
  • Mathlib: ringKrullDim — Mathlib/RingTheory/KrullDimension/Basic.lean
• Height of a prime ideal — Dimension theory of Noetherian local rings, p. 120
  • Mathlib: Ideal.height — Mathlib/RingTheory/Ideal/Height.lean
• System of parameters — Dimension theory of Noetherian local rings, p. 122
  • LeanCategories: LeanCategories.Algebra.IsSystemOfParameters — LeanCategories/Algebra/DimensionTheory.lean
• Regular local ring — Regular local rings, p. 123
  • Mathlib: IsRegularLocalRing — Mathlib/RingTheory/RegularLocalRing/Defs.lean
• Field of rational functions of an affine variety — Transcendental dimension, p. 124
  • Mathlib: FractionRing — Mathlib/RingTheory/FractionalIdeal/Basic.lean
• Dimension of an affine variety — Transcendental dimension, p. 124
  • Mathlib: ringKrullDim — Mathlib/RingTheory/KrullDimension/Basic.lean
• Local dimension of a variety at a point — Transcendental dimension, p. 124
  • Mathlib: AlgebraicGeometry.ringKrullDim_stalk_eq_coheight — Mathlib/AlgebraicGeometry/Properties.lean