Theorems · Definition · algebraic geometry

AlgebraicGeometry.StructureSheaf.Localizations.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) →
                      (y : ↑(AlgebraicGeometry.PrimeSpectrum.Top S)) →
                        AlgebraicGeometry.StructureSheaf.Localizations M (PrimeSpectrum.comap σ y) →ₛₗ[σ]
                          AlgebraicGeometry.StructureSheaf.Localizations N y

The map M_{f y} ⟶ N_{y} used to build maps between structure sheaves.

Defined in

Mathlib.AlgebraicGeometry.StructureSheaf

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupModuleCommRingAddCommGroupModule