isReduced_of_isOpenImmersion — Mathlib

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

Похожие утверждения