Theorems · Definition · commutative algebra

Ideal.piOrderIso

{ι : Type u_4} →
  {R : ι → Type u_5} → [inst : (i : ι) → Semiring (R i)] → [Finite ι] → Ideal ((i : ι) → R i) ≃o ((i : ι) → Ideal (R i))

Ideals in a finite direct product semiring Πᵢ Rᵢ are identified with tuples of ideals in the individual semirings, in an order-preserving way. (Note that this is not in general true for infinite direct products: If infinitely many of the Rᵢ are nontrivial, then there exists an ideal of Πᵢ Rᵢ that is not of the form Πᵢ Iᵢ, namely the ideal of finitely supported elements of Πᵢ Rᵢ (it is also not a principal ideal).)

Defined in

Mathlib.RingTheory.Ideal.Maps

Cited by

2 results in Mathlib

Foundations

Depth 72 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SemiringFinite