Theorems · Definition · commutative algebra

HomogeneousIdeal.comap

{A : Type u_1} →
  {B : Type u_2} →
    {σ : Type u_4} →
      {τ : Type u_5} →
        {ι : Type u_7} →
          [inst : Semiring A] →
            [inst_1 : Semiring B] →
              [inst_2 : SetLike σ A] →
                [inst_3 : SetLike τ B] →
                  [inst_4 : AddSubmonoidClass σ A] →
                    [inst_5 : AddSubmonoidClass τ B] →
                      [inst_6 : DecidableEq ι] →
                        [inst_7 : AddMonoid ι] →
                          {𝒜 : ι → σ} →
                            {ℬ : ι → τ} →
                              [inst_8 : GradedRing 𝒜] →
                                [inst_9 : GradedRing ℬ] → (𝒜 →+*ᵍ ℬ) → HomogeneousIdeal ℬ → HomogeneousIdeal 𝒜

Pull back a homogeneous ideal along a graded ring homomorphism. The underlying ideal is (definitionally) equal to Ideal.comap, whose underlying set is definitionally equal to the preimage.

Defined in

Mathlib.RingTheory.GradedAlgebra.Homogeneous.Maps

Cited by

10 results in Mathlib

Foundations

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

Assumes

SemiringSemiringSetLikeSetLikeAddSubmonoidClassAddSubmonoidClassDecidableEqAddMonoidGradedRingGradedRing