Documentation

Mathlib.FieldTheory.PerfectClosure

The perfect closure of a field #

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, 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 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.

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

      Constructor for PerfectClosure.

      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.

        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
          @[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.fst + y.fst, (↑(frobenius K p))^[y.fst] x.snd * (↑(frobenius K p))^[x.fst] y.snd)
          theorem PerfectClosure.one_def (K : Type u) [CommRing K] (p : ) [Fact (Nat.Prime p)] [CharP K p] :
          1 = PerfectClosure.mk K p (0, 1)
          @[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.fst + y.fst, (↑(frobenius K p))^[y.fst] x.snd + (↑(frobenius K p))^[x.fst] y.snd)
          @[simp]
          theorem PerfectClosure.neg_mk (K : Type u) [CommRing K] (p : ) [Fact (Nat.Prime p)] [CharP K p] (x : × K) :
          -PerfectClosure.mk K p x = PerfectClosure.mk K p (x.fst, -x.snd)
          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)
          theorem PerfectClosure.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.fst + z] x.snd = (↑(frobenius K p))^[x.fst + z] y.snd
          theorem PerfectClosure.nat_cast (K : Type u) [CommRing K] (p : ) [Fact (Nat.Prime p)] [CharP K p] (n : ) (x : ) :
          x = PerfectClosure.mk K p (n, x)
          theorem PerfectClosure.int_cast (K : Type u) [CommRing K] (p : ) [Fact (Nat.Prime p)] [CharP K p] (x : ) :
          x = PerfectClosure.mk K p (0, x)
          theorem PerfectClosure.nat_cast_eq_iff (K : Type u) [CommRing K] (p : ) [Fact (Nat.Prime p)] [CharP K p] (x : ) (y : ) :
          x = y x = y
          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.fst, x.snd ^ p)
          def PerfectClosure.of (K : Type u) [CommRing K] (p : ) [Fact (Nat.Prime p)] [CharP K p] :

          Embedding of K into PerfectClosure K p

          Instances For
            theorem PerfectClosure.of_apply (K : Type u) [CommRing K] (p : ) [Fact (Nat.Prime p)] [CharP K p] (x : K) :
            ↑(PerfectClosure.of K p) x = PerfectClosure.mk K p (0, x)
            theorem PerfectClosure.eq_iff (K : Type u) [CommRing K] [IsReduced K] (p : ) [Fact (Nat.Prime p)] [CharP K p] (x : × K) (y : × K) :
            Quot.mk (PerfectClosure.R K p) x = Quot.mk (PerfectClosure.R K p) y (↑(frobenius K p))^[y.fst] x.snd = (↑(frobenius K p))^[x.fst] y.snd
            @[simp]
            theorem PerfectClosure.mk_inv (K : Type u) [Field K] (p : ) [Fact (Nat.Prime p)] [CharP K p] (x : × K) :
            @[simp]
            theorem PerfectClosure.iterate_frobenius_mk (K : Type u) [Field K] (p : ) [Fact (Nat.Prime p)] [CharP K p] (n : ) (x : K) :
            noncomputable def PerfectClosure.lift (K : Type u) [Field K] (p : ) [Fact (Nat.Prime p)] [CharP K p] (L : Type v) [CommSemiring L] [CharP L p] [PerfectRing L p] :

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

            Instances For