Theorems · Definition · commutative algebra

FractionalIdeal.map

{R : Type u_1} →
  [inst : CommRing R] →
    {S : Submonoid R} →
      {P : Type u_2} →
        [inst_1 : CommRing P] →
          [inst_2 : Algebra R P] →
            {P' : Type u_3} →
              [inst_3 : CommRing P'] →
                [inst_4 : Algebra R P'] → (P →ₐ[R] P') → FractionalIdeal S P → FractionalIdeal S P'

I.map g is the pushforward of the fractional ideal I along the algebra morphism g

Defined in

Mathlib.RingTheory.FractionalIdeal.Operations

Cited by

20 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraCommRingAlgebra