Banach algebras

The declarations the status of Tau Ceti's roadmap names, and the other results named in the modules where only this status names declarations, or in folders below the areas where only it names 2 or more, as Tau Ceti has them at commit ace60277.

TheoremCohen–Hewitt factorization#

Let A be a Banach algebra with a left approximate identity l bounded by C, acting boundedly on the left of a Banach space E through L. Every x in the essential part closure (span (A · E)) factors as x = L a y with ‖a‖ ≤ C, where y lies in the closure of A · x and within any prescribed distance ε of x.

ContinuousLinearMap.exists_apply_eq_of_mem_topologicalClosure_span.{u_1, u_2, u_3} {𝕜 : Type u_1}
  {A : Type u_2} {E : Type u_3} [RCLike 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A]
  [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [CompleteSpace A] [NormedAddCommGroup E]
  [NormedSpace 𝕜 E] [CompleteSpace E] (L : A →L[𝕜] E →L[𝕜] E)
  (hL : ∀ (a b : A) (z : E), (L (a * b)) z = (L a) ((L b) z)) {l : Filter A} [l.NeBot] {C : ℝ}
  (hC : ∀ᶠ (e : A) in l, ‖e‖ ≤ C) (hl : ∀ (a : A), Filter.Tendsto (fun x => x * a) l (nhds a))
  {x : E} (hx : x ∈ (Submodule.span 𝕜 (Set.range fun p => (L p.1) p.2)).topologicalClosure) {ε : ℝ}
  (hε : 0 < ε) :
  ∃ a y, ‖a‖ ≤ C ∧ y ∈ closure (Set.range fun b => (L b) x) ∧ ‖y - x‖ < ε ∧ (L a) y = x
Lean

Formalized in Tau Ceti as ContinuousLinearMap.exists_apply_eq_of_mem_topologicalClosure_span.

Sources
LeanContinuousLinearMap.exists_apply_eq_of_mem_topologicalClosure_span
Uses 1 · Used by 1
Proof usesContinuousLinearMap.unitizationAction
Used byCohen's factorization theorem for Banach algebras

TheoremSinclair's stability lemma#

Let E n and F be Banach spaces, let R n : E (n + 1) → E n be continuous linear maps, and let T n : E n →ₗ F be linear maps, not assumed continuous, with T (n + 1) = T n ∘ R n, so that T n = T 0 ∘ R 0 ∘ ⋯ ∘ R (n - 1). Then the decreasing sequence of separating spaces of the T n is eventually constant.

TauCeti.eventuallyConst_separatingSpace.{u_1, u_2, u_3} {𝕜 : Type u_1} {F : Type u_2}
  [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : ℕ → Type u_3}
  [(n : ℕ) → NormedAddCommGroup (E n)] [(n : ℕ) → NormedSpace 𝕜 (E n)]
  {R : (n : ℕ) → E (n + 1) →L[𝕜] E n} [CompleteSpace F] [∀ (n : ℕ), CompleteSpace (E n)]
  {T : (n : ℕ) → E n →ₗ[𝕜] F} (hT : ∀ (n : ℕ), T (n + 1) = T n ∘ₗ ↑(R n)) :
  Filter.EventuallyConst (fun n => (T n).separatingSpace) Filter.atTop
Lean

Formalized in Tau Ceti as TauCeti.eventuallyConst_separatingSpace.

Sources
LeanTauCeti.eventuallyConst_separatingSpace
Uses 1 · Used by 2
Statement usesLinearMap.separatingSpace
Used byJohnson–Sinclair theorem, nonunital form · Johnson's theorem

TheoremLinearMap.continuous_iff_separatingSpace_eq_bot#

A linear map between Banach spaces is continuous if and only if its separating space is trivial.

LinearMap.continuous_iff_separatingSpace_eq_bot.{u_1, u_2, u_3} {𝕜 : Type u_1} {E : Type u_2}
  {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  [NormedAddCommGroup F] [NormedSpace 𝕜 F] (T : E →ₗ[𝕜] F) [CompleteSpace E] [CompleteSpace F] :
  Continuous ⇑T ↔ T.separatingSpace = ⊥
Lean

Formalized in Tau Ceti as LinearMap.continuous_iff_separatingSpace_eq_bot.

Sources
LeanLinearMap.continuous_iff_separatingSpace_eq_bot
Uses 1 · Used by 3
Statement usesLinearMap.separatingSpace
Used byJohnson–Sinclair theorem, nonunital form · Johnson's theorem · Šilov's theorem

TheoremTauCeti.Ring.mem_jacobson_iff_forall_gelfandRadius_mul_eq_zero#

An element of a complex Banach algebra lies in its Jacobson radical exactly when every left multiple b * a is quasinilpotent, that is, ‖(b * a) ^ n‖ ^ (1 / n) tends to zero.

TauCeti.Ring.mem_jacobson_iff_forall_gelfandRadius_mul_eq_zero.{u_3} {B : Type u_3} [NormedRing B]
  [NormedAlgebra ℂ B] [CompleteSpace B] {a : B} :
  a ∈ Ring.jacobson B ↔ ∀ (b : B), gelfandRadius (b * a) = 0
Lean

Formalized in Tau Ceti as TauCeti.Ring.mem_jacobson_iff_forall_gelfandRadius_mul_eq_zero.

Sources
LeanTauCeti.Ring.mem_jacobson_iff_forall_gelfandRadius_mul_eq_zero

TheoremThe homology Cauchy theorem for contour cycles#

Let C be a finite formal integer combination of closed piecewise-C¹ curves whose trace lies in an open set U. If C is null-homologous in U and f is holomorphic on U, with values in any complex normed space, then the contour integral of f over the whole cycle vanishes.

The null-homology assumption is imposed only on C, not on each supported curve, so the theorem includes cancellations between different generators.

TauCeti.Contour.Cycle.homologyCauchyTheorem.{u_1} {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace ℂ E] {f : ℂ → E} {C : TauCeti.Contour.Cycle} {U : Set ℂ} (hU : IsOpen U)
  (hCU : C.IsIn U) (hf : DifferentiableOn ℂ f U) (hnull : C.IsNullHomologous U) :
  (TauCeti.Contour.Cycle.integral f) C = 0
Lean

Formalized in Tau Ceti as TauCeti.Contour.Cycle.homologyCauchyTheorem.

Sources
LeanTauCeti.Contour.Cycle.homologyCauchyTheorem
Uses 2 · Used by 3
Statement usesGeneralized winding number (HW Def 2.1) · TauCeti.Contour.Cycle
Used byThe classical residue theorem for a null-homologous contour cycle · The Hungerbühler–Wasem generalized residue theorem for a contour cycle (HW Thm 3.3) · Cauchy's theorem on a disc

DefinitionLinearMap.separatingSpace#

The separating space of a linear map T : E →ₗ[R] F between topological modules: the vertical fibre over 0 of the closure of the graph of T. For first countable spaces it consists of the limits of T xₙ along sequences xₙ → 0 (LinearMap.mem_separatingSpace_iff_exists_seq).

LinearMap.separatingSpace.{u_1, u_3, u_4} {R : Type u_1} {E : Type u_3} {F : Type u_4} [Ring R]
  [AddCommGroup E] [_root_.Module R E] [TopologicalSpace E] [IsTopologicalAddGroup E]
  [ContinuousConstSMul R E] [AddCommGroup F] [_root_.Module R F] [TopologicalSpace F]
  [IsTopologicalAddGroup F] [ContinuousConstSMul R F] (T : E →ₗ[R] F) : Submodule R F
Lean

Formalized in Tau Ceti as LinearMap.separatingSpace.

Sources
LeanLinearMap.separatingSpace
Used by 5
Used byLinearMap.continuous_iff_separatingSpace_eq_bot · Sinclair's stability lemma · Johnson–Sinclair theorem, nonunital form · Johnson's theorem · Šilov's theorem

DefinitionTauCeti.nonUnitalJacobson#

The Jacobson radical of a nonunital algebra, defined through its external unitization.

TauCeti.nonUnitalJacobson.{u_1, u_2} (R : Type u_1) (A : Type u_2) [CommRing R] [NonUnitalRing A]
  [_root_.Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : TwoSidedIdeal A
Lean

Formalized in Tau Ceti as TauCeti.nonUnitalJacobson.

Sources
LeanTauCeti.nonUnitalJacobson
Used by 5
Used byJohnson–Sinclair theorem, nonunital form · Johnson's theorem · Johnson's uniqueness-of-norm theorem · Šilov's theorem · The Singer–Wermer theorem

DefinitionContinuousLinearMap.unitizationAction#

The unital action on E of the ℓ¹ unitization of A extending the left action L.

ContinuousLinearMap.unitizationAction.{u_1, u_2, u_3} {𝕜 : Type u_1} {A : Type u_2} {E : Type u_3}
  [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A]
  [SMulCommClass 𝕜 A A] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (L : A →L[𝕜] E →L[𝕜] E)
  (hL : ∀ (a b : A) (z : E), (L (a * b)) z = (L a) ((L b) z)) :
  WithLp 1 (Unitization 𝕜 A) →ₐ[𝕜] E →L[𝕜] E
Lean

Formalized in Tau Ceti as ContinuousLinearMap.unitizationAction.

Sources
LeanContinuousLinearMap.unitizationAction
Used by 1
Used byCohen–Hewitt factorization

TheoremCohen's factorization theorem for Banach algebras#

if A has a left approximate identity bounded by C, then every element of A is a product a * y with ‖a‖ ≤ C.

TauCeti.exists_mul_eq_of_tendsto_mul_right.{u_1, u_2} {A : Type u_1} [NonUnitalNormedRing A]
  [CompleteSpace A] (𝕜 : Type u_2) [RCLike 𝕜] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A]
  [SMulCommClass 𝕜 A A] {l : Filter A} [l.NeBot] {C : ℝ} (hC : ∀ᶠ (e : A) in l, ‖e‖ ≤ C)
  (hl : ∀ (a : A), Filter.Tendsto (fun x => x * a) l (nhds a)) (x : A) : ∃ a y, ‖a‖ ≤ C ∧ a * y = x
Lean

Formalized in Tau Ceti as TauCeti.exists_mul_eq_of_tendsto_mul_right.

Sources
LeanTauCeti.exists_mul_eq_of_tendsto_mul_right
Uses 1
Proof usesCohen–Hewitt factorization

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.