instRespectsRightScheme — Mathlib

English

SourceLocalClosure preserves Right-respect of morphism properties on schemes.

Русский

SourceLocalClosure сохраняет правая устойчивость к свойствам морфизмов на схемах.

LaTeX

$$RespectsRight Scheme$$

Lean4

instance [P.RespectsRight Q] : (sourceLocalClosure W P).RespectsRight Q :=
  by
  refine ⟨fun {X Y} Z f hf g ⟨𝒰, hg⟩ ↦ ⟨𝒰, fun i ↦ ?_⟩⟩
  rw [← Category.assoc]
  exact RespectsRight.postcomp _ hf _ (hg i)

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