sigmaMk_mk — Mathlib

English

For isotopes i and x, sigmaMk f maps mk i x to the base correspondence with Sigma.ι f i.

Русский

Для элемента i и x отображение sigmaMk f переведено к базовой карте через Sigma.ι f i.

LaTeX

$$$\\sigmaMk f (\\.mk\, i\, x) = (\\Sigma.ι f i).\\text{base} x$$$

Lean4

@[simp]
theorem sigmaMk_mk (i) (x : f i) : sigmaMk f (.mk i x) = (Sigma.ι f i).base x :=
  by
  change
    ((TopCat.sigmaCofan (fun x ↦ (f x).toTopCat)).inj i ≫
          (colimit.isoColimitCocone ⟨_, TopCat.sigmaCofanIsColimit _⟩).inv ≫ _)
        x =
      Scheme.forgetToTop.map (Sigma.ι f i) x
  congr 2
  refine (colimit.isoColimitCocone_ι_inv_assoc ⟨_, TopCat.sigmaCofanIsColimit _⟩ _ _).trans ?_
  exact ι_comp_sigmaComparison Scheme.forgetToTop _ _

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