projIsoSpecTopComponent — Mathlib

English

The map toSpec 𝒜 f is surjective for f_deg, hm.

Русский

Отображение toSpec 𝒜 f сюръективно при f_deg, hm.

LaTeX

$$$toSpec(𝒜,f) \text{ is surjective when } f ∈ 𝒜(m), hm>0$$$

Lean4

/-- The homeomorphism `Proj|D(f) ≅ Spec A⁰_f` defined by
- `φ : Proj|D(f) ⟶ Spec A⁰_f` by sending `x` to `A⁰_f ∩ span {g / 1 | g ∈ x}`
- `ψ : Spec A⁰_f ⟶ Proj|D(f)` by sending `q` to `{a | aᵢᵐ/fⁱ ∈ q}`.
-/
def projIsoSpecTopComponent {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) : (Proj.T| (pbo f)) ≅ (Spec.T (A⁰_ f))
    where
  hom := ProjIsoSpecTopComponent.toSpec 𝒜 f
  inv := ProjIsoSpecTopComponent.fromSpec f_deg hm
  hom_inv_id := ConcreteCategory.hom_ext _ _ (ProjIsoSpecTopComponent.fromSpec_toSpec 𝒜 f_deg hm)
  inv_hom_id := ConcreteCategory.hom_ext _ _ (ProjIsoSpecTopComponent.toSpec_fromSpec 𝒜 f_deg hm)

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