baseChange_obj — Mathlib

English

If P is stable under base change, then for objects in Over S, P holds for the pulled-back object’s morphism.

Русский

Если P устойчива к базовому изменению, то при рассмотрении объектов над S свойство P сохраняется для морфизма притянутого обратно объекта.

LaTeX

$$baseChange_obj P$$

Lean4

theorem baseChange_obj [IsStableUnderBaseChange P] {S S' : C} (f : S' ⟶ S) [∀ {W} (h : W ⟶ S), HasPullback h f]
    (X : Over S) (H : P X.hom) : P ((Over.pullback f).obj X).hom :=
  pullback_snd X.hom f H

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