IsQuotientEquivQuotientPrime — Mathlib

English

A definition; two submodules N1 ≤ N2 with the quotient N2/N1 isomorphic to A/p for some prime p ∈ Spec(A).

Русский

Определение: N1 ≤ N2 и существует изоморфизм (N2/N1) ≅ A/p для некоторого простого идеала p ∈ Spec(A).

LaTeX

$$$ N_1 \\le N_2 \\; \\land\\; \\exists p \\in \\operatorname{PrimeSpectrum}(A),\\; (N_2/N_1) \\cong_A A/p. $$$

Lean4

/-- A `Prop` asserting that two submodules `N₁, N₂` satisfy `N₁ ≤ N₂` and
`N₂ / N₁` is isomorphic to `A / p` for some prime ideal `p` of `A`. -/
def IsQuotientEquivQuotientPrime (N₁ N₂ : Submodule A M) :=
  N₁ ≤ N₂ ∧ ∃ (p : PrimeSpectrum A), Nonempty ((↥N₂ ⧸ N₁.submoduleOf N₂) ≃ₗ[A] A ⧸ p.1)

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