pullbackHom_map — Mathlib

English

Under base-change stability assumptions, the pullback morphism commutes with the evaluation on the base, i.e. 𝒰.pullbackHom f i ≫ 𝒰.f i = (𝒰.pullback₁ f).f i ≫ f.

Русский

При условии устойчивости к базовым изменениям, композиция тягодравной морфизмы с 𝒰.f i равна композиции с pullback₁ f и f.

LaTeX

$$$$ 𝒰.pullbackHom f i \;\circ\; 𝒰.f i = (𝒰.pullback₁ f).f i \;\circ\; f $$$$

Lean4

@[reassoc (attr := simp)]
theorem pullbackHom_map [P.IsStableUnderBaseChange] [IsJointlySurjectivePreserving P] {X W : Scheme.{u}}
    (𝒰 : X.Cover (precoverage P)) (f : W ⟶ X) [∀ (x : 𝒰.I₀), HasPullback f (𝒰.f x)] (i) :
    𝒰.pullbackHom f i ≫ 𝒰.f i = (𝒰.pullback₁ f).f i ≫ f :=
  pullback.condition.symm

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