English
For an open immersion f, Y is germ-injective at f.base x if and only if X is germ-injective at x.
Русский
Для открытого встраивания f верно: Y germ-injects в f.base x тогда и только тогда, когда X germ-injective в x.
LaTeX
$$$\text{isOpenImmersion } f \; \Rightarrow\; Y.IsGermInjectiveAt(f.x) \iff X.IsGermInjectiveAt(x)$$$
Lean4
theorem isGermInjectiveAt_iff_of_isOpenImmersion {x : X} [IsOpenImmersion f] :
Y.IsGermInjectiveAt (f.base x) ↔ X.IsGermInjectiveAt x :=
by
refine ⟨fun H ↦ ?_, fun _ ↦ inferInstance⟩
obtain ⟨U, hxU, hU, hU', H⟩ := Y.exists_le_and_germ_injective (f.base x) (V := f.opensRange) ⟨x, rfl⟩
obtain ⟨V, hV⟩ := (IsOpenImmersion.affineOpensEquiv f).surjective ⟨⟨U, hU⟩, hU'⟩
obtain rfl : f ''ᵁ V = U := Subtype.eq_iff.mp (Subtype.eq_iff.mp hV)
obtain ⟨y, hy, e : f.base y = f.base x⟩ := hxU
obtain rfl := f.isOpenEmbedding.injective e
refine ⟨V, hy, V.2, ?_⟩
replace H := ((MorphismProperty.injective CommRingCat).cancel_right_of_respectsIso _ (f.stalkMap y)).mpr H
replace H := ((MorphismProperty.injective CommRingCat).cancel_left_of_respectsIso (f.appIso V).inv _).mpr H
simpa using H
