instIsGermInjectiveOfIsIntegral — Mathlib

English

If X is integral, then X is germ-injective.

Русский

Если X целостен (интегральный), то X germ-injective.

LaTeX

$$$\text{IsGermInjective}(X)\;\text{holds if } X\text{ is integral}$$$

Lean4

instance (priority := 100) [IsIntegral X] : X.IsGermInjective :=
  by
  refine fun x ↦
    ⟨⟨(X.affineCover.f _).opensRange, X.affineCover.covers x, (isAffineOpen_opensRange (X.affineCover.f _)), ?_⟩⟩
  have : Nonempty (X.affineCover.f _).opensRange := ⟨⟨_, X.affineCover.covers x⟩⟩
  have := (isAffineOpen_opensRange (X.affineCover.f _)).isLocalization_stalk ⟨_, X.affineCover.covers x⟩
  exact @IsLocalization.injective _ _ _ _ _ (show _ from _) this (Ideal.primeCompl_le_nonZeroDivisors _)

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