English
If f is a ring isomorphism, mapping an ideal forward by f and then back by f’s inverse yields the original ideal: map f I then map f⁻¹ returns I.
Русский
Если f — изоморфизм колец, отображение I вперёд и затем обратное возвращает I.
LaTeX
$$$f : R \simeq+\! S \Rightarrow (I.map (f : R \to+* S)).map (f^{-1} : S \to+* R) = I$$$
Lean4
/-- 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).) -/
@[simps!]
def piOrderIso [Finite ι] : Ideal (Π i, R i) ≃o Π i, Ideal (R i) :=
.symm
{ toFun := pi
invFun I i := I.map (Pi.evalRingHom R i)
left_inv _ := funext map_evalRingHom_pi
right_inv
I := by
ext r
simp_rw [mem_pi, mem_map_iff_of_surjective (Pi.evalRingHom R _) (Function.surjective_eval _)]
refine ⟨(fun ⟨r', hr'⟩ ↦ ?_) ∘ Classical.skolem.mp, fun hr i ↦ ⟨r, hr, rfl⟩⟩
have := Fintype.ofFinite ι
classical
rw [show r = ∑ i, Pi.single i 1 * r' i from
funext fun i ↦ by rw [← (hr' _).2, Finset.sum_apply, Fintype.sum_eq_single i fun j ne ↦ by simp [ne]]; simp]
exact sum_mem fun i _ ↦ I.mul_mem_left _ (hr' i).1
map_rel_iff' := pi_le_pi_iff }
