Theorems · Definition · algebraic geometry

AlgebraicGeometry.StructureSheaf.comapFun

{R M : Type u} →
  [inst : CommRing R] →
    [inst_1 : AddCommGroup M] →
      [inst_2 : Module R M] →
        {S : Type u} →
          [inst_3 : CommRing S] →
            {N : Type u} →
              [inst_4 : AddCommGroup N] →
                [inst_5 : Module S N] →
                  {σ : R →+* S} →
                    (M →ₛₗ[σ] N) →
                      (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) →
                        (V : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top S)) →
                          V.carrier ⊆ PrimeSpectrum.comap σ ⁻¹' U.carrier →
                            ((x : ↥U) → AlgebraicGeometry.StructureSheaf.Localizations M ↑x) →
                              (y : ↥V) → AlgebraicGeometry.StructureSheaf.Localizations N ↑y

Given a ring homomorphism f : R →+* S, an open set U of the prime spectrum of R and an open set V of the prime spectrum of S, such that V ⊆ (comap f) ⁻¹' U, we can push a section s on U to a section on V, by composing with Localization.localRingHom _ _ f from the left and comap f from the right. Explicitly, if s evaluates on comap f p to a / b, its image on V evaluates on p to f(a) / f(b). At the moment, we work with arbitrary dependent functions s : Π x : U, Localizations R x. Below, we prove the predicate isLocallyFraction is preserved by this map, hence it can be extended to a morphism between the structure sheaves of R and S.

Defined in

Mathlib.AlgebraicGeometry.StructureSheaf

Cited by

2 results in Mathlib

Foundations

Depth 83 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingAddCommGroupModuleCommRingAddCommGroupModule