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 _ _