instIsStableUnderBaseChangeScheme

English

Repeat of stability under base change for IsIntegralHom.

Русский

Повтор устойчивости к базовому изменению для IsIntegralHom.

LaTeX

$$instIsStableUnderBaseChangeScheme$$

Lean4

instance [P.IsStableUnderBaseChange] : (sourceLocalClosure W P).IsStableUnderBaseChange :=
  by
  refine .mk' fun X Y S f g _ ⟨𝒰, hg⟩ ↦ ⟨𝒰.pullback₁ (pullback.snd f g), fun i ↦ ?_⟩
  simpa [← pullbackLeftPullbackSndIso_hom_fst, P.cancel_left_of_respectsIso] using P.pullback_fst _ _ (hg i)

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