Theorems · Theorem · field theory

IsPurelyInseparable.injective_comp_algebraMap

∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] [IsPurelyInseparable F E]
  (L : Type u_2) [inst_4 : CommRing L] [IsReduced L], Function.Injective fun f => f.comp (algebraMap F E)

If E / F is purely inseparable, then for any reduced ring L, the map (E →+* L) → (F →+* L) induced by algebraMap F E is injective. In particular, a purely inseparable field extension is an epimorphism in the category of fields.

Defined in

Mathlib.FieldTheory.PurelyInseparable.Basic

Cited by

3 results in Mathlib

Foundations

Depth 187 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldFieldAlgebraIsPurelyInseparableCommRingIsReduced