English
Under hypotheses of germ injectivity, there exist V, hxV, φ′, i such that V is affine, etc., providing a lift of φ through germ on V.
Русский
При условиях инъективности гера существуют V, hxV, φ′, i, где V аффинно, образуя подъем через гера на V.
LaTeX
$$$\exists V\; (hxV)\; (φ′)\; (i) \; \text{is affine and lifts } φ$$$
Lean4
instance (x : X) [X.IsGermInjectiveAt x] [IsOpenImmersion f] : Y.IsGermInjectiveAt (f.base x) :=
by
obtain ⟨U, hxU, hU, H⟩ := X.exists_germ_injective x
refine ⟨⟨f ''ᵁ U, ⟨x, hxU, rfl⟩, hU.image_of_isOpenImmersion f, ?_⟩⟩
refine ((MorphismProperty.injective CommRingCat).cancel_right_of_respectsIso _ (f.stalkMap x)).mp ?_
refine ((MorphismProperty.injective CommRingCat).cancel_left_of_respectsIso (f.appIso U).inv _).mp ?_
simpa
