English
The morphism from the pullback is the composition of the pullback projection with awayι, i.e., the natural map to Proj_comm is compatible with the pullback structure.
Русский
Гомоморфизм из вытяжки есть композиция проекции вытяжки с awayι; естественная карта к Proj совместима с конструкцией вытяжки.
LaTeX
$$(pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx).hom ≫ awayι 𝒜 x = Limits.pullback.fst _ _ ≫ awayι 𝒜 f f_deg hm$$
Lean4
/-- The isomorphism `D₊(f) ×[Proj 𝒜] D₊(g) ≅ D₊(fg)`. -/
noncomputable def pullbackAwayιIso :
Limits.pullback (awayι 𝒜 f f_deg hm) (awayι 𝒜 g g_deg hm') ≅ Spec (.of <| Away 𝒜 x) :=
IsOpenImmersion.isoOfRangeEq (Limits.pullback.fst _ _ ≫ awayι 𝒜 f f_deg hm)
(awayι 𝒜 x (hx ▸ SetLike.mul_mem_graded f_deg g_deg) (hm.trans_le (m.le_add_right m'))) <|
by
rw [IsOpenImmersion.range_pullback_to_base_of_left]
change ((awayι 𝒜 f _ _).opensRange ⊓ (awayι 𝒜 g _ _).opensRange).1 = (awayι 𝒜 _ _ _).opensRange.1
rw [opensRange_awayι, opensRange_awayι, opensRange_awayι, ← basicOpen_mul, hx]
