Theorems · Definition · commutative algebra

PerfectionMap.map

(p : ℕ) →
  [inst : Fact (Nat.Prime p)] →
    {R : Type u₁} →
      [inst_1 : CommSemiring R] →
        [inst_2 : CharP R p] →
          {P : Type u₃} →
            [inst_3 : CommSemiring P] →
              [inst_4 : CharP P p] →
                [inst_5 : PerfectRing P p] →
                  {S : Type u₂} →
                    [inst_6 : CommSemiring S] →
                      [inst_7 : CharP S p] →
                        {Q : Type u₄} →
                          [inst_8 : CommSemiring Q] →
                            [inst_9 : CharP Q p] →
                              [inst_10 : PerfectRing Q p] →
                                {π : P →+* R} →
                                  PerfectionMap p π → {σ : Q →+* S} → PerfectionMap p σ → (R →+* S) → P →+* Q

A ring homomorphism R →+* S induces P →+* Q, a map of the respective perfections.

Defined in

Mathlib.RingTheory.Perfection

Cited by

3 results in Mathlib

Foundations

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

Assumes

FactCommSemiringCharPCommSemiringCharPPerfectRingCommSemiringCharPCommSemiringCharPPerfectRing