extendScalars_injective — Mathlib

English

Let F ≤ E ≤ L be intermediate fields of the extension L/K. The map that sends each intermediate field E (with F ≤ E) to its scalar extension extendScalars(E) is injective on the collection of such intermediate fields; i.e., if extendScalars(E) = extendScalars(E') then E = E'.

Русский

Пусть F ⊆ E ⊆ L — промежуточные поля расширения L/K. Отображение E ↦ extendScalars(E) инъективно на множестве таких полей: если extendScalars(E) = extendScalars(E'), то E = E'.

LaTeX

$$$\\forall E,E'\\big( F \\le E \\land F \\le E' \\rightarrow (extendScalars(E) = extendScalars(E') \\rightarrow E = E') \\big)$$$

Lean4

theorem extendScalars_injective : Function.Injective fun E : { E : Subfield L // F ≤ E } ↦ extendScalars E.2 :=
  (extendScalars.orderIso F).injective

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