English
The image of the restricted preimage under f|_U equals the preimage under f of the image: (f|_U)ⱼ''ᵁ((f|_U)^{-1}ᵁ V) = f^{-1}ᵁ(U.ι''ᵁ V).
Русский
Образ ограниченного прообраза под f|_U совпадает с прообразом образа под f: (f|_U)ⱼ''ᵁ((f|_U)^{-1}ᵁ V) = f^{-1}ᵁ(U.ι''ᵁ V).
LaTeX
$$$\mathrm{image}\;((f|_U)^{-1}ᵁ V) = f^{-1}ᵁ(U.ι''ᵁ V)$$$
Lean4
theorem image_morphismRestrict_preimage {X Y : Scheme.{u}} (f : X ⟶ Y) (U : Y.Opens) (V : Opens U) :
(f ⁻¹ᵁ U).ι ''ᵁ ((f ∣_ U) ⁻¹ᵁ V) = f ⁻¹ᵁ (U.ι ''ᵁ V) :=
by
ext1
ext x
constructor
· rintro ⟨⟨x, hx⟩, hx' : (f ∣_ U).base _ ∈ V, rfl⟩
refine ⟨⟨_, hx⟩, ?_, rfl⟩
convert hx'
refine Subtype.ext ?_
exact (morphismRestrict_base_coe f U ⟨x, hx⟩).symm
· rintro ⟨⟨x, hx⟩, hx' : _ ∈ V.1, rfl : x = _⟩
refine ⟨⟨_, hx⟩, (?_ : (f ∣_ U).base ⟨x, hx⟩ ∈ V.1), rfl⟩
convert hx'
refine Subtype.ext ?_
exact morphismRestrict_base_coe f U ⟨x, hx⟩
