English
There is a canonical ring homomorphism from Γ(U, 𝒪_R) to Γ(V, 𝒪_S) induced by f: R → S, sending a section s to its comapped version via comapFun.
Русский
Существует канонический гомоморфизм колец от секций над U к секциям над V, индуцируемый гомоморфизмом f: R → S, отправляющий секцию s в её образ через comapFun.
LaTeX
$$$\\text{comap } f U V hUV : \\Gamma(U, 𝒪_R) \\to \\Gamma(V, 𝒪_S)$$$
Lean4
/-- For a ring homomorphism `f : R →+* S` and open sets `U` and `V` of the prime spectra of `R` and
`S` such that `V ⊆ (comap f) ⁻¹ U`, the induced ring homomorphism from the structure sheaf of `R`
at `U` to the structure sheaf of `S` at `V`.
Explicitly, this map is given as follows: For a point `p : V`, if the section `s` evaluates on `p`
to the fraction `a / b`, its image on `V` evaluates on `p` to the fraction `f(a) / f(b)`.
-/
def comap (f : R →+* S) (U : Opens (PrimeSpectrum.Top R)) (V : Opens (PrimeSpectrum.Top S))
(hUV : V.1 ⊆ PrimeSpectrum.comap f ⁻¹' U.1) : (structureSheaf R).1.obj (op U) →+* (structureSheaf S).1.obj (op V)
where
toFun s := ⟨comapFun f U V hUV s.1, comapFunIsLocallyFraction f U V hUV s.1 s.2⟩
map_one' :=
Subtype.ext <|
funext fun p => by
dsimp
rw [comapFun, (sectionsSubring R (op U)).coe_one, Pi.one_apply, RingHom.map_one]
rfl
map_zero' :=
Subtype.ext <|
funext fun p => by
dsimp
rw [comapFun, (sectionsSubring R (op U)).coe_zero, Pi.zero_apply, RingHom.map_zero]
rfl
map_add' s
t :=
Subtype.ext <|
funext fun p => by
dsimp
rw [comapFun, (sectionsSubring R (op U)).coe_add, Pi.add_apply, RingHom.map_add]
rfl
map_mul' s
t :=
Subtype.ext <|
funext fun p => by
dsimp
rw [comapFun, (sectionsSubring R (op U)).coe_mul, Pi.mul_apply, RingHom.map_mul]
rfl
