Documentation

Mathlib.RingTheory.Perfection

Ring Perfection and Tilt #

In this file we define the perfection of a ring of characteristic p, and the tilt of a field given a valuation to ℝ≥0.

TODO #

Define the valuation on the tilt, and define a characteristic predicate for the tilt.

def Monoid.perfection (M : Type u₁) [CommMonoid M] (p : ) :
Submonoid (M)

The perfection of a monoid M, defined to be the projective limit of M using the p-th power maps M → M indexed by the natural numbers, implemented as { f : ℕ → M | ∀ n, f (n + 1) ^ p = f n }.

Equations
Instances For
    def Ring.perfectionSubsemiring (R : Type u₁) [CommSemiring R] (p : ) [hp : Fact (Nat.Prime p)] [CharP R p] :

    The perfection of a ring R with characteristic p, as a subsemiring, defined to be the projective limit of R using the Frobenius maps R → R indexed by the natural numbers, implemented as { f : ℕ → R | ∀ n, f (n + 1) ^ p = f n }.

    Equations
    Instances For
      def Ring.perfectionSubring (R : Type u₁) [CommRing R] (p : ) [hp : Fact (Nat.Prime p)] [CharP R p] :
      Subring (R)

      The perfection of a ring R with characteristic p, as a subring, defined to be the projective limit of R using the Frobenius maps R → R indexed by the natural numbers, implemented as { f : ℕ → R | ∀ n, f (n + 1) ^ p = f n }.

      Equations
      Instances For
        def Ring.Perfection (R : Type u₁) [CommSemiring R] (p : ) :
        Type u₁

        The perfection of a ring R with characteristic p, defined to be the projective limit of R using the Frobenius maps R → R indexed by the natural numbers, implemented as {f : ℕ → R // ∀ n, f (n + 1) ^ p = f n}.

        Equations
        Instances For
          instance Perfection.commSemiring (R : Type u₁) [CommSemiring R] (p : ) [hp : Fact (Nat.Prime p)] [CharP R p] :
          Equations
          instance Perfection.charP (R : Type u₁) [CommSemiring R] (p : ) [hp : Fact (Nat.Prime p)] [CharP R p] :
          Equations
          • =
          instance Perfection.ring (p : ) [hp : Fact (Nat.Prime p)] (R : Type u₁) [CommRing R] [CharP R p] :
          Equations
          instance Perfection.commRing (p : ) [hp : Fact (Nat.Prime p)] (R : Type u₁) [CommRing R] [CharP R p] :
          Equations
          Equations
          def Perfection.coeff (R : Type u₁) [CommSemiring R] (p : ) [hp : Fact (Nat.Prime p)] [CharP R p] (n : ) :

          The n-th coefficient of an element of the perfection.

          Equations
          Instances For
            theorem Perfection.ext {R : Type u₁} [CommSemiring R] {p : } [hp : Fact (Nat.Prime p)] [CharP R p] {f : Ring.Perfection R p} {g : Ring.Perfection R p} (h : ∀ (n : ), (Perfection.coeff R p n) f = (Perfection.coeff R p n) g) :
            f = g
            def Perfection.pthRoot (R : Type u₁) [CommSemiring R] (p : ) [hp : Fact (Nat.Prime p)] [CharP R p] :

            The p-th root of an element of the perfection.

            Equations
            Instances For
              @[simp]
              theorem Perfection.coeff_mk {R : Type u₁} [CommSemiring R] {p : } [hp : Fact (Nat.Prime p)] [CharP R p] (f : R) (hf : ∀ (n : ), f (n + 1) ^ p = f n) (n : ) :
              (Perfection.coeff R p n) f, hf = f n
              theorem Perfection.coeff_pthRoot {R : Type u₁} [CommSemiring R] {p : } [hp : Fact (Nat.Prime p)] [CharP R p] (f : Ring.Perfection R p) (n : ) :
              (Perfection.coeff R p n) ((Perfection.pthRoot R p) f) = (Perfection.coeff R p (n + 1)) f
              theorem Perfection.coeff_pow_p {R : Type u₁} [CommSemiring R] {p : } [hp : Fact (Nat.Prime p)] [CharP R p] (f : Ring.Perfection R p) (n : ) :
              (Perfection.coeff R p (n + 1)) (f ^ p) = (Perfection.coeff R p n) f
              theorem Perfection.coeff_pow_p' {R : Type u₁} [CommSemiring R] {p : } [hp : Fact (Nat.Prime p)] [CharP R p] (f : Ring.Perfection R p) (n : ) :
              (Perfection.coeff R p (n + 1)) f ^ p = (Perfection.coeff R p n) f
              theorem Perfection.coeff_frobenius {R : Type u₁} [CommSemiring R] {p : } [hp : Fact (Nat.Prime p)] [CharP R p] (f : Ring.Perfection R p) (n : ) :
              (Perfection.coeff R p (n + 1)) ((frobenius (Ring.Perfection R p) p) f) = (Perfection.coeff R p n) f
              theorem Perfection.coeff_iterate_frobenius {R : Type u₁} [CommSemiring R] {p : } [hp : Fact (Nat.Prime p)] [CharP R p] (f : Ring.Perfection R p) (n : ) (m : ) :
              (Perfection.coeff R p (n + m)) (((frobenius (Ring.Perfection R p) p))^[m] f) = (Perfection.coeff R p n) f
              theorem Perfection.coeff_iterate_frobenius' {R : Type u₁} [CommSemiring R] {p : } [hp : Fact (Nat.Prime p)] [CharP R p] (f : Ring.Perfection R p) (n : ) (m : ) (hmn : m n) :
              (Perfection.coeff R p n) (((frobenius (Ring.Perfection R p) p))^[m] f) = (Perfection.coeff R p (n - m)) f
              theorem Perfection.coeff_add_ne_zero {R : Type u₁} [CommSemiring R] {p : } [hp : Fact (Nat.Prime p)] [CharP R p] {f : Ring.Perfection R p} {n : } (hfn : (Perfection.coeff R p n) f 0) (k : ) :
              (Perfection.coeff R p (n + k)) f 0
              theorem Perfection.coeff_ne_zero_of_le {R : Type u₁} [CommSemiring R] {p : } [hp : Fact (Nat.Prime p)] [CharP R p] {f : Ring.Perfection R p} {m : } {n : } (hfm : (Perfection.coeff R p m) f 0) (hmn : m n) :
              (Perfection.coeff R p n) f 0
              instance Perfection.perfectRing (R : Type u₁) [CommSemiring R] (p : ) [hp : Fact (Nat.Prime p)] [CharP R p] :
              Equations
              • =
              @[simp]
              theorem Perfection.lift_symm_apply (p : ) [hp : Fact (Nat.Prime p)] (R : Type u₁) [CommSemiring R] [CharP R p] [PerfectRing R p] (S : Type u₂) [CommSemiring S] [CharP S p] (f : R →+* Ring.Perfection S p) :
              (Perfection.lift p R S).symm f = (Perfection.coeff S p 0).comp f
              @[simp]
              theorem Perfection.lift_apply_apply_coe (p : ) [hp : Fact (Nat.Prime p)] (R : Type u₁) [CommSemiring R] [CharP R p] [PerfectRing R p] (S : Type u₂) [CommSemiring S] [CharP S p] (f : R →+* S) (r : R) (n : ) :
              (((Perfection.lift p R S) f) r) n = f (((frobeniusEquiv R p).symm)^[n] r)
              noncomputable def Perfection.lift (p : ) [hp : Fact (Nat.Prime p)] (R : Type u₁) [CommSemiring R] [CharP R p] [PerfectRing R p] (S : Type u₂) [CommSemiring S] [CharP S p] :

              Given rings R and S of characteristic p, with R being perfect, any homomorphism R →+* S can be lifted to a homomorphism R →+* Perfection S p.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                theorem Perfection.hom_ext (p : ) [hp : Fact (Nat.Prime p)] {R : Type u₁} [CommSemiring R] [CharP R p] [PerfectRing R p] {S : Type u₂} [CommSemiring S] [CharP S p] {f : R →+* Ring.Perfection S p} {g : R →+* Ring.Perfection S p} (hfg : ∀ (x : R), (Perfection.coeff S p 0) (f x) = (Perfection.coeff S p 0) (g x)) :
                f = g
                @[simp]
                theorem Perfection.map_apply_coe {R : Type u₁} [CommSemiring R] (p : ) [hp : Fact (Nat.Prime p)] [CharP R p] {S : Type u₂} [CommSemiring S] [CharP S p] (φ : R →+* S) (f : Ring.Perfection R p) (n : ) :
                ((Perfection.map p φ) f) n = φ ((Perfection.coeff R p n) f)
                def Perfection.map {R : Type u₁} [CommSemiring R] (p : ) [hp : Fact (Nat.Prime p)] [CharP R p] {S : Type u₂} [CommSemiring S] [CharP S p] (φ : R →+* S) :

                A ring homomorphism R →+* S induces Perfection R p →+* Perfection S p.

                Equations
                Instances For
                  theorem Perfection.coeff_map {R : Type u₁} [CommSemiring R] (p : ) [hp : Fact (Nat.Prime p)] [CharP R p] {S : Type u₂} [CommSemiring S] [CharP S p] (φ : R →+* S) (f : Ring.Perfection R p) (n : ) :
                  (Perfection.coeff S p n) ((Perfection.map p φ) f) = φ ((Perfection.coeff R p n) f)
                  structure PerfectionMap (p : ) [Fact (Nat.Prime p)] {R : Type u₁} [CommSemiring R] [CharP R p] {P : Type u₂} [CommSemiring P] [CharP P p] [PerfectRing P p] (π : P →+* R) :

                  A perfection map to a ring of characteristic p is a map that is isomorphic to its perfection.

                  Instances For
                    theorem PerfectionMap.injective {p : } [Fact (Nat.Prime p)] {R : Type u₁} [CommSemiring R] [CharP R p] {P : Type u₂} [CommSemiring P] [CharP P p] [PerfectRing P p] {π : P →+* R} (self : PerfectionMap p π) ⦃x : P ⦃y : P :
                    (∀ (n : ), π (((frobeniusEquiv P p).symm)^[n] x) = π (((frobeniusEquiv P p).symm)^[n] y))x = y
                    theorem PerfectionMap.surjective {p : } [Fact (Nat.Prime p)] {R : Type u₁} [CommSemiring R] [CharP R p] {P : Type u₂} [CommSemiring P] [CharP P p] [PerfectRing P p] {π : P →+* R} (self : PerfectionMap p π) (f : R) :
                    (∀ (n : ), f (n + 1) ^ p = f n)∃ (x : P), ∀ (n : ), π (((frobeniusEquiv P p).symm)^[n] x) = f n
                    theorem PerfectionMap.mk' {p : } [Fact (Nat.Prime p)] {R : Type u₁} [CommSemiring R] [CharP R p] {P : Type u₃} [CommSemiring P] [CharP P p] [PerfectRing P p] {f : P →+* R} (g : P ≃+* Ring.Perfection R p) (hfg : (Perfection.lift p P R) f = g) :

                    Create a PerfectionMap from an isomorphism to the perfection.

                    theorem PerfectionMap.of (p : ) [Fact (Nat.Prime p)] (R : Type u₁) [CommSemiring R] [CharP R p] :

                    The canonical perfection map from the perfection of a ring.

                    theorem PerfectionMap.id (p : ) [Fact (Nat.Prime p)] (R : Type u₁) [CommSemiring R] [CharP R p] [PerfectRing R p] :

                    For a perfect ring, it itself is the perfection.

                    noncomputable def PerfectionMap.equiv {p : } [Fact (Nat.Prime p)] {R : Type u₁} [CommSemiring R] [CharP R p] {P : Type u₃} [CommSemiring P] [CharP P p] [PerfectRing P p] {π : P →+* R} (m : PerfectionMap p π) :

                    A perfection map induces an isomorphism to the perfection.

                    Equations
                    Instances For
                      theorem PerfectionMap.equiv_apply {p : } [Fact (Nat.Prime p)] {R : Type u₁} [CommSemiring R] [CharP R p] {P : Type u₃} [CommSemiring P] [CharP P p] [PerfectRing P p] {π : P →+* R} (m : PerfectionMap p π) (x : P) :
                      m.equiv x = ((Perfection.lift p P R) π) x
                      theorem PerfectionMap.comp_equiv {p : } [Fact (Nat.Prime p)] {R : Type u₁} [CommSemiring R] [CharP R p] {P : Type u₃} [CommSemiring P] [CharP P p] [PerfectRing P p] {π : P →+* R} (m : PerfectionMap p π) (x : P) :
                      (Perfection.coeff R p 0) (m.equiv x) = π x
                      theorem PerfectionMap.comp_equiv' {p : } [Fact (Nat.Prime p)] {R : Type u₁} [CommSemiring R] [CharP R p] {P : Type u₃} [CommSemiring P] [CharP P p] [PerfectRing P p] {π : P →+* R} (m : PerfectionMap p π) :
                      (Perfection.coeff R p 0).comp m.equiv = π
                      theorem PerfectionMap.comp_symm_equiv {p : } [Fact (Nat.Prime p)] {R : Type u₁} [CommSemiring R] [CharP R p] {P : Type u₃} [CommSemiring P] [CharP P p] [PerfectRing P p] {π : P →+* R} (m : PerfectionMap p π) (f : Ring.Perfection R p) :
                      π (m.equiv.symm f) = (Perfection.coeff R p 0) f
                      theorem PerfectionMap.comp_symm_equiv' {p : } [Fact (Nat.Prime p)] {R : Type u₁} [CommSemiring R] [CharP R p] {P : Type u₃} [CommSemiring P] [CharP P p] [PerfectRing P p] {π : P →+* R} (m : PerfectionMap p π) :
                      π.comp m.equiv.symm = Perfection.coeff R p 0
                      @[simp]
                      theorem PerfectionMap.lift_apply (p : ) [Fact (Nat.Prime p)] (R : Type u₁) [CommSemiring R] [CharP R p] [PerfectRing R p] (S : Type u₂) [CommSemiring S] [CharP S p] (P : Type u₃) [CommSemiring P] [CharP P p] [PerfectRing P p] (π : P →+* S) (m : PerfectionMap p π) (f : R →+* S) :
                      (PerfectionMap.lift p R S P π m) f = (m.equiv.symm).comp ((Perfection.lift p R S) f)
                      @[simp]
                      theorem PerfectionMap.lift_symm_apply (p : ) [Fact (Nat.Prime p)] (R : Type u₁) [CommSemiring R] [CharP R p] [PerfectRing R p] (S : Type u₂) [CommSemiring S] [CharP S p] (P : Type u₃) [CommSemiring P] [CharP P p] [PerfectRing P p] (π : P →+* S) (m : PerfectionMap p π) (f : R →+* P) :
                      (PerfectionMap.lift p R S P π m).symm f = π.comp f
                      noncomputable def PerfectionMap.lift (p : ) [Fact (Nat.Prime p)] (R : Type u₁) [CommSemiring R] [CharP R p] [PerfectRing R p] (S : Type u₂) [CommSemiring S] [CharP S p] (P : Type u₃) [CommSemiring P] [CharP P p] [PerfectRing P p] (π : P →+* S) (m : PerfectionMap p π) :
                      (R →+* S) (R →+* P)

                      Given rings R and S of characteristic p, with R being perfect, any homomorphism R →+* S can be lifted to a homomorphism R →+* P, where P is any perfection of S.

                      Equations
                      Instances For
                        theorem PerfectionMap.hom_ext {p : } [Fact (Nat.Prime p)] {R : Type u₁} [CommSemiring R] [CharP R p] [PerfectRing R p] {S : Type u₂} [CommSemiring S] [CharP S p] {P : Type u₃} [CommSemiring P] [CharP P p] [PerfectRing P p] (π : P →+* S) (m : PerfectionMap p π) {f : R →+* P} {g : R →+* P} (hfg : ∀ (x : R), π (f x) = π (g x)) :
                        f = g
                        noncomputable def PerfectionMap.map (p : ) [Fact (Nat.Prime p)] {R : Type u₁} [CommSemiring R] [CharP R p] {P : Type u₃} [CommSemiring P] [CharP P p] [PerfectRing P p] {S : Type u₂} [CommSemiring S] [CharP S p] {Q : Type u₄} [CommSemiring Q] [CharP Q p] [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.

                        Equations
                        Instances For
                          theorem PerfectionMap.comp_map (p : ) [Fact (Nat.Prime p)] {R : Type u₁} [CommSemiring R] [CharP R p] {P : Type u₃} [CommSemiring P] [CharP P p] [PerfectRing P p] {S : Type u₂} [CommSemiring S] [CharP S p] {Q : Type u₄} [CommSemiring Q] [CharP Q p] [PerfectRing Q p] {π : P →+* R} (m : PerfectionMap p π) {σ : Q →+* S} (n : PerfectionMap p σ) (φ : R →+* S) :
                          σ.comp (PerfectionMap.map p m n φ) = φ.comp π
                          theorem PerfectionMap.map_map (p : ) [Fact (Nat.Prime p)] {R : Type u₁} [CommSemiring R] [CharP R p] {P : Type u₃} [CommSemiring P] [CharP P p] [PerfectRing P p] {S : Type u₂} [CommSemiring S] [CharP S p] {Q : Type u₄} [CommSemiring Q] [CharP Q p] [PerfectRing Q p] {π : P →+* R} (m : PerfectionMap p π) {σ : Q →+* S} (n : PerfectionMap p σ) (φ : R →+* S) (x : P) :
                          σ ((PerfectionMap.map p m n φ) x) = φ (π x)
                          theorem PerfectionMap.map_eq_map (p : ) [Fact (Nat.Prime p)] {R : Type u₁} [CommSemiring R] [CharP R p] {S : Type u₂} [CommSemiring S] [CharP S p] (φ : R →+* S) :
                          def ModP (K : Type u₁) [Field K] (v : Valuation K NNReal) (O : Type u₂) [CommRing O] [Algebra O K] :
                          v.Integers OType u₂

                          O/(p) for O, ring of integers of K.

                          Equations
                          Instances For
                            instance ModP.commRing (K : Type u₁) [Field K] (v : Valuation K NNReal) (O : Type u₂) [CommRing O] [Algebra O K] (hv : v.Integers O) (p : ) :
                            CommRing (ModP K v O hv p)
                            Equations
                            instance ModP.charP (K : Type u₁) [Field K] (v : Valuation K NNReal) (O : Type u₂) [CommRing O] [Algebra O K] (hv : v.Integers O) (p : ) [hp : Fact (Nat.Prime p)] [hvp : Fact (v p 1)] :
                            CharP (ModP K v O hv p) p
                            Equations
                            • =
                            instance ModP.instNontrivial (K : Type u₁) [Field K] (v : Valuation K NNReal) (O : Type u₂) [CommRing O] [Algebra O K] (hv : v.Integers O) (p : ) [hp : Fact (Nat.Prime p)] [hvp : Fact (v p 1)] :
                            Nontrivial (ModP K v O hv p)
                            Equations
                            • =
                            noncomputable def ModP.preVal (K : Type u₁) [Field K] (v : Valuation K NNReal) (O : Type u₂) [CommRing O] [Algebra O K] (hv : v.Integers O) (p : ) (x : ModP K v O hv p) :

                            For a field K with valuation v : K → ℝ≥0 and ring of integers O, a function O/(p) → ℝ≥0 that sends 0 to 0 and x + (p) to v(x) as long as x ∉ (p).

                            Equations
                            Instances For
                              theorem ModP.preVal_mk {K : Type u₁} [Field K] {v : Valuation K NNReal} {O : Type u₂} [CommRing O] [Algebra O K] {hv : v.Integers O} {p : } {x : O} (hx : (Ideal.Quotient.mk (Ideal.span {p})) x 0) :
                              ModP.preVal K v O hv p ((Ideal.Quotient.mk (Ideal.span {p})) x) = v ((algebraMap O K) x)
                              theorem ModP.preVal_zero {K : Type u₁} [Field K] {v : Valuation K NNReal} {O : Type u₂} [CommRing O] [Algebra O K] {hv : v.Integers O} {p : } :
                              ModP.preVal K v O hv p 0 = 0
                              theorem ModP.preVal_mul {K : Type u₁} [Field K] {v : Valuation K NNReal} {O : Type u₂} [CommRing O] [Algebra O K] {hv : v.Integers O} {p : } {x : ModP K v O hv p} {y : ModP K v O hv p} (hxy0 : x * y 0) :
                              ModP.preVal K v O hv p (x * y) = ModP.preVal K v O hv p x * ModP.preVal K v O hv p y
                              theorem ModP.preVal_add {K : Type u₁} [Field K] {v : Valuation K NNReal} {O : Type u₂} [CommRing O] [Algebra O K] {hv : v.Integers O} {p : } (x : ModP K v O hv p) (y : ModP K v O hv p) :
                              ModP.preVal K v O hv p (x + y) max (ModP.preVal K v O hv p x) (ModP.preVal K v O hv p y)
                              theorem ModP.v_p_lt_preVal {K : Type u₁} [Field K] {v : Valuation K NNReal} {O : Type u₂} [CommRing O] [Algebra O K] {hv : v.Integers O} {p : } {x : ModP K v O hv p} :
                              v p < ModP.preVal K v O hv p x x 0
                              theorem ModP.preVal_eq_zero {K : Type u₁} [Field K] {v : Valuation K NNReal} {O : Type u₂} [CommRing O] [Algebra O K] {hv : v.Integers O} {p : } {x : ModP K v O hv p} :
                              ModP.preVal K v O hv p x = 0 x = 0
                              theorem ModP.v_p_lt_val {K : Type u₁} [Field K] {v : Valuation K NNReal} {O : Type u₂} [CommRing O] [Algebra O K] (hv : v.Integers O) {p : } {x : O} :
                              v p < v ((algebraMap O K) x) (Ideal.Quotient.mk (Ideal.span {p})) x 0
                              theorem ModP.mul_ne_zero_of_pow_p_ne_zero {K : Type u₁} [Field K] {v : Valuation K NNReal} {O : Type u₂} [CommRing O] [Algebra O K] {hv : v.Integers O} {p : } [hp : Fact (Nat.Prime p)] {x : ModP K v O hv p} {y : ModP K v O hv p} (hx : x ^ p 0) (hy : y ^ p 0) :
                              x * y 0
                              def PreTilt (K : Type u₁) [Field K] (v : Valuation K NNReal) (O : Type u₂) [CommRing O] [Algebra O K] (hv : v.Integers O) (p : ) :
                              Type u₂

                              Perfection of O/(p) where O is the ring of integers of K.

                              Equations
                              Instances For
                                instance PreTilt.instCommRing (K : Type u₁) [Field K] (v : Valuation K NNReal) (O : Type u₂) [CommRing O] [Algebra O K] (hv : v.Integers O) (p : ) [hp : Fact (Nat.Prime p)] [hvp : Fact (v p 1)] :
                                CommRing (PreTilt K v O hv p)
                                Equations
                                instance PreTilt.instCharP (K : Type u₁) [Field K] (v : Valuation K NNReal) (O : Type u₂) [CommRing O] [Algebra O K] (hv : v.Integers O) (p : ) [hp : Fact (Nat.Prime p)] [hvp : Fact (v p 1)] :
                                CharP (PreTilt K v O hv p) p
                                Equations
                                • =
                                noncomputable def PreTilt.valAux (K : Type u₁) [Field K] (v : Valuation K NNReal) (O : Type u₂) [CommRing O] [Algebra O K] (hv : v.Integers O) (p : ) [hp : Fact (Nat.Prime p)] [hvp : Fact (v p 1)] (f : PreTilt K v O hv p) :

                                The valuation Perfection(O/(p)) → ℝ≥0 as a function. Given f ∈ Perfection(O/(p)), if f = 0 then output 0; otherwise output preVal(f(n))^(p^n) for any n such that f(n) ≠ 0.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  theorem PreTilt.coeff_nat_find_add_ne_zero {K : Type u₁} [Field K] {v : Valuation K NNReal} {O : Type u₂} [CommRing O] [Algebra O K] {hv : v.Integers O} {p : } [hp : Fact (Nat.Prime p)] [hvp : Fact (v p 1)] {f : PreTilt K v O hv p} {h : ∃ (n : ), (Perfection.coeff (ModP K v O hv p) p n) f 0} (k : ) :
                                  (Perfection.coeff (ModP K v O hv p) p (Nat.find h + k)) f 0
                                  theorem PreTilt.valAux_eq {K : Type u₁} [Field K] {v : Valuation K NNReal} {O : Type u₂} [CommRing O] [Algebra O K] {hv : v.Integers O} {p : } [hp : Fact (Nat.Prime p)] [hvp : Fact (v p 1)] {f : PreTilt K v O hv p} {n : } (hfn : (Perfection.coeff (ModP K v O hv p) p n) f 0) :
                                  PreTilt.valAux K v O hv p f = ModP.preVal K v O hv p ((Perfection.coeff (ModP K v O hv p) p n) f) ^ p ^ n
                                  theorem PreTilt.valAux_zero {K : Type u₁} [Field K] {v : Valuation K NNReal} {O : Type u₂} [CommRing O] [Algebra O K] {hv : v.Integers O} {p : } [hp : Fact (Nat.Prime p)] [hvp : Fact (v p 1)] :
                                  PreTilt.valAux K v O hv p 0 = 0
                                  theorem PreTilt.valAux_one {K : Type u₁} [Field K] {v : Valuation K NNReal} {O : Type u₂} [CommRing O] [Algebra O K] {hv : v.Integers O} {p : } [hp : Fact (Nat.Prime p)] [hvp : Fact (v p 1)] :
                                  PreTilt.valAux K v O hv p 1 = 1
                                  theorem PreTilt.valAux_mul {K : Type u₁} [Field K] {v : Valuation K NNReal} {O : Type u₂} [CommRing O] [Algebra O K] {hv : v.Integers O} {p : } [hp : Fact (Nat.Prime p)] [hvp : Fact (v p 1)] (f : PreTilt K v O hv p) (g : PreTilt K v O hv p) :
                                  PreTilt.valAux K v O hv p (f * g) = PreTilt.valAux K v O hv p f * PreTilt.valAux K v O hv p g
                                  theorem PreTilt.valAux_add {K : Type u₁} [Field K] {v : Valuation K NNReal} {O : Type u₂} [CommRing O] [Algebra O K] {hv : v.Integers O} {p : } [hp : Fact (Nat.Prime p)] [hvp : Fact (v p 1)] (f : PreTilt K v O hv p) (g : PreTilt K v O hv p) :
                                  PreTilt.valAux K v O hv p (f + g) max (PreTilt.valAux K v O hv p f) (PreTilt.valAux K v O hv p g)
                                  noncomputable def PreTilt.val (K : Type u₁) [Field K] (v : Valuation K NNReal) (O : Type u₂) [CommRing O] [Algebra O K] (hv : v.Integers O) (p : ) [hp : Fact (Nat.Prime p)] [hvp : Fact (v p 1)] :
                                  Valuation (PreTilt K v O hv p) NNReal

                                  The valuation Perfection(O/(p)) → ℝ≥0. Given f ∈ Perfection(O/(p)), if f = 0 then output 0; otherwise output preVal(f(n))^(p^n) for any n such that f(n) ≠ 0.

                                  Equations
                                  • PreTilt.val K v O hv p = { toFun := PreTilt.valAux K v O hv p, map_zero' := , map_one' := , map_mul' := , map_add_le_max' := }
                                  Instances For
                                    theorem PreTilt.map_eq_zero {K : Type u₁} [Field K] {v : Valuation K NNReal} {O : Type u₂} [CommRing O] [Algebra O K] {hv : v.Integers O} {p : } [hp : Fact (Nat.Prime p)] [hvp : Fact (v p 1)] {f : PreTilt K v O hv p} :
                                    (PreTilt.val K v O hv p) f = 0 f = 0
                                    instance PreTilt.instIsDomain (K : Type u₁) [Field K] (v : Valuation K NNReal) (O : Type u₂) [CommRing O] [Algebra O K] (hv : v.Integers O) (p : ) [hp : Fact (Nat.Prime p)] [hvp : Fact (v p 1)] :
                                    IsDomain (PreTilt K v O hv p)
                                    Equations
                                    • =
                                    def Tilt (K : Type u₁) [Field K] (v : Valuation K NNReal) (O : Type u₂) [CommRing O] [Algebra O K] (hv : v.Integers O) (p : ) [hp : Fact (Nat.Prime p)] [hvp : Fact (v p 1)] :
                                    Type u₂

                                    The tilt of a field, as defined in Perfectoid Spaces by Peter Scholze, as in [scholze2011perfectoid]. Given a field K with valuation K → ℝ≥0 and ring of integers O, this is implemented as the fraction field of the perfection of O/(p).

                                    Equations
                                    Instances For
                                      noncomputable instance Tilt.instField (K : Type u₁) [Field K] (v : Valuation K NNReal) (O : Type u₂) [CommRing O] [Algebra O K] (hv : v.Integers O) (p : ) [hp : Fact (Nat.Prime p)] [hvp : Fact (v p 1)] :
                                      Field (Tilt K v O hv p)
                                      Equations