English
If a closed subalgebra S of a Banach algebra contains an invertible element a, and nearby elements in a filter l are invertible in S, then a is invertible in S.
Русский
Если S — замкнутая подалгебра Банаховой алгебры и содержит обратимый элемент a, а рядом лежащие относительно фильтра l элементы также обратимы в S, то и a обратим в S.
LaTeX
$$IsUnit a ∈ S given ha : IsUnit (a:A) and l ⊆ neighborhoods, hl : ∀ᶠ x∈l, IsUnit x, hl' : l.NeBot → IsUnit a$$
Lean4
/-- Let `S` be a closed subalgebra of a Banach algebra `A`. If `a : S` is invertible in `A`,
and for all `x : S` sufficiently close to `a` within some filter `l`, `x` is invertible in `S`,
then `a` is invertible in `S` as well. -/
theorem _root_.Subalgebra.isUnit_of_isUnit_val_of_eventually {l : Filter S} {a : S} (ha : IsUnit (a : A))
(hla : l ≤ 𝓝 a) (hl : ∀ᶠ x in l, IsUnit x) (hl' : l.NeBot) : IsUnit a :=
by
have hla₂ : Tendsto Ring.inverse (map (val S) l) (𝓝 (↑ha.unit⁻¹ : A)) :=
by
rw [← Ring.inverse_unit]
exact (NormedRing.inverse_continuousAt _).tendsto.comp <| continuousAt_subtype_val.tendsto.comp <| map_mono hla
suffices mem : (↑ha.unit⁻¹ : A) ∈ S
by
refine ⟨⟨a, ⟨(↑ha.unit⁻¹ : A), mem⟩, ?_, ?_⟩, rfl⟩
all_goals ext; simp
apply hS.mem_of_tendsto hla₂
rw [Filter.eventually_map]
apply hl.mono fun x hx ↦ ?_
suffices Ring.inverse (val S x) = (val S ↑hx.unit⁻¹) from this ▸ Subtype.property _
rw [← (hx.map (val S)).unit_spec, Ring.inverse_unit (hx.map (val S)).unit, val]
apply Units.mul_eq_one_iff_inv_eq.mp
simpa [-IsUnit.mul_val_inv] using congr(($hx.mul_val_inv : A))
