Chapter 1. Rings and Ideals (pp. 1–9)
FC04 — Atiyah & Macdonald, Introduction to Commutative Algebra.
This chapter contains 25 definitions, 1 theorem, 12 propositions, 2 corollaries, 10 constructions, 2 conventions, 1 notation and 6 other statements.
Of the 59 statements checked against Lean, 53 are formalized somewhere and 6 are not.
| Status | Statements | Share | What it means |
|---|---|---|---|
| in Mathlib | 53 | 90% | Mathlib states and proves it. |
| not formalized | 6 | 10% | A documented search found no Lean statement of it anywhere. |
| checked in total | 59 |
- Project search:
LeanCategories/**outside.lake/.agents/.gitwas searched first for the ring, ideal, quotient, local-ring, radical, Chinese-remainder, and extension/contraction material in this chapter. The project uses the Mathlib algebraic interfaces downstream but does not own a source-shaped replacement for these C01 units. - Pinned Mathlib: project pin
db584cd6d46c92f209a44c0f1c829460d327499d(Apache-2.0, Lean v4.33.0), denotedP, was checked declaration-wise. It contains the foundational commutative-ring/ideal API and the theorem-level realizations cited below. - Current/open Mathlib: upstream
29ea5de9cb981cb62dfa7979aaff0851f50c603a(Apache-2.0, Lean v4.34.0-rc2), denotedH, was refreshed 2026-09-06. Targeted current-tree and open-work searches found no post-pin owner for the six negative source bundles below. - External search: targeted GitHub/Reservoir and indexed Lean search was used for the strict negative boundaries, including maximal-ideal contraction, the multivariable-polynomial examples, arbitrary-subset radicals, radicals of annihilators, coprime radicals, and Gaussian-prime ideal splitting. Searches found only generic/partial ingredients or mirrors/forks of Mathlib, not declarations realizing those complete source units.
Ndenotes dated 2026-09-06 negative evidence after project-first search, pinned/current Mathlib, relevant open work, and external indexed search. A bundled source row is not credited merely because some of its clauses can be reconstructed from generic infrastructure.
Definition: Ring
A set with addition and multiplication satisfying the abelian-group, associative/distributive, commutative, and identity axioms.
Formalized. Mathlib/Algebra/Ring/Defs.lean::CommRing — Mathlib’s CommRing is a commutative unital ring; as in Atiyah–Macdonald, the degenerate one-element ring is permitted unless Nontrivial is separately assumed.
Convention: “Ring” convention
Throughout FC04, rings are commutative and have identity.
Formalized. Mathlib/Algebra/Ring/Hom/Defs.lean::RingHom — RingHom preserves 0, 1, addition, and multiplication, exactly the source convention for ring homomorphisms.
Definition: Zero ring
The permitted case 1=0, hence the one-element ring, denoted 0.
Formalized. Mathlib/Algebra/Ring/Subring/Defs.lean::Subring — A Subring is a subset closed under the ring operations and containing 1, with inherited structure.
Definition: Ring homomorphism
Map preserving addition, multiplication, and 1.
Formalized. Mathlib/RingTheory/Ideal/Defs.lean::Ideal — Ideal R is the additive submodule of R over itself, hence exactly an additive subgroup closed under multiplication by arbitrary ring elements.
Definition: Subring
Subset closed under addition and multiplication and containing the identity of the ambient ring.
Formalized. Ideal; Submodule.add_mem; Submodule.neg_mem; Submodule.smul_mem — The bundled closure fields give the stated additive-subgroup-plus-absorption criterion for ideals.
Definition: Ideal
Additive subgroup 𝔞⊆A satisfying A𝔞⊆𝔞.
Formalized. Mathlib/RingTheory/Ideal/Span.lean::Ideal.span; Ideal.subset_span; Ideal.span_le — span S is the least ideal containing S, with the universal property used by the source.
Construction / definition: Quotient (residue-class) ring A/𝔞
Cosets of an ideal with multiplication induced from A.
Formalized. Ideal.span ({x} : Set R); Ideal.mem_span_singleton; Ideal.span_singleton_mul_span_singleton — Singleton span is the principal ideal (x) and its membership API is divisibility by x.
Construction: Canonical quotient homomorphism A→A/𝔞
x↦x+𝔞; a surjective ring homomorphism.
Formalized. Mathlib/RingTheory/Ideal/Quotient/Basic.lean::Ideal.Quotient; Ideal.Quotient.mk — The quotient ring and canonical map are exactly R/I by the ideal congruence.
Proposition 1.1: Ideal correspondence for a quotient
Ideals of A containing 𝔞 correspond order-preservingly to ideals of A/𝔞 by inverse image.
Formalized. Mathlib/RingTheory/Ideal/Maps.lean::Ideal.relIsoOfSurjective; Ideal.Quotient.mk_surjective; Ideal.Quotient.mk_ker — Applying the surjective correspondence order-isomorphism to R → R/I identifies ideals of the quotient with ideals of R containing I.
Construction / comparison: Kernel, image, and first isomorphism for ring homomorphisms
For f:A→B, ker f is an ideal, f(A) a subring, and A/ker f≅f(A).
Formalized. Mathlib/RingTheory/Ideal/Quotient/Operations.lean::RingHom.quotientKerEquivRange — This is the first isomorphism theorem R/ker f ≃+* range f.
Notation: Congruence modulo an ideal
x≡y (mod 𝔞) means x−y∈𝔞.
Formalized. Mathlib/Algebra/GroupWithZero/Basic.lean::subsingleton_iff_zero_eq_one; subsingleton_of_zero_eq_one — A commutative ring is the zero ring exactly when it is subsingleton, equivalently 0 = 1; no global nontriviality assumption is built into CommRing.
Definition: Zero-divisor
x is a zero-divisor if xy=0 for some y≠0.
Formalized. Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean::nonZeroDivisors; notMem_nonZeroDivisors_iff_left — The complement of nonZeroDivisors is exactly the elements annihilating some nonzero element; in a nontrivial ring this includes 0, matching the source convention.
Definition: Integral domain
Nonzero ring with no nonzero zero-divisors.
Formalized. Mathlib/Algebra/Ring/Defs.lean::IsDomain — IsDomain R combines nontriviality with the no-zero-divisors property, exactly the integral-domain definition.
Definition: Nilpotent element
x is nilpotent if x^n=0 for some n>0.
Formalized. Mathlib/Algebra/GroupWithZero/Defs.lean::mul_left_cancel₀; mul_right_cancel₀ — In a domain, multiplication by a nonzero element cancels on either side.
Definition: Unit and inverse
x is a unit if xy=1 for some y; y is unique and written x⁻¹.
Formalized. Mathlib/Algebra/GroupWithZero/Defs.lean::IsNilpotent — IsNilpotent x means x^n = 0 for some positive exponent (with the standard equivalent encoding used by Mathlib).
Definition / notation: Principal ideal
The ideal of multiples ax of x, denoted (x) or Ax.
Formalized. IsNilpotent (I : Ideal R); Mathlib/RingTheory/Nilpotent/Lemmas.lean::mem_nilradical — Ideals themselves carry multiplication, so IsNilpotent I is I^n=0; the condition that every element of I is nilpotent is equivalently I ≤ nilradical R via mem_nilradical.
Convention: Zero ideal notation
The ideal (0) is usually denoted 0.
Formalized. Mathlib/Algebra/Group/Units/Defs.lean::IsUnit — IsUnit x means x is represented by a unit, equivalently admits a multiplicative inverse in the commutative ring.
Definition: Field
A nonzero ring in which every nonzero element is a unit.
Formalized. Mathlib/RingTheory/Ideal/Span.lean::Ideal.span_singleton_eq_top — (x)=R ↔︎ IsUnit x is exactly the source characterization.
Proposition 1.2: Characterizations of a field
For A≠0: A is a field iff its only ideals are 0,(1) iff every homomorphism A→B to B≠0 is injective.
Formalized. Mathlib/Algebra/Field/Defs.lean::Field — Field is the nontrivial commutative ring structure in which every nonzero element is invertible.
Definition: Prime ideal
𝔭≠(1) and xy∈𝔭 implies x∈𝔭 or y∈𝔭.
Formalized. Mathlib/RingTheory/Ideal/Basic.lean::Ring.isField_iff_isSimpleOrder_ideal; RingHom.injective_iff_ker_eq_bot; field-source RingHom.injective — The ideal lattice is simple exactly for a field; a homomorphism is injective exactly when its kernel is zero, and a homomorphism from a field to a nontrivial ring has zero kernel, yielding the source’s three equivalent criteria.
Definition: Maximal ideal
𝔪≠(1) with no ideal strictly between 𝔪 and (1).
Formalized. Mathlib/RingTheory/Ideal/Maximal.lean::Ideal.IsMaximal; Ideal.isMaximal_iff — This is maximality among proper ideals under inclusion.
Comparison: Prime/maximal ideals via quotients
𝔭 prime iff A/𝔭 is a domain; 𝔪 maximal iff A/𝔪 is a field.
Formalized. Mathlib/RingTheory/Ideal/Quotient/Basic.lean::Ideal.Quotient.isDomain_iff_prime; Ideal.Quotient.maximal_ideal_iff_isField_quotient — The quotient is a domain exactly when the ideal is prime, and a field exactly when it is maximal.
Comparison: Maximal ideals are prime; 0 prime iff domain
Every maximal ideal is prime; the zero ideal is prime exactly for integral domains.
Formalized. Mathlib/RingTheory/Ideal/Maximal.lean::Ideal.IsMaximal.isPrime; Mathlib/RingTheory/Ideal/Prime.lean::Ideal.isPrime_bot — Maximal ideals are prime, and the zero ideal is prime precisely in the domain setting.
Construction / comparison: Contraction preserves prime ideals
For f:A→B and prime 𝔮⊂B, f⁻¹(𝔮) is prime; maximality need not contract (example Z→Q).
Not formalized. partial: Mathlib/RingTheory/Ideal/Maps.lean::Ideal.IsPrime.comap — Prime contraction is pinned, but no checked declaration realizes the source’s accompanying failure of maximal contraction via the concrete inclusion ℤ → ℚ; current Mathlib and targeted GitHub search still expose only the general prime-comap theorem and unrelated ideal-contraction examples.
Searched: N
Theorem 1.3 / order-theory convention: Existence of maximal ideals
Every nonzero ring has a maximal ideal. The source footnote defines a chain in a poset as a totally ordered subset and states the Zorn criterion used in the proof.
Formalized. Mathlib/RingTheory/Ideal/Maximal.lean::Ideal.exists_maximal — This is the Zorn-lemma existence of a maximal ideal in a nontrivial commutative ring.
Corollary 1.4: Proper ideals lie in maximal ideals
Every ideal 𝔞≠(1) is contained in a maximal ideal.
Formalized. Mathlib/RingTheory/Ideal/Maximal.lean::Ideal.exists_le_maximal — Every proper ideal is contained in a maximal ideal.
Corollary 1.5: Non-units lie in maximal ideals
Every non-unit belongs to a maximal ideal.
Formalized. Mathlib/RingTheory/Ideal/Nonunits.lean::exists_max_ideal_of_mem_nonunits; coe_subset_nonunits — Every nonunit lies in a maximal ideal, while every proper ideal consists only of nonunits; together these identify the nonunits with the union of maximal ideals.
Definition: Local ring
A ring with exactly one maximal ideal 𝔪.
Formalized. Mathlib/RingTheory/LocalRing/Defs.lean::IsLocalRing; Mathlib/RingTheory/LocalRing/Basic.lean::IsLocalRing.of_unique_max_ideal; Mathlib/RingTheory/LocalRing/MaximalIdeal/Basic.lean::IsLocalRing.maximal_ideal_unique; IsLocalRing.of_nonunits_add — Mathlib proves equivalence between the local-ring unit criterion, a unique maximal ideal, and additive closure of the nonunits.
Definition: Residue field of a local ring
For local (A,𝔪), the field k=A/𝔪.
Formalized. Mathlib/RingTheory/LocalRing/ResidueField/Basic.lean::IsLocalRing.ResidueField; IsLocalRing.residue — The residue field is the quotient by the unique maximal ideal, with its canonical residue map.
Proposition 1.6: Criteria for local rings
- If every element outside 𝔪 is a unit then 𝔪 is the unique maximal ideal; (ii) if 𝔪 maximal and every element of 1+𝔪 is a unit then A is local.
Formalized. IsLocalRing.isUnit_or_isUnit_of_add_one; Mathlib/RingTheory/LocalRing/Basic.lean::IsLocalRing.isUnit_or_isUnit_one_sub_self — If a+b=1, one summand is a unit; equivalently a nonunit a forces 1-a to be a unit.
Definition: Semi-local ring
A ring with finitely many maximal ideals.
Formalized. [Finite (MaximalSpectrum R)] as used throughout Mathlib/RingTheory/LocalProperties/Semilocal.lean — Mathlib’s semilocal hypotheses are exactly finiteness of the maximal spectrum, i.e. finitely many maximal ideals.
Reusable examples: Prime and maximal ideals in polynomial rings and Z
Irreducible f in k[x₁,…,xₙ] gives prime (f); in Z, (p) is maximal for prime p; the zero-constant-term ideal in k[x₁,…,xₙ] is maximal and for n>1 nonprincipal.
Not formalized. partial: polynomial/MvPolynomial ideal, irreducibility, maximality, and principal-ideal APIs — P/H formalize many individual ingredients, but no checked declaration realizes the complete source bundle, in particular the zero-constant-term maximal ideal of k[x₁,…,xₙ] together with its nonprincipality for n>1. Targeted GitHub search found no external Lean owner.
Searched: N
Definition / comparison: Principal ideal domain
An integral domain in which every ideal is principal; every nonzero prime ideal in a PID is maximal.
Formalized. Mathlib/RingTheory/PrincipalIdealDomain.lean::IsPrincipalIdealRing; IsPrime.to_maximal_ideal — A PID is a domain whose ideals are principal, and every nonzero prime ideal in such a ring is maximal.
Proposition 1.7: Nilpotents form an ideal
Nilpotent elements form an ideal 𝔑, and A/𝔑 has no nonzero nilpotent.
Formalized. Mathlib/RingTheory/Nilpotent/Lemmas.lean::nilradical; mem_nilradical; nilradical_eq_bot_iff; Mathlib/RingTheory/Ideal/Quotient/Nilpotent.lean::Ideal.isRadical_iff_quotient_reduced — The nilpotent elements form nilradical R; quotienting by this radical ideal is reduced, matching the source construction.
Definition: Nilradical
The ideal 𝔑 of all nilpotent elements.
Formalized. Mathlib/RingTheory/Nilpotent/Lemmas.lean::nilradical; mem_nilradical — mem_nilradical identifies the nilradical with the nilpotent elements, and Mathlib’s ideal radical specializes at ⊥ to the same ideal.
Proposition 1.8: Nilradical as intersection of primes
𝔑 is the intersection of all prime ideals of A.
Formalized. Mathlib/RingTheory/Nilpotent/Lemmas.lean::nilradical_eq_sInf — The nilradical is exactly the infimum/intersection of all prime ideals.
Definition: Jacobson radical
Intersection of all maximal ideals of A, denoted ℜ.
Formalized. Mathlib/RingTheory/Jacobson/Ideal.lean::Ideal.jacobson; Ideal.jacobson_bot — Ideal.jacobson ⊥ is the intersection of all maximal ideals, exactly the Jacobson radical of the ring.
Proposition 1.9: Unit characterization of the Jacobson radical
x∈ℜ iff 1−xy is a unit for every y∈A.
Formalized. Mathlib/RingTheory/Jacobson/Ideal.lean::Ideal.mem_jacobson_bot — Mathlib characterizes Jacobson-radical membership by unitness of 1+xy for all y; replacing y by -y is exactly 1-xy in the source.
Construction / definition: Sum of ideals
𝔞+𝔟 consists of x+y; arbitrary sums are finite-support sums and are the smallest ideal containing the family.
Formalized. Mathlib/RingTheory/Ideal/Operations.lean::Ideal.add_eq_sup; Mathlib/RingTheory/Ideal/Span.lean::Ideal.iSup_eq_span; Ideal.span_iUnion — Binary ideal sum is lattice supremum, and arbitrary sums are the least ideal containing the union.
Construction / comparison: Intersections and complete lattice of ideals
Arbitrary intersections are ideals; ideals form a complete lattice under inclusion.
Formalized. complete-lattice instance on Ideal R; Ideal.mem_iInf; Ideal.mem_sInf — Arbitrary intersections are ideals and Ideal R is a complete lattice under inclusion.
Construction / convention: Product and powers of ideals
𝔞𝔟 is generated by products xy; finite products and powers are defined, with 𝔞⁰=(1).
Formalized. Mathlib/RingTheory/Ideal/Operations.lean ideal multiplication and power instances; Ideal.mul_assoc; Ideal.prod_mem_prod — Ideal multiplication is generated by finite sums of products, with finite products and powers and I^0=⊤=(1).
Comparison: Ideal arithmetic laws and modular law
Sum/intersection/product are associative where defined; product distributes over sum; modular law 𝔞∩(𝔟+𝔠)=𝔞∩𝔟+𝔞∩𝔠 under the stated containment; 𝔞𝔟⊆𝔞∩𝔟, with equality when 𝔞+𝔟=(1).
Formalized. Ideal.mul_assoc; Ideal.mul_sup; Ideal.sup_mul; Ideal.mul_le_inf; Mathlib/Order/ModularLattice.lean::sup_inf_assoc_of_le; Ideal.mul_eq_inf_of_isCoprime — These give associativity/distributivity, the modular lattice identity under the source containment, ab≤a∩b, and equality for comaximal ideals.
Definition: Coprime/comaximal ideals
𝔞 and 𝔟 are coprime iff 𝔞+𝔟=(1), equivalently 1=x+y with x∈𝔞,y∈𝔟.
Formalized. Mathlib/RingTheory/Ideal/Operations.lean::Ideal.IsCoprime; isCoprime_iff_sup_eq; Ideal.isCoprime_iff_add — Coprimality is exactly a+b=⊤; membership of 1 in the sum gives 1=x+y with the stated memberships.
Construction: Finite direct product of rings
∏Aᵢ has componentwise operations and identity (1,…,1); coordinate projections are ring homomorphisms.
Formalized. Mathlib/Algebra/Ring/Prod.lean; RingHom.fst; RingHom.snd; finite Pi ring instances — Finite products have componentwise ring operations and unit, and coordinate projections are ring homomorphisms.
Construction: Chinese-remainder comparison map
φ:A→∏(A/𝔞ᵢ), x↦(x+𝔞₁,…,x+𝔞ₙ).
Formalized. Mathlib/RingTheory/Ideal/Quotient/Operations.lean::Ideal.quotientInfToPiQuotient — This is the canonical map A → ∏ i, A/Iᵢ, sending x to its quotient classes.
Proposition 1.10: Chinese remainder criteria
Pairwise coprime ideals satisfy ∏𝔞ᵢ=∩𝔞ᵢ; φ is surjective iff pairwise coprime and injective iff ∩𝔞ᵢ=0.
Formalized. Ideal.prod_eq_iInf_of_pairwise_isCoprime; Ideal.quotientInfToPiQuotient_surj; Ideal.quotientInfRingEquivPiQuotient; kernel of quotientInfToPiQuotient — Pairwise comaximal ideals have product equal to intersection; the CRT map is surjective exactly in the pairwise-coprime setting and its kernel is the intersection, so injectivity is equivalent to zero intersection.
Proposition 1.11: Prime avoidance / prime over finite intersection
Finite prime avoidance for an ideal; a prime containing a finite intersection contains one member, with equality consequence.
Formalized. Mathlib/RingTheory/Ideal/Operations.lean::Ideal.subset_union_prime; Ideal.subset_union_prime_finite; Ideal.IsPrime.prod_le — Mathlib supplies finite prime avoidance and the prime-containing-a-finite-product/intersection consequence used in Proposition 1.11.
Definition: Ideal quotient (𝔞:𝔟)
(𝔞:𝔟)={x∈A : x𝔟⊆𝔞}.
Formalized. Mathlib/RingTheory/Ideal/Colon.lean::Submodule.colon; Ideal.mem_colon — The colon ideal consists exactly of x such that x • I ≤ J, i.e. xI⊆J in the commutative ring.
Definition / notation: Annihilator ideal
Ann(𝔟)=(0:𝔟); for principal (x), write (𝔞:x) for (𝔞:(x)).
Formalized. Mathlib/RingTheory/Ideal/Maps.lean::Module.annihilator; Mathlib/RingTheory/Ideal/Colon.lean::Submodule.bot_colon; Ideal.mem_colon_span_singleton — The annihilator is (0:I), and the singleton colon specializes to the source notation (a:x).
Definition: Radical of an ideal
r(𝔞)={x:xⁿ∈𝔞 for some n>0}; equivalently inverse image of the nilradical of A/𝔞.
Formalized. Mathlib/RingTheory/Ideal/Operations.lean::Ideal.radical; Ideal.mem_radical_iff; Mathlib/RingTheory/Ideal/Maps.lean::Ideal.comap_radical; Mathlib/RingTheory/Nilpotent/Lemmas.lean::nilradical — Ideal radical has exactly the positive-power membership condition; the quotient characterization identifies it as the pullback of the quotient nilradical.
Proposition 1.14: Radical as intersection of containing primes
r(𝔞) equals the intersection of prime ideals containing 𝔞.
Formalized. Mathlib/RingTheory/Ideal/Operations.lean::Ideal.radical_eq_sInf — The radical is the infimum/intersection of all prime ideals containing the ideal.
Construction: Radical of an arbitrary subset
r(E) is defined by the same power condition; generally not an ideal; radicals commute with arbitrary unions.
Not formalized. partial: Ideal.radical for ideals only — P/H have ideal radicals but no checked construction of the source’s power-radical for an arbitrary subset E, together with the fact it need not be an ideal and the arbitrary-union law. Targeted external search found no exact Lean owner.
Searched: N
Proposition 1.15: Zero-divisors via radicals of annihilators
D=⋃_{x≠0} r(Ann(x)).
Not formalized. partial: Module.annihilator; Ideal.radical; nonZeroDivisors; Noetherian associated-prime results — No checked P/H or external declaration proves the source-general identity D = ⋃_{x≠0} radical(Ann(x)); the available associated-prime description of zero divisors has stronger finiteness/Noetherian hypotheses and is not this theorem.
Searched: N
Proposition 1.16: Coprimality from coprime radicals
If r(𝔞) and r(𝔟) are coprime, then 𝔞 and 𝔟 are coprime.
Not formalized. partial: Ideal.radical; Ideal.IsCoprime — Neither P nor H nor targeted external Lean search contains the implication that coprime radicals force the original ideals to be coprime as a named/source-shaped theorem.
Searched: N
Definition: Extension of an ideal
For f:A→B, 𝔞ᵉ=Bf(𝔞), the ideal generated by the image of 𝔞.
Formalized. Mathlib/RingTheory/Ideal/Maps.lean::Ideal.map; Ideal.map_span — I.map f is the ideal generated by the image f(I), exactly extension Iᵉ.
Definition: Contraction of an ideal
For ideal 𝔟⊂B, 𝔟ᶜ=f⁻¹(𝔟); prime ideals contract to prime ideals.
Formalized. Mathlib/RingTheory/Ideal/Maps.lean::Ideal.comap; Ideal.IsPrime.comap — J.comap f is inverse image/contraction, and prime ideals contract to prime ideals.
Comparison: Surjective versus injective behavior of ideals under a ring homomorphism
Factor f as A↠f(A)↪B: ideals over the surjective part correspond by Proposition 1.1, while extension across the inclusion is generally subtler.
Formalized. RingHom.range; RingHom.rangeSRestrict; Ideal.relIsoOfSurjective; Ideal.map; Ideal.comap — Mathlib factors a ring map through its range and gives the full ideal correspondence for the surjective factor, while extension across the range inclusion remains the general map operation, exactly the source comparison.
Reusable example: Prime extension in Z⊂Z[i]
- ramifies as ((1+i)²); p≡1 mod4 splits into two distinct prime ideals; p≡3 mod4 remains prime; relates splitting to sums of two squares.
Not formalized. partial: Mathlib/NumberTheory/Zsqrtd/QuadraticReciprocity.lean::GaussianInt.prime_iff_mod_four_eq_three_of_nat_prime; Mathlib/NumberTheory/SumTwoSquares.lean::Nat.Prime.sq_add_sq — P/H prove that a rational prime stays prime in ℤ[i] exactly in the 3 mod 4 case and supply the sum-of-two-squares theorem, but no checked declaration realizes the full ideal-factorization bundle (2)=((1+i)^2) plus the two-distinct-prime-ideal splitting for p≡1 mod4. Targeted GitHub search found only Mathlib/mirrors and no complete external owner.
Searched: N
Proposition 1.17: Extension–contraction identities and bijection on fixed ideals
𝔞⊆𝔞ᵉᶜ, 𝔟⊇𝔟ᶜᵉ; iterated ec/ce stabilize, giving inverse bijections between contracted ideals of A and extended ideals of B.
Formalized. Mathlib/RingTheory/Ideal/Maps.lean::Ideal.gc_map_comap; Ideal.le_comap_map; Ideal.map_comap_le; Ideal.map_comap_map; Ideal.comap_map_comap — Extension and contraction form a Galois connection; its unit/counit inequalities and closure/interior idempotence are exactly the stated a⊆aᵉᶜ, b⊇bᶜᵉ, stabilization, and fixed-point bijection.