Theorems · Definition · commutative algebra

Perfection.lift

(p : ℕ) →
  [hp : Fact (Nat.Prime p)] →
    (R : Type u₁) →
      [inst : CommSemiring R] →
        [CharP R p] →
          [PerfectRing R p] →
            (S : Type u₂) → [inst_3 : CommSemiring S] → [inst_4 : CharP S p] → (R →+* S) ≃ (R →+* Perfection S p)

Given rings R and S of characteristic p, with R being perfect, any homomorphism R →+* S can be lifted to a homomorphism R →+* Perfection S p.

Defined in

Mathlib.RingTheory.Perfection

Cited by

8 results in Mathlib

Foundations

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

Assumes

FactCommSemiringCharPPerfectRingCommSemiringCharP