comap_inf — Mathlib

English

If s and t are subrings of S and f: R →+* S is a ring homomorphism, then the preimage of the intersection equals the intersection of the preimages: (s ∩ t).comap f = s.comap f ∩ t.comap f.

Русский

Пусть s и t — подкольца S, а f: R →+* S — гомоморфизм колец. Тогда предобраз пересечения равен пересечению предобразов: (s ∩ t).comap f = s.comap f ∩ t.comap f.

LaTeX

$$$ (s \cap t).comap f = s.comap f \cap t.comap f $$$

Lean4

theorem comap_inf (s t : Subring S) (f : R →+* S) : (s ⊓ t).comap f = s.comap f ⊓ t.comap f :=
  (gc_map_comap f).u_inf

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