comap_const — Mathlib

English

Composing with comap on constants: the comap of a constant a/b is the constant f(a)/f(b) after applying f to coefficients.

Русский

Применение comap к константам: константа a/b переходит в константу f(a)/f(b) после применения f к коэффициентам.

LaTeX

$$$comap f U V hUV (const R a b U hb) = const S (f a) (f b) V (\\dots)$$$

Lean4

theorem comap_const (f : R →+* S) (U : Opens (PrimeSpectrum.Top R)) (V : Opens (PrimeSpectrum.Top S))
    (hUV : V.1 ⊆ PrimeSpectrum.comap f ⁻¹' U.1) (a b : R)
    (hb : ∀ x : PrimeSpectrum R, x ∈ U → b ∈ x.asIdeal.primeCompl) :
    comap f U V hUV (const R a b U hb) = const S (f a) (f b) V fun p hpV => hb (PrimeSpectrum.comap f p) (hUV hpV) :=
  Subtype.eq <| funext fun p => by rw [comap_apply, const_apply, const_apply, Localization.localRingHom_mk']

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