Structures · Algebra
IsPRadical
If i : K →+* L is a ring homomorphism of characteristic p rings, then it is called
p-radical if the following conditions are satisfied:
- For any element x of L there is n : ℕ such that x ^ (p ^ n) is contained in K.
- The kernel of i is contained in the p-nilradical of K.
It is a generalization of purely inseparable extension for fields.
- Defined in
- Mathlib.FieldTheory.IsPerfectClosure
- Shape
- 2 explicit arguments · adds pow_mem', ker_le'
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by36
- PerfectRing.lift
- PerfectRing.liftEquiv
- PerfectRing.liftAux
- PerfectRing.liftAux_self_apply
- IsPRadical.pow_mem
- PerfectRing.lift_comp_apply
- PerfectRing.lift_aux
- IsPRadical.injective_comp_of_perfect
- IsPRadical.ker_le
- PerfectRing.lift_comp
- PerfectRing.lift_lift
- PerfectRing.lift_comp_lift_apply
- IsPRadical.injective_comp_of_pNilradical_eq_bot
- PerfectRing.liftAux_apply
- IsPRadical.ker_le'
- IsPRadical.comap_pNilradical
- PerfectRing.lift_comp_lift_apply_eq_self
- PerfectRing.liftEquiv_comp_apply
- PerfectRing.comp_lift
- PerfectRing.lift_apply
- IsPRadical.pow_mem'
- PerfectRing.lift_self_apply
- PerfectRing.lift_comp_lift
- PerfectRing.liftAux.congr_simp
- PerfectRing.liftAux_self
- PerfectRing.lift_lift_apply
- PerfectRing.lift.congr_simp
- PerfectRing.liftEquiv_apply
- PerfectRing.comp_lift_apply
- PerfectRing.liftEquiv_trans
- IsPRadical.injective_comp
- IsPRadical.isPurelyInseparable
- PerfectRing.liftEquiv_symm_apply
- PerfectRing.lift_self
- IsPRadical.trans
- PerfectRing.lift_comp_lift_eq_id
Ancestors0
No ancestors.