hasOfPostcompProperty_monomorphisms

English

A second formulation of the pullback map stability under base change and composition; the result expresses how P interacts with pullback.map.

Русский

Вторая формулировка устойчивости отображения pullback_map под базовым изменением и композиции; результат описывает взаимодействие P с pullback.map.

LaTeX

$$PullbackMapStableUnderBaseChange$$

Lean4

instance hasOfPostcompProperty_monomorphisms [P.IsStableUnderBaseChange] :
    P.HasOfPostcompProperty (MorphismProperty.monomorphisms C) where
  of_postcomp {X Y Z} f g (hg : Mono g)
    hcomp :=
    by
    have : f = (asIso (pullback.fst (f ≫ g) g)).inv ≫ pullback.snd (f ≫ g) g := by
      simp [← cancel_mono g, pullback.condition]
    rw [this, cancel_left_of_respectsIso (P := P)]
    exact P.pullback_snd _ _ hcomp

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