Purely inseparable ring homomorphisms

In this file we define purely inseparable ring homomorphisms and show their meta properties.

Since purely inseparable is mainly used for fields, we cannot prove many general ring hom properties. E.g. we can't prove StableUnderComposition IsPurelyInseparable, since IsPurelyInseparable.trans requires the involved rings to be fields.

def RingHom.IsPurelyInseparable {F : Type u} {E : Type v} [CommRing F] [CommRing E] (f : F →+* E) : Prop

A ring homomorphism f : F →+* E is purely inseparable if E is purely inseparable as an F-algebra.

Equations

• f.IsPurelyInseparable = IsPurelyInseparable F E

theorem RingHom.isPurelyInseparable_algebraMap_iff {F : Type u} {E : Type v} [CommRing F] [CommRing E] [Algebra F E] : (algebraMap F E).IsPurelyInseparable ↔ IsPurelyInseparable F E

theorem RingHom.IsPurelyInseparable.id (F : Type u_1) [CommRing F] : (RingHom.id F).IsPurelyInseparable

The identity of a ring is purely inseparable.

theorem RingHom.IsPurelyInseparable.containsIdentities : ContainsIdentities fun {R S : Type u_4} [CommRing R] [CommRing S] => RingHom.IsPurelyInseparable

theorem RingHom.IsPurelyInseparable.comp {F : Type u_1} {E : Type u_2} {K : Type u_3} [Field F] [Field E] [Field K] {f : F →+* E} {g : E →+* K} (hf : f.IsPurelyInseparable) (hg : g.IsPurelyInseparable) : (g.comp f).IsPurelyInseparable

Composition of purely inseparable ring homomorphisms between fields is purely inseparable.