map_iInf — Mathlib

English

If f: A →ₐ[R] B is an injective algebra homomorphism, then the image of the infimum equals the infimum of the images: map f (iInf s) = ⨅ i, map f (s i).

Русский

Если f: A →ₐ[R] B — инъективное алгебраическое гомоморфизм, то образ пересечения равен пересечению образов: map f (iInf s) = ⨅ i, map f (s i).

LaTeX

$$Subalgebra.map f (iInf s) = iInf (fun i => Subalgebra.map f (s i))$$

Lean4

theorem map_iInf {ι : Sort*} [Nonempty ι] (f : A →ₐ[R] B) (hf : Function.Injective f) (s : ι → Subalgebra R A) :
    (iInf s).map f = ⨅ (i : ι), (s i).map f :=
  by
  apply SetLike.coe_injective
  simpa using (Set.injOn_of_injective hf).image_iInter_eq (s := SetLike.coe ∘ s)

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