Front matter — conventions and terminology

FC13 — Matsumura, Commutative Ring Theory.

This chapter contains 3 conventions and 2 notations.

Of the 5 statements checked against Lean, 5 are formalized somewhere and 0 are not.

Status Statements Share What it means
in Mathlib 4 80% Mathlib states and proves it.
in lean-categories 1 20% This repository states and proves it.
checked in total 5
  • Canonical source block: FC13 Matsumura front matter, FC13-C00-U001–FC13-C00-U005, in canonical source-ID order from Foundational corpus units FC13 Matsumura. All five catalogue rows are mapped exactly once; no FC01–FC07 mapping record and no Sweep-I catalogue was modified.
  • Project-first inspection was performed at repository HEAD A=3b2239e161592472b34e02ad3b7da308f9ce7280 on Lean 4.33.0. LeanCategories/Algebra/Ideals.lean (Apache-2.0 file header) already owns the complete U002 interface: idealMapOrderHom / idealComapOrderHom are definitionally Ideal.map / Ideal.comap, with object theorems exposing the maps. This is therefore project-existing rather than a redundant Mathlib route.
  • Pinned Mathlib is P=db584cd6d46c92f209a44c0f1c829460d327499d, Apache-2.0, Lean 4.33.0 and directly project-compatible. Every Mathlib path and declaration promoted in C00 was inspected at that exact revision. The generator validation checks each cited path against the pinned checkout and checks the cited declaration token in that file.
  • Current Mathlib was refreshed on 2026-09-07 to H=f15b4f161f6ff698ab91b4494faa75925856d0f5, Apache-2.0, Lean 4.34.0-rc2. The C00 primitives CommRing, RingHom, Subring, Ideal.span, StrictMono, CharP, and Nat.Prime remain present with the same relevant interfaces; no C00 route depends on post-pin code.
  • Open Mathlib PR searches on 2026-09-07 for CommRing, Ideal.map, Ideal.span, StrictMono, and CharP found only downstream instances, corollaries, tactics, or applications relevant to these names; none supplied a distinct C00 interface that supersedes the project/P route.
  • Loogle and LeanSearch were queried through the pinned project’s LeanSearchClient; current Mathlib documentation, Lean Reservoir, and indexed GitHub Lean repositories were also searched for the C00 notions. External hits were downstream users/extensions of the Mathlib primitives, not independently owned replacements. Consequently C00 has no package-import or reference-port route.
  • Strict bundle semantics govern each row. U001 is credited only as the bundle CommRing + unital RingHom + Subring, because no one component alone states all three source conventions. U003 uses Ideal.span together with span_insert, which gives the finite sum of principal ideals by iteration. U004 records both non-strict inclusion and a genuinely strict indexed chain. U005 deliberately uses CharP R p together with Nat.Prime p; CharP alone does not imply that an arbitrary characteristic is prime.
  • Route totals for C00: mathlib 4, project-existing 1, package-import 0, reference-port 0, unmatched 0.

Convention: rings and homomorphisms

FC13-C00-U001 · Conventions and terminology, PDF p. 9 · in Mathlib

Throughout, a ring is commutative with identity; ring homomorphisms preserve 1, and subrings share the same identity.

Formalized. Mathlib/Algebra/Ring/Defs.lean::CommRing; Mathlib/Algebra/Ring/Hom/Defs.lean::RingHom; Mathlib/Algebra/Ring/Subring/Defs.lean::Subring — CommRing is the commutative ring structure with identity; RingHom is the bundled unital ring homomorphism (through its multiplicative-hom component); and the pinned Subring definition explicitly shares the ambient 0 and 1. Together these are exactly Matsumura’s standing convention.

Notation: extension and contraction of ideals

FC13-C00-U002 · Conventions and terminology, PDF p. 9 · in lean-categories

For f:A→B and J⊲B, write A∩J=f⁻¹(J); for I⊲A, write IB=f(I)B.

Formalized. LeanCategories/Algebra/Ideals.lean::LeanCategories.Algebra.idealMapOrderHom, LeanCategories.Algebra.idealComapOrderHom, LeanCategories.Algebra.idealMapFunctor_obj, LeanCategories.Algebra.idealComapFunctor_obj — At project HEAD, extension along f : A →+* B is definitionally Ideal.map f I and contraction is Ideal.comap f J; the object theorems expose those equalities. Pinned Mathlib defines Ideal.map as the ideal span of the image and Ideal.comap as the preimage, so this project-owned pair is exactly the source IB=f(I)B / f⁻¹(J) notation semantics.

Searched: A=3b2239e161592472b34e02ad3b7da308f9ce7280

Notation: generated ideals

FC13-C00-U003 · Conventions and terminology, PDF p. 9 · in Mathlib

The ideal generated by a₁,…,aₙ may be written ΣaᵢA or (a₁,…,aₙ).

Formalized. Mathlib/RingTheory/Ideal/Span.lean::Ideal.span, Ideal.span_insert — Ideal.span s is explicitly the ideal generated by a subset s; Ideal.span_insert identifies adjoining one generator with the join of the corresponding principal ideal and the previous span. Iterating over a finite generator set gives exactly the source ideal (a₁,…,aₙ)=Σ aᵢA.

Convention: inclusion and chains

FC13-C00-U004 · Conventions and terminology, PDF p. 9 · in Mathlib

The inclusion symbol permits equality; an “ascending chain” M₁⊂M₂⊂⋯ is intended to be strictly increasing unless stated otherwise.

Formalized. Mathlib/Data/Set/Defs.lean::Set.Subset; Mathlib/Order/Monotone/Defs.lean::StrictMono — Set.Subset (and the induced subobject order ≤) is non-strict and therefore permits equality, while StrictMono f requires a<b → f a<f b. Thus a module/ideal chain represented by a strictly monotone indexed family has exactly the source “ascending chain means strictly increasing” convention.

Convention: positive characteristic

FC13-C00-U005 · Conventions and terminology, PDF p. 9 · in Mathlib

Writing char R=p means p>0 is a prime number.

Formalized. Mathlib/Algebra/CharP/Defs.lean::CharP; Mathlib/Data/Nat/Prime/Defs.lean::Nat.Prime — CharP R p records that the characteristic is p; the additional hypothesis Nat.Prime p says p≥2, hence positive and prime. The conjunction, rather than CharP alone, exactly represents Matsumura’s convention when the symbol p is used for positive characteristic.