instEpiTopCatBaseCommRingCatFromGlued

English

The base map of fromGlued is an epimorphism in the TopCat sense (surjective on points).

Русский

Базовое отображение fromGlued является эпиморфизмом в смысле TopCat (сюръективно на точках).

LaTeX

$$$$ \text{base} : \text{fromGlued}_{\text{base}} \text{ is epi}. $$$$

Lean4

instance : Epi 𝒰.fromGlued.base := by
  rw [TopCat.epi_iff_surjective]
  intro x
  obtain ⟨y, h⟩ := 𝒰.covers x
  use (𝒰.gluedCover.ι (𝒰.idx x)).base y
  rw [← ConcreteCategory.comp_apply]
  rw [← 𝒰.ι_fromGlued (𝒰.idx x)] at h
  exact h

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