map_injective — Mathlib

English

The map that sends an intermediate field along an algebra hom f is injective.

Русский

Отображение промежуточного поля по гомоморфизму f инъективно.

LaTeX

$$$ \\text{map}_f : \\text{IntermediateField}(K,L) \\to \\text{IntermediateField}(K,L') \\; \\text{is injective}$$$

Lean4

theorem map_injective (f : L →ₐ[K] L') : Function.Injective (map f) :=
  by
  intro _ _ h
  rwa [← toSubalgebra_injective.eq_iff, toSubalgebra_map, toSubalgebra_map,
    (Subalgebra.map_injective f.injective).eq_iff, toSubalgebra_inj] at h

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