Perfection.ext
theorem Perfection.ext :
∀ {R : Type u₁} [inst : CommSemiring R] {p : ℕ} [hp : Fact p.Prime] [inst_1 : CharP R p]
{f g : Ring.Perfection R p}, (∀ (n : ℕ), (Perfection.coeff R p n) f = (Perfection.coeff R p n) g) → f = g
The theorem `Perfection.ext` states that for any commutative semiring `R`, any prime number `p` such that `R` has characteristic `p`, and any two elements `f` and `g` of the perfection of `R` with respect to `p`, if for all natural numbers `n` the `n`-th coefficient of `f` equals the `n`-th coefficient of `g`, then `f` and `g` are equal. In other words, two elements of the perfection of a ring are equal if and only if all their coefficients are equal.
More concisely: In a commutative semiring of characteristic `p`, two elements of its perfection with respect to `p` are equal if and only if their coefficients are equal for all natural numbers.
|
PerfectionMap.of
theorem PerfectionMap.of :
∀ (p : ℕ) [inst : Fact p.Prime] (R : Type u₁) [inst_1 : CommSemiring R] [inst_2 : CharP R p],
PerfectionMap p (Perfection.coeff R p 0)
The theorem `PerfectionMap.of` asserts that for any natural number `p` which is prime, in any commutative semiring `R` of characteristic `p`, the operation that gives the zero-th coefficient is a perfection map from the perfection of the ring `R` to `R`. In other words, the zero-th coefficient function serves as a canonical perfection map from the perfection of a ring of characteristic `p` to the ring itself.
More concisely: For any prime number p and commutative semiring R of characteristic p, the zero-th coefficient function serves as the perfection map from the perfection of R to R.
|
PerfectionMap.mk'
theorem PerfectionMap.mk' :
∀ {p : ℕ} [inst : Fact p.Prime] {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] {f : P →+* R}
(g : P ≃+* Ring.Perfection R p), (Perfection.lift p P R) f = ↑g → PerfectionMap p f
The theorem `PerfectionMap.mk'` states that for any prime number `p`, given a commutative semiring `R` with characteristic `p`, another commutative semiring `P` also with characteristic `p` that is a perfect ring, a ring homomorphism `f` from `P` to `R`, and an isomorphism `g` from `P` to the perfection of `R`, if the lift of `f` to the perfection of `R` equals `g`, then `f` is a perfection map. In simpler terms, it establishes a condition under which a ring homomorphism is a perfection map, i.e., a map that commutes with the Frobenius endomorphism.
More concisely: Given a prime number `p`, commutative semirings `R` and `P` of characteristic `p` with `P` being perfect, a ring homomorphism `f` from `P` to `R`, and an isomorphism `g` from `P` to the perfection of `R`, if `g = f⁛` (the lift of `f` to the perfection of `R`), then `f` is a perfection map.
|
PerfectionMap.id
theorem PerfectionMap.id :
∀ (p : ℕ) [inst : Fact p.Prime] (R : Type u₁) [inst_1 : CommSemiring R] [inst_2 : CharP R p]
[inst_3 : PerfectRing R p], PerfectionMap p (RingHom.id R)
This theorem states that for any perfect ring `R` of characteristic `p` (where `p` is a prime number), the identity function from `R` to itself is a perfection map. In other words, in the context of perfect rings (which are rings with certain properties related to the Frobenius endomorphism), the identity ring homomorphism serves as the perfection map, mapping the ring to its own perfection. This is a key property in the study of perfect rings in algebra.
More concisely: For any perfect ring `R` of characteristic `p`, the identity map `id : R → R` is a perfection map.
|
Perfection.coeff_frobenius
theorem Perfection.coeff_frobenius :
∀ {R : Type u₁} [inst : CommSemiring R] {p : ℕ} [hp : Fact p.Prime] [inst_1 : 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
The theorem `Perfection.coeff_frobenius` states that for any commutative semiring `R` and prime number `p` (where `R` has characteristic `p`), and for any element `f` of the 'perfection' of `R` (a structure related to the limit of repeated applications of the Frobenius map `x ↦ x^p`), and any natural number `n`, the `n`-th coefficient of the Frobenius image of `f` is equal to the `(n+1)`-th coefficient of `f`. In other words, applying the Frobenius map and then taking the `n`-th coefficient is the same as taking the `(n+1)`-th coefficient of the original element.
More concisely: For any commutative semiring R of characteristic p, prime number p, and perfection element f, the n-th coefficient of the Frobenius image of f is equal to the (n+1)-th coefficient of f.
|