Theorems · Definition · algebraic geometry

Function.locallyFinsupp.map

{X : Type u_1} →
  {Y : Type u_2} →
    {R : Type u_3} →
      [inst : TopologicalSpace X] →
        [inst_1 : TopologicalSpace Y] →
          (f : X → Y) →
            (X → R) →
              [inst_2 : Semiring R] →
                [PrespectralSpace Y] → IsSpectralMap f → Function.locallyFinsupp X R → Function.locallyFinsupp Y R

The pushforward of a function c of locally finite support by a spectral map with respect to a weight function w.

Defined in

Mathlib.Topology.LocallyFinsupp.Pushforward

Cited by

4 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpaceSemiringPrespectralSpace