English
If f is an open immersion X → Y and Y is reduced, then X is reduced.
Русский
Если f является открытым вложением X → Y и Y редуцировано, то и X редуцировано.
LaTeX
$$$ \text{IsOpenImmersion}(f) \wedge \text{IsReduced}(Y) \Rightarrow \text{IsReduced}(X) $$$
Lean4
theorem isReduced_of_isOpenImmersion {X Y : Scheme} (f : X ⟶ Y) [H : IsOpenImmersion f] [IsReduced Y] : IsReduced X :=
by
constructor
intro U
have : U = f ⁻¹ᵁ f ''ᵁ U := by ext1; exact (Set.preimage_image_eq _ H.base_open.injective).symm
rw [this]
exact
isReduced_of_injective (inv <| f.app (f ''ᵁ U)).hom
(asIso <| f.app (f ''ᵁ U) : Γ(Y, f ''ᵁ U) ≅ _).symm.commRingCatIsoToRingEquiv.injective