copyBase_eq — Mathlib

English

If two base maps agree, copying with that base gives back the original morphism.

Русский

Если две базовые мапы совпадают, копирование с этой базой возвращает исходный морфизм.

LaTeX

$$$ f.copyBase\, g\, h = f \quad\text{whenever } h:\ f. base = g. $$$

Lean4

theorem copyBase_eq {X Y : Scheme} (f : X.Hom Y) (g : X → Y) (h : f.base = g) : f.copyBase g h = f :=
  by
  subst h
  obtain ⟨⟨⟨f₁, f₂⟩, f₃⟩, f₄⟩ := f
  simp only [Hom.copyBase, LocallyRingedSpace.Hom.toShHom_mk]
  congr
  cat_disch

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