comap_map_eq_of_injective — Mathlib

English

If S is a substructure of M and f:M→[L]N is an L-homomorphism that is injective, then the comapped image of S under map f, comap f (map f S), equals S.

Русский

Пусть S — подструктура M и f:M →[L] N — инъективный гомоморфизм языковой теории. Тогда comap f (map f S) = S.

LaTeX

$$$(S.map\\ f).comap f = S$ (при $hf: \\text{Injective } f\$)$$

Lean4

theorem comap_map_eq_of_injective (S : L.Substructure M) : (S.map f).comap f = S :=
  (gciMapComap hf).u_l_eq _

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