Documentation

Mathlib.FieldTheory.PerfectClosure

The perfect closure of a characteristic p ring #

Main definitions #

Main results #

Tags #

perfect ring, perfect closure

theorem PerfectClosure.r_iff (K : Type u) [CommRing K] (p : ) [Fact (Nat.Prime p)] [CharP K p] :
∀ (a a_1 : × K), PerfectClosure.R K p a a_1 ∃ (n : ) (x : K), a = (n, x) a_1 = (n + 1, (frobenius K p) x)
inductive PerfectClosure.R (K : Type u) [CommRing K] (p : ) [Fact (Nat.Prime p)] [CharP K p] :
× K × KProp

PerfectClosure.R is the relation (n, x) ∼ (n + 1, x ^ p) for n : ℕ and x : K. PerfectClosure K p is the quotient by this relation.

Instances For
    def PerfectClosure (K : Type u) [CommRing K] (p : ) [Fact (Nat.Prime p)] [CharP K p] :

    The perfect closure is the smallest extension that makes frobenius surjective.

    Equations
    Instances For
      def PerfectClosure.mk (K : Type u) [CommRing K] (p : ) [Fact (Nat.Prime p)] [CharP K p] (x : × K) :

      PerfectClosure.mk K p (n, x) for n : ℕ and x : K is an element of PerfectClosure K p, viewed as x ^ (p ^ -n). Every element of PerfectClosure K p is of this form (PerfectClosure.mk_surjective).

      Equations
      Instances For
        @[simp]
        theorem PerfectClosure.mk_succ_pow (K : Type u) [CommRing K] (p : ) [Fact (Nat.Prime p)] [CharP K p] (m : ) (x : K) :
        PerfectClosure.mk K p (m + 1, x ^ p) = PerfectClosure.mk K p (m, x)
        @[simp]
        theorem PerfectClosure.quot_mk_eq_mk (K : Type u) [CommRing K] (p : ) [Fact (Nat.Prime p)] [CharP K p] (x : × K) :
        def PerfectClosure.liftOn {K : Type u} [CommRing K] {p : } [Fact (Nat.Prime p)] [CharP K p] {L : Type u_1} (x : PerfectClosure K p) (f : × KL) (hf : ∀ (x y : × K), PerfectClosure.R K p x yf x = f y) :
        L

        Lift a function ℕ × K → L to a function on PerfectClosure K p.

        Equations
        Instances For
          @[simp]
          theorem PerfectClosure.liftOn_mk {K : Type u} [CommRing K] {p : } [Fact (Nat.Prime p)] [CharP K p] {L : Type u_1} (f : × KL) (hf : ∀ (x y : × K), PerfectClosure.R K p x yf x = f y) (x : × K) :
          theorem PerfectClosure.induction_on {K : Type u} [CommRing K] {p : } [Fact (Nat.Prime p)] [CharP K p] (x : PerfectClosure K p) {q : PerfectClosure K pProp} (h : ∀ (x : × K), q (PerfectClosure.mk K p x)) :
          q x
          instance PerfectClosure.instMul (K : Type u) [CommRing K] (p : ) [Fact (Nat.Prime p)] [CharP K p] :
          Equations
          • One or more equations did not get rendered due to their size.
          @[simp]
          theorem PerfectClosure.mk_mul_mk (K : Type u) [CommRing K] (p : ) [Fact (Nat.Prime p)] [CharP K p] (x : × K) (y : × K) :
          PerfectClosure.mk K p x * PerfectClosure.mk K p y = PerfectClosure.mk K p (x.1 + y.1, ((frobenius K p))^[y.1] x.2 * ((frobenius K p))^[x.1] y.2)
          Equations
          theorem PerfectClosure.one_def (K : Type u) [CommRing K] (p : ) [Fact (Nat.Prime p)] [CharP K p] :
          1 = PerfectClosure.mk K p (0, 1)
          Equations
          instance PerfectClosure.instAdd (K : Type u) [CommRing K] (p : ) [Fact (Nat.Prime p)] [CharP K p] :
          Equations
          • One or more equations did not get rendered due to their size.
          @[simp]
          theorem PerfectClosure.mk_add_mk (K : Type u) [CommRing K] (p : ) [Fact (Nat.Prime p)] [CharP K p] (x : × K) (y : × K) :
          PerfectClosure.mk K p x + PerfectClosure.mk K p y = PerfectClosure.mk K p (x.1 + y.1, ((frobenius K p))^[y.1] x.2 + ((frobenius K p))^[x.1] y.2)
          instance PerfectClosure.instNeg (K : Type u) [CommRing K] (p : ) [Fact (Nat.Prime p)] [CharP K p] :
          Equations
          @[simp]
          theorem PerfectClosure.neg_mk (K : Type u) [CommRing K] (p : ) [Fact (Nat.Prime p)] [CharP K p] (x : × K) :
          instance PerfectClosure.instZero (K : Type u) [CommRing K] (p : ) [Fact (Nat.Prime p)] [CharP K p] :
          Equations
          theorem PerfectClosure.zero_def (K : Type u) [CommRing K] (p : ) [Fact (Nat.Prime p)] [CharP K p] :
          0 = PerfectClosure.mk K p (0, 0)
          @[simp]
          theorem PerfectClosure.mk_zero_zero (K : Type u) [CommRing K] (p : ) [Fact (Nat.Prime p)] [CharP K p] :
          PerfectClosure.mk K p (0, 0) = 0
          theorem PerfectClosure.mk_zero (K : Type u) [CommRing K] (p : ) [Fact (Nat.Prime p)] [CharP K p] (n : ) :
          PerfectClosure.mk K p (n, 0) = 0
          theorem PerfectClosure.R.sound (K : Type u) [CommRing K] (p : ) [Fact (Nat.Prime p)] [CharP K p] (m : ) (n : ) (x : K) (y : K) (H : ((frobenius K p))^[m] x = y) :
          PerfectClosure.mk K p (n, x) = PerfectClosure.mk K p (m + n, y)
          Equations
          Equations
          theorem PerfectClosure.mk_eq_iff (K : Type u) [CommRing K] (p : ) [Fact (Nat.Prime p)] [CharP K p] (x : × K) (y : × K) :
          PerfectClosure.mk K p x = PerfectClosure.mk K p y ∃ (z : ), ((frobenius K p))^[y.1 + z] x.2 = ((frobenius K p))^[x.1 + z] y.2
          @[simp]
          theorem PerfectClosure.mk_pow (K : Type u) [CommRing K] (p : ) [Fact (Nat.Prime p)] [CharP K p] (x : × K) (n : ) :
          PerfectClosure.mk K p x ^ n = PerfectClosure.mk K p (x.1, x.2 ^ n)
          theorem PerfectClosure.natCast (K : Type u) [CommRing K] (p : ) [Fact (Nat.Prime p)] [CharP K p] (n : ) (x : ) :
          x = PerfectClosure.mk K p (n, x)
          theorem PerfectClosure.intCast (K : Type u) [CommRing K] (p : ) [Fact (Nat.Prime p)] [CharP K p] (x : ) :
          x = PerfectClosure.mk K p (0, x)
          theorem PerfectClosure.natCast_eq_iff (K : Type u) [CommRing K] (p : ) [Fact (Nat.Prime p)] [CharP K p] (x : ) (y : ) :
          x = y x = y
          instance PerfectClosure.instCharP (K : Type u) [CommRing K] (p : ) [Fact (Nat.Prime p)] [CharP K p] :
          Equations
          • =
          theorem PerfectClosure.frobenius_mk (K : Type u) [CommRing K] (p : ) [Fact (Nat.Prime p)] [CharP K p] (x : × K) :
          (frobenius (PerfectClosure K p) p) (PerfectClosure.mk K p x) = PerfectClosure.mk K p (x.1, x.2 ^ p)
          def PerfectClosure.of (K : Type u) [CommRing K] (p : ) [Fact (Nat.Prime p)] [CharP K p] :

          Embedding of K into PerfectClosure K p

          Equations
          • PerfectClosure.of K p = { toMonoidHom := { toOneHom := { toFun := fun (x : K) => PerfectClosure.mk K p (0, x), map_one' := }, map_mul' := }, map_zero' := , map_add' := }
          Instances For
            theorem PerfectClosure.of_apply (K : Type u) [CommRing K] (p : ) [Fact (Nat.Prime p)] [CharP K p] (x : K) :
            Equations
            • =
            Equations
            • =
            @[simp]
            theorem PerfectClosure.iterate_frobenius_mk (K : Type u) [CommRing K] (p : ) [Fact (Nat.Prime p)] [CharP K p] (n : ) (x : K) :
            ((frobenius (PerfectClosure K p) p))^[n] (PerfectClosure.mk K p (n, x)) = (PerfectClosure.of K p) x
            noncomputable def PerfectClosure.lift (K : Type u) [CommRing K] (p : ) [Fact (Nat.Prime p)] [CharP K p] (L : Type v) [CommSemiring L] [CharP L p] [PerfectRing L p] :

            Given a ring K of characteristic p and a perfect ring L of the same characteristic, any homomorphism K →+* L can be lifted to PerfectClosure K p.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              theorem PerfectClosure.eq_iff (K : Type u) [CommRing K] [IsReduced K] (p : ) [Fact (Nat.Prime p)] [CharP K p] (x : × K) (y : × K) :
              PerfectClosure.mk K p x = PerfectClosure.mk K p y ((frobenius K p))^[y.1] x.2 = ((frobenius K p))^[x.1] y.2
              instance PerfectClosure.instInv (K : Type u) [Field K] (p : ) [Fact (Nat.Prime p)] [CharP K p] :
              Equations
              @[simp]
              theorem PerfectClosure.mk_inv (K : Type u) [Field K] (p : ) [Fact (Nat.Prime p)] [CharP K p] (x : × K) :
              Equations
              instance PerfectClosure.instField (K : Type u) [Field K] (p : ) [Fact (Nat.Prime p)] [CharP K p] :
              Equations
              • PerfectClosure.instField K p = let __src := inferInstance; let __src_1 := inferInstance; Field.mk DivisionRing.zpow DivisionRing.qsmul
              Equations
              • =