Structures · Algebra
PerfectRing
A perfect ring of characteristic p (prime) in the sense of Serre.
NB: This is not related to the concept with the same name introduced by Bass (related to projective
covers of modules).
- Defined in
- Mathlib.FieldTheory.Perfect
- Shape
- 2 explicit arguments · adds bijective_frobenius
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances5
- PerfectClosure
- Perfection
- PreTilt
- Subtype
- Prod
How is a type an instance?
Loading the hierarchy index…
Assumed by178
- frobeniusEquiv
- iterateFrobeniusEquiv
- PerfectRing.lift
- IsPerfectClosure
- IsPerfectClosure.equiv
- powMulEquiv
- WittVector.FractionRing.frobeniusRingHom
- WittVector.Isocrystal.frobenius
- WittVector.FractionRing.frobenius
- WittVector.frobeniusEquiv
- Perfection.lift
- PerfectionMap.equiv
- PerfectRing.liftEquiv
- frobenius_apply_frobeniusEquiv_symm
- PerfectRing.liftAux
- PerfectionMap.lift
- Perfection.liftMonoidHom
- frobeniusEquiv_apply
- PerfectRing.liftAux_self_apply
- iterateFrobeniusEquiv_add_apply
- PerfectRing.lift_comp_apply
- PerfectionMap.map
- frobeniusEquiv_symm_apply_frobenius
- IsPRadical.injective_comp_of_perfect
- PerfectRing.liftAux_id_apply
- WittVector.frobeniusEquiv_apply
- Polynomial.roots_expand_pow
- PerfectRing.lift_comp
- iterateFrobeniusEquiv_def
- iterateFrobeniusEquiv_apply
- Polynomial.roots_X_pow_char_pow_sub_C
- WittVector.frobenius_bijective
- PerfectRing.lift_lift
- WittVector.exists_eq_pow_p_mul
- PerfectRing.toPerfectField
- PerfectRing.lift_comp_lift_apply
- iterateFrobeniusEquiv_one
- PerfectRing.bijective_frobenius
- FiniteField.frobeniusAlgEquiv
- bijective_frobenius
- iterateFrobeniusEquiv_eq_pow
- IsPerfectClosure.equiv_self_apply
- Polynomial.rootsExpandPowEquivRoots
- PerfectRing.liftAux_apply
- iterate_frobeniusEquiv_symm_pow_p_pow
- frobeniusEquiv_symm_pow_p
- IsPerfectClosure.equiv_comp_equiv_apply
- PerfectRing.lift_comp_lift_apply_eq_self
- MonoidHom.map_iterate_frobeniusEquiv_symm
- frobeniusEquiv_symm_pow
Ancestors0
No ancestors.