isClosedEmbedding_cfcₙHom_of_cfcHom

English

The embedding cfc_nHom_of_cfcHom is a closed embedding (in the appropriate topology).

Русский

Вспомогательное вложение cfc_nHom_of_cfcHom является замкнутым вложением.

LaTeX

$$$$ \\text{IsClosedEmbedding}(cfc\\!_nHom\\_of\\_cfcHom\\ ha) $$$$

Lean4

theorem isClosedEmbedding_cfcₙHom_of_cfcHom {a : A} (ha : p a) : IsClosedEmbedding (cfcₙHom_of_cfcHom R ha) :=
  by
  let f : C(spectrum R a, σₙ R a) := ⟨_, continuous_inclusion <| spectrum_subset_quasispectrum R a⟩
  refine (cfcHom_isClosedEmbedding ha).comp <| (IsUniformInducing.isUniformEmbedding ⟨?_⟩).isClosedEmbedding
  have :=
    uniformSpace_eq_inf_precomp_of_cover (β := R) f (0 : C(Unit, σₙ R a)) (map_continuous f).isProperMap
        (map_continuous 0).isProperMap <|
      by
      simp only [← Subtype.val_injective.image_injective.eq_iff, f, ContinuousMap.coe_mk, ContinuousMap.coe_zero,
        range_zero, image_union, image_singleton, quasispectrum.coe_zero, ← range_comp, val_comp_inclusion, image_univ,
        Subtype.range_coe, quasispectrum_eq_spectrum_union_zero]
  simp_rw [ContinuousMapZero.instUniformSpace, this, uniformity_comap, @inf_uniformity _ (.comap _ _) (.comap _ _),
    uniformity_comap, Filter.comap_inf, Filter.comap_comap]
  refine .symm <| inf_eq_left.mpr <| le_top.trans <| eq_top_iff.mp ?_
  have : ∀ U ∈ 𝓤 (C(Unit, R)), (0, 0) ∈ U := fun U hU ↦ refl_mem_uniformity hU
  convert Filter.comap_const_of_mem this with ⟨u, v⟩ <;> ext ⟨x, rfl⟩ <;> [exact map_zero u; exact map_zero v]

Похожие утверждения