Commit 2024-02-02 21:03 96a6d295

View on Github →

refactor: generalize CharP+Prime to ExpChar in frobenius (#10016) Consequently, the part about frobenius in Algebra/CharP/Basic is moved to CharP/ExpChar, and imports are adjusted as necessary.

  • Add instances from CharP+Fact(Nat.Prime) and CharZero to ExpChar, to allow lemmas generalized to ExpChar still apply to CharP.
  • Remove lemmas in Algebra/CharP/ExpChar from [#9799](https://github.com/leanprover-community/mathlib4/commit/1e74fcfff8d5ffe5a3a9881864cf10fa39f619e6) because they coincide with the generalized lemmas, and golf the other lemmas (in Algebra/CharP/Basic).
  • Define the RingHom iterateFrobenius and the semilinear map LinearMap.(iterate)Frobenius for an algebra. When the characteristic is zero (ExpChar is 1), these are all equal to the identity map (· ^ 1). Also define iterateFrobeniusEquiv for perfect rings.
  • Fix and/or generalize other files.

Estimated changes

deleted theorem MonoidHom.map_frobenius
deleted theorem RingHom.map_frobenius
deleted def frobenius
deleted theorem frobenius_add
deleted theorem frobenius_def
deleted theorem frobenius_mul
deleted theorem frobenius_nat_cast
deleted theorem frobenius_neg
deleted theorem frobenius_one
deleted theorem frobenius_sub
deleted theorem frobenius_zero
deleted theorem iterate_frobenius
deleted theorem list_sum_pow_char
deleted theorem list_sum_pow_char_pow
deleted theorem multiset_sum_pow_char
deleted theorem multiset_sum_pow_char_pow
deleted theorem sum_pow_char
deleted theorem sum_pow_char_pow
added theorem RingHom.map_frobenius
added theorem coe_iterateFrobenius
added def frobenius
added theorem frobenius_add
added theorem frobenius_def
added theorem frobenius_mul
added theorem frobenius_nat_cast
added theorem frobenius_neg
added theorem frobenius_one
added theorem frobenius_sub
added theorem frobenius_zero
added def iterateFrobenius
added theorem iterateFrobenius_add
added theorem iterateFrobenius_def
added theorem iterateFrobenius_one
added theorem iterateFrobenius_zero
added theorem iterate_frobenius
added theorem list_sum_pow_char
added theorem list_sum_pow_char_pow
deleted theorem list_sum_pow_expChar
deleted theorem list_sum_pow_expChar_pow
added theorem multiset_sum_pow_char
deleted theorem multiset_sum_pow_expChar
added theorem sum_pow_char
added theorem sum_pow_char_pow
deleted theorem sum_pow_expChar
deleted theorem sum_pow_expChar_pow
modified theorem frobenius_inj
modified theorem Polynomial.expand_contract
modified theorem PerfectRing.ofSurjective
modified theorem not_irreducible_expand