Theorems · Theorem · commutative algebra

PerfectionMap.lift_symm_apply

∀ (p : ℕ) [inst : Fact (Nat.Prime p)] (R : Type u₁) [inst_1 : CommSemiring R] [inst_2 : CharP R p]
  [inst_3 : 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) (m : PerfectionMap p π)
  (f : R →+* P), (PerfectionMap.lift p R S P π m).symm f = π.comp f

Defined in

Mathlib.RingTheory.Perfection

Cited by

0 results in Mathlib

Foundations

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

Assumes

FactCommSemiringCharPPerfectRingCommSemiringCharPCommSemiringCharPPerfectRing