sigma_ι_isOpenImmersion — Mathlib

English

An auxiliary version of the previous statement showing an open embedding for the colimit injection base.

Русский

Вспомогательная версия предыдущего утверждения, показывающая открытое вложение для базовой инъекции колимитa.

LaTeX

$$$\text{OpenEmbedding}(\text{colimit.ι } F i)^{base}$$$

Lean4

instance sigma_ι_isOpenImmersion {ι : Type w} [Small.{v} ι] (F : Discrete ι ⥤ SheafedSpace.{_, v, v} C) [HasColimit F]
    (i : Discrete ι) [HasStrictTerminalObjects C] : SheafedSpace.IsOpenImmersion (colimit.ι F i) :=
  by
  obtain ⟨ι', ⟨e⟩⟩ := Small.equiv_small (α := ι)
  let f : Discrete ι' ≌ Discrete ι := Discrete.equivalence e.symm
  have :
    colimit.ι F i =
      (colimit.ι F i ≫ (HasColimit.isoOfEquivalence f (Iso.refl _)).inv) ≫
        (HasColimit.isoOfEquivalence f (Iso.refl _)).hom :=
    by simp
  rw [this, HasColimit.isoOfEquivalence_inv_π]
  infer_instance

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