instRespectsLeftSchemeOfIsStableUnderBaseChange

English

Isomorphisms and their behavior with respect to scheme morphisms respect isomorphisms; the instance ensures the closure property under isomorphisms.

Русский

Изоморфизмы и их поведение по отношению к отображениям схем сохраняют изоморфизмы; экземпляр обеспечивает свойство замыкания при изоморфизмах.

LaTeX

$$IsRespectsIso Isomorphisms$$

Lean4

instance [P.RespectsLeft Q] [Q.IsStableUnderBaseChange] : (sourceLocalClosure W P).RespectsLeft Q :=
  by
  refine ⟨fun {X Y} Z f hf g ⟨𝒰, hg⟩ ↦ ⟨𝒰.pullback₁ f, fun i ↦ ?_⟩⟩
  simpa [pullback.condition_assoc] using RespectsLeft.precomp (Q := Q) _ (Q.pullback_snd _ _ hf) _ (hg i)

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