map_iInf — Mathlib

English

Let f be a ring homomorphism and s(i) a nonempty index family of subfields of K. Then (iInf s).map f = ⨅ i, (s i).map f.

Русский

Пусть f — кольцеобразный гомоморфизм, и {S_i} — непустая индексированная семейство подполей K. Тогда (iInf s).map f = ⨅ i, (s i).map f.

LaTeX

$$$$(\operatorname{iInf}_{i} S(i)).map f = \bigwedge_{i} (S(i)).map f$$$$

Lean4

theorem map_iInf {ι : Sort*} [Nonempty ι] (f : K →+* L) (s : ι → Subfield K) : (iInf s).map f = ⨅ i, (s i).map f :=
  by
  apply SetLike.coe_injective
  simpa using (Set.injOn_of_injective f.injective).image_iInter_eq (s := SetLike.coe ∘ s)

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