sigmaFunctor — Mathlib

Lean4
/-- Collapsing a cover to a single object cover is functorial. -/
@[simps]
noncomputable def sigmaFunctor : S.Cover (precoverage P) ⥤ S.Cover (precoverage P)
    where
  obj 𝒰 := 𝒰.sigma
  map f := f.sigma
  map_id
    𝒰 :=
    Scheme.Cover.Hom.ext rfl <|
      by
      simp only [sigma_I₀, sigma_X, Hom.sigma_idx, PUnit.default_eq_unit, id_idx_apply, heq_eq_eq]
      ext j : 1
      exact Sigma.hom_ext _ _ (by simp)
  map_comp f
    g :=
    Scheme.Cover.Hom.ext rfl <|
      by
      simp only [sigma_I₀, sigma_X, Hom.sigma_idx, PUnit.default_eq_unit, comp_idx_apply, heq_eq_eq]
      ext j : 1
      exact Sigma.hom_ext _ _ (by simp)
Похожие утверждения