comap_apply — Mathlib

English

Applying comap to a section s over U, evaluated at p ∈ V, gives the localization map of the evaluated fraction.

Русский

Применение comap к секции s над U и её вычисление в p ∈ V даёт локализационную карту дроби, полученной на p.

LaTeX

$$$((comap f U V hUV)\\, s).1\\; p = \\mathrm{Localization.localRingHom}((\\mathrm{PrimeSpectrum.comap} f) p.1).asIdeal _ f rfl (s.1 ⟨p.1, hUV p.2⟩ :)$$$

Lean4

@[simp]
theorem comap_apply (f : R →+* S) (U : Opens (PrimeSpectrum.Top R)) (V : Opens (PrimeSpectrum.Top S))
    (hUV : V.1 ⊆ PrimeSpectrum.comap f ⁻¹' U.1) (s : (structureSheaf R).1.obj (op U)) (p : V) :
    (comap f U V hUV s).1 p =
      Localization.localRingHom (PrimeSpectrum.comap f p.1).asIdeal _ f rfl
        (s.1 ⟨PrimeSpectrum.comap f p.1, hUV p.2⟩ :) :=
  rfl

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