Theorems · Definition · commutative algebra

PerfectionMap.casesOn

{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] →
                  {π : P →+* R} →
                    {motive : PerfectionMap p π → Sort u} →
                      (t : PerfectionMap p π) →
                        ((injective :
                              ∀ ⦃x y : P⦄,
                                (∀ (n : ℕ),
                                    π ((⇑(frobeniusEquiv P p).symm)^[n] x) = π ((⇑(frobeniusEquiv P p).symm)^[n] y)) →
                                  x = y) →
                            (surjective :
                                ∀ (f : ℕ → R),
                                  (∀ (n : ℕ), f (n + 1) ^ p = f n) →
                                    ∃ x, ∀ (n : ℕ), π ((⇑(frobeniusEquiv P p).symm)^[n] x) = f n) →
                              motive ⋯) →
                          motive t

Defined in

Mathlib.RingTheory.Perfection

Cited by

0 results in Mathlib

Foundations

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

Assumes

FactCommSemiringCharPCommSemiringCharPPerfectRing