Commit 2022-04-22 01:34 1da12b57

View on Github →

fix(analysis/normed_space/basic): allow the zero ring to be a normed algebra (#13544) This replaces norm_algebra_map_eq : ∀ x : 𝕜, ∥algebra_map 𝕜 𝕜' x∥ = ∥x∥ with norm_smul_le : ∀ (r : 𝕜) (x : 𝕜'), ∥r • x∥ ≤ ∥r∥ * ∥x∥ in normed_algebra. With this change, normed_algebra means nothing more than "a normed module that is also an algebra", which seems to be the only notion actually used in mathlib anyway. In practice, this change really just removes any constraints on ∥1∥. The old meaning of [normed_algebra R A] is now achieved with [normed_algebra R A] [norm_one_class A]. As a result, lemmas like normed_algebra.norm_one_class and normed_algebra.nontrivial have been removed, as they no longer make sense now that the two typeclasses are entirely orthogonal. Notably this means that the following normed_algebra instances hold more generally than before:

  • continuous_linear_map.to_normed_algebra
  • pi.normed_algebra
  • bounded_continuous_function.normed_algebra
  • continuous_map.normed_algebra
  • Instances not yet in mathlib:
    • Matrices under the L1-L_inf norm are a normed algebra even if the matrix is empty
    • Matrices under the frobenius norm are a normed algebra (note ∥(1 : matrix n n 𝕜')∥ = \sqrt (fintype.card n) with that norm) This last one is the original motivation for this PR; otherwise every lemma about a matrix exponential has to case on whether the matrices are empty. It is possible that some of the [norm_one_class A]s added in spectrum.lean are unnecessary; however, the assumptions are no stronger than they were before, and I'm not interested in trying to generalize them as part of this PR. Zulip

Estimated changes

modified def algebra_map_clm
modified theorem algebra_map_clm_coe
modified theorem algebra_map_isometry
added theorem nnnorm_algebra_map'
added theorem nnnorm_algebra_map
deleted theorem nnorm_algebra_map_eq
added theorem norm_algebra_map'
added theorem norm_algebra_map
deleted theorem norm_algebra_map_eq
deleted theorem normed_algebra.nontrivial
deleted theorem normed_algebra.norm_one