PerfectClosure.mk_mul_mk
theorem PerfectClosure.mk_mul_mk :
∀ (K : Type u) [inst : CommRing K] (p : ℕ) [inst_1 : Fact p.Prime] [inst_2 : CharP K p] (x 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)
The theorem `PerfectClosure.mk_mul_mk` asserts that for any commutative ring `K`, prime number `p`, and pair of elements `x` and `y` from the cartesian product of natural numbers and `K`, the multiplication of the perfect closures of `x` and `y` is equal to the perfect closure of a pair. This pair is constructed from the sum of the first elements of `x` and `y`, and a product involving the Frobenius map applied to the second elements of `x` and `y`, where the Frobenius map is iteratively applied a number of times equal to the first element of the pair to each of the second elements of the pairs, respectively. In other words, if `x = (n, a)` and `y = (m, b)`, then the product of the perfect closures of `x` and `y` is equal to the perfect closure of `(n+m, a^p^m * b^p^n)`.
More concisely: For any commutative ring K, prime number p, and pairs x = (n, a) and y = (m, b) in the cartesian product of natural numbers and K, the perfect closure of x \* y is equal to the perfect closure of (n + m, a^p^m \* b^p^n).
|
PerfectClosure.mk_eq_iff
theorem PerfectClosure.mk_eq_iff :
∀ (K : Type u) [inst : CommRing K] (p : ℕ) [inst_1 : Fact p.Prime] [inst_2 : CharP K p] (x 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
The theorem `PerfectClosure.mk_eq_iff` states that for any commutative ring `K`, prime number `p`, and pairs of natural number and element of `K` denoted as `x` and `y`, the equality of `PerfectClosure.mk K p x` and `PerfectClosure.mk K p y` is equivalent to the existence of a natural number `z` such that applying the Frobenius map `p` times to `x.2` incremented by `y.1` and `z` times is equal to applying the Frobenius map `p` times to `y.2` incremented by `x.1` and `z` times.
In mathematical terms, this means that two elements in the perfect closure of a commutative ring are equal if and only if there exists a natural number such that the p-th power Frobenius map applied to the second element of the first pair, raised to the power of the sum of the first element of the second pair and the natural number, is equal to the p-th power Frobenius map applied to the second element of the second pair, raised to the sum of the first element of the first pair and the natural number.
More concisely: For any commutative ring K and prime number p, two elements in the perfect closure of K with respect to p are equal if and only if their second components differ by a natural number z such that (Frobenius^p(k.2 + z))^(p+1) = (Frobenius^p(l.2 + z))^(p+1), where k and l are the given pairs and Frobenius denotes the p-th power map.
|