baseChange_map — Mathlib

English

Under base change, the morphism left in the pullback map preserves the property P.

Русский

При базовом изменении левый морфизм в отображении pullback сохраняет свойство P.

LaTeX

$$baseChange_map P$$

Lean4

theorem baseChange_map [IsStableUnderBaseChange P] {S S' : C} (f : S' ⟶ S) [∀ {W} (h : W ⟶ S), HasPullback h f]
    {X Y : Over S} (g : X ⟶ Y) (H : P g.left) : P ((Over.pullback f).map g).left :=
  by
  let e := pullbackRightPullbackFstIso Y.hom f g.left ≪≫ pullback.congrHom (g.w.trans (Category.comp_id _)) rfl
  have : e.inv ≫ (pullback.snd _ _) = ((Over.pullback f).map g).left := by ext <;> dsimp [e] <;> simp
  rw [← this, P.cancel_left_of_respectsIso]
  exact pullback_snd _ _ H

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