English
Same as above: if f is an open immersion and Y is integral with X nonempty, then X is integral.
Русский
Аналогично: если f открытое вложение и Y целостна, то X целостна.
LaTeX
$$$\text{IsOpenImmersion}(f) \wedge \text{IsIntegral}(Y) \wedge \text{Nonempty}(X) \Rightarrow \text{IsIntegral}(X)$$$
Lean4
theorem isIntegral_of_isOpenImmersion {X Y : Scheme} (f : X ⟶ Y) [H : IsOpenImmersion f] [IsIntegral Y] [Nonempty X] :
IsIntegral X := by
constructor; · infer_instance
intro U hU
have : U = f ⁻¹ᵁ f ''ᵁ U := by ext1; exact (Set.preimage_image_eq _ H.base_open.injective).symm
rw [this]
have : IsDomain Γ(Y, f ''ᵁ U) :=
by
apply (config := { allowSynthFailures := true }) IsIntegral.component_integral
exact ⟨⟨_, _, hU.some.prop, rfl⟩⟩
exact (asIso <| f.app (f ''ᵁ U) : Γ(Y, f ''ᵁ U) ≅ _).symm.commRingCatIsoToRingEquiv.toMulEquiv.isDomain _
