Theorems · Definition · commutative algebra

PerfectionMap.lift

(p : ℕ) →
  [inst : Fact (Nat.Prime p)] →
    (R : Type u₁) →
      [inst_1 : CommSemiring R] →
        [CharP R p] →
          [PerfectRing R p] →
            (S : Type u₂) →
              [inst_4 : CommSemiring S] →
                [inst_5 : CharP S p] →
                  (P : Type u₃) →
                    [inst_6 : CommSemiring P] →
                      [inst_7 : CharP P p] →
                        [inst_8 : PerfectRing P p] → (π : P →+* S) → PerfectionMap p π → (R →+* S) ≃ (R →+* P)

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

Defined in

Mathlib.RingTheory.Perfection

Cited by

4 results in Mathlib

Foundations

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

Assumes

FactCommSemiringCharPPerfectRingCommSemiringCharPCommSemiringCharPPerfectRing