prod — Mathlib

English

The ideal product I.prod J in R × S is the intersection of the pullback of I and J along fst and snd.

Русский

Произведение идеалов I.prod J в кольце R × S есть пересечение их обратных отображений по fst и snd.

LaTeX

$$prod : \text{Ideal}(R) \to \text{Ideal}(S) \to \text{Ideal}(R \times S) \,; \\ prod\ I\ J = I.comap(\text{fst}) \cap J.comap(\text{snd})$$

Lean4

/-- `I × J` as an ideal of `R × S`. -/
def prod : Ideal (R × S) :=
  I.comap (RingHom.fst R S) ⊓ J.comap (RingHom.snd R S)

Похожие утверждения