Documentation

Mathlib.RingTheory.GradedAlgebra.Homogeneous.Maps

Maps on homogeneous ideals #

In this file we define HomogeneousIdeal.map and HomogeneousIdeal.comap.

source
๐Ÿ”ธ coverage
def HomogeneousIdeal.map {A : Type u_1} {B : Type u_2} {ฯƒ : Type u_4} {ฯ„ : Type u_5} {ฮน : Type u_7} [Semiring A] [Semiring B] [SetLike ฯƒ A] [SetLike ฯ„ B] [AddSubmonoidClass ฯƒ A] [AddSubmonoidClass ฯ„ B] [DecidableEq ฮน] [AddMonoid ฮน] {๐’œ : ฮน โ†’ ฯƒ} {โ„ฌ : ฮน โ†’ ฯ„} [GradedRing ๐’œ] [GradedRing โ„ฌ] (f : ๐’œ โ†’+*แต โ„ฌ) (I : HomogeneousIdeal ๐’œ) :
HomogeneousIdeal โ„ฌ

Map a homogeneous ideal along a graded ring homomorphism. The underlying ideal is (definitionally) equal to Ideal.map.

Instances For
    source
    ๐Ÿ”ธ coverage
    def HomogeneousIdeal.comap {A : Type u_1} {B : Type u_2} {ฯƒ : Type u_4} {ฯ„ : Type u_5} {ฮน : Type u_7} [Semiring A] [Semiring B] [SetLike ฯƒ A] [SetLike ฯ„ B] [AddSubmonoidClass ฯƒ A] [AddSubmonoidClass ฯ„ B] [DecidableEq ฮน] [AddMonoid ฮน] {๐’œ : ฮน โ†’ ฯƒ} {โ„ฌ : ฮน โ†’ ฯ„} [GradedRing ๐’œ] [GradedRing โ„ฌ] (f : ๐’œ โ†’+*แต โ„ฌ) (I : 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.

    Instances For
      source
      ๐Ÿ“ coverage
      theorem HomogeneousIdeal.map_le_iff_le_comap {A : Type u_1} {B : Type u_2} {ฯƒ : Type u_4} {ฯ„ : Type u_5} {ฮน : Type u_7} [Semiring A] [Semiring B] [SetLike ฯƒ A] [SetLike ฯ„ B] [AddSubmonoidClass ฯƒ A] [AddSubmonoidClass ฯ„ B] [DecidableEq ฮน] [AddMonoid ฮน] {๐’œ : ฮน โ†’ ฯƒ} {โ„ฌ : ฮน โ†’ ฯ„} [GradedRing ๐’œ] [GradedRing โ„ฌ] (f : ๐’œ โ†’+*แต โ„ฌ) {I : HomogeneousIdeal ๐’œ} {J : HomogeneousIdeal โ„ฌ} :
      map f I โ‰ค J โ†” I โ‰ค comap f J
      source
      ๐Ÿ“ coverage
      theorem HomogeneousIdeal.le_comap_of_map_le {A : Type u_1} {B : Type u_2} {ฯƒ : Type u_4} {ฯ„ : Type u_5} {ฮน : Type u_7} [Semiring A] [Semiring B] [SetLike ฯƒ A] [SetLike ฯ„ B] [AddSubmonoidClass ฯƒ A] [AddSubmonoidClass ฯ„ B] [DecidableEq ฮน] [AddMonoid ฮน] {๐’œ : ฮน โ†’ ฯƒ} {โ„ฌ : ฮน โ†’ ฯ„} [GradedRing ๐’œ] [GradedRing โ„ฌ] (f : ๐’œ โ†’+*แต โ„ฌ) {I : HomogeneousIdeal ๐’œ} {J : HomogeneousIdeal โ„ฌ} :
      map f I โ‰ค J โ†’ I โ‰ค comap f J

      Alias of the forward direction of HomogeneousIdeal.map_le_iff_le_comap.

      source
      ๐Ÿ“ coverage
      theorem HomogeneousIdeal.map_le_of_le_comap {A : Type u_1} {B : Type u_2} {ฯƒ : Type u_4} {ฯ„ : Type u_5} {ฮน : Type u_7} [Semiring A] [Semiring B] [SetLike ฯƒ A] [SetLike ฯ„ B] [AddSubmonoidClass ฯƒ A] [AddSubmonoidClass ฯ„ B] [DecidableEq ฮน] [AddMonoid ฮน] {๐’œ : ฮน โ†’ ฯƒ} {โ„ฌ : ฮน โ†’ ฯ„} [GradedRing ๐’œ] [GradedRing โ„ฌ] (f : ๐’œ โ†’+*แต โ„ฌ) {I : HomogeneousIdeal ๐’œ} {J : HomogeneousIdeal โ„ฌ} :
      I โ‰ค comap f J โ†’ map f I โ‰ค J

      Alias of the reverse direction of HomogeneousIdeal.map_le_iff_le_comap.

      source
      ๐Ÿ“ coverage
      theorem HomogeneousIdeal.gc_map_comap {A : Type u_1} {B : Type u_2} {ฯƒ : Type u_4} {ฯ„ : Type u_5} {ฮน : Type u_7} [Semiring A] [Semiring B] [SetLike ฯƒ A] [SetLike ฯ„ B] [AddSubmonoidClass ฯƒ A] [AddSubmonoidClass ฯ„ B] [DecidableEq ฮน] [AddMonoid ฮน] {๐’œ : ฮน โ†’ ฯƒ} {โ„ฌ : ฮน โ†’ ฯ„} [GradedRing ๐’œ] [GradedRing โ„ฌ] (f : ๐’œ โ†’+*แต โ„ฌ) :
      GaloisConnection (map f) (comap f)
      source
      ๐Ÿ“ coverage
      theorem HomogeneousIdeal.map_mono {A : Type u_1} {B : Type u_2} {ฯƒ : Type u_4} {ฯ„ : Type u_5} {ฮน : Type u_7} [Semiring A] [Semiring B] [SetLike ฯƒ A] [SetLike ฯ„ B] [AddSubmonoidClass ฯƒ A] [AddSubmonoidClass ฯ„ B] [DecidableEq ฮน] [AddMonoid ฮน] {๐’œ : ฮน โ†’ ฯƒ} {โ„ฌ : ฮน โ†’ ฯ„} [GradedRing ๐’œ] [GradedRing โ„ฌ] (f : ๐’œ โ†’+*แต โ„ฌ) :
      Monotone (map f)
      source
      ๐Ÿ“ coverage
      theorem HomogeneousIdeal.comap_mono {A : Type u_1} {B : Type u_2} {ฯƒ : Type u_4} {ฯ„ : Type u_5} {ฮน : Type u_7} [Semiring A] [Semiring B] [SetLike ฯƒ A] [SetLike ฯ„ B] [AddSubmonoidClass ฯƒ A] [AddSubmonoidClass ฯ„ B] [DecidableEq ฮน] [AddMonoid ฮน] {๐’œ : ฮน โ†’ ฯƒ} {โ„ฌ : ฮน โ†’ ฯ„} [GradedRing ๐’œ] [GradedRing โ„ฌ] (f : ๐’œ โ†’+*แต โ„ฌ) :
      Monotone (comap f)
      source
      ๐Ÿ“ coverage
      @[simp]
      theorem HomogeneousIdeal.toIdeal_comap {A : Type u_1} {B : Type u_2} {ฯƒ : Type u_4} {ฯ„ : Type u_5} {ฮน : Type u_7} [Semiring A] [Semiring B] [SetLike ฯƒ A] [SetLike ฯ„ B] [AddSubmonoidClass ฯƒ A] [AddSubmonoidClass ฯ„ B] [DecidableEq ฮน] [AddMonoid ฮน] {๐’œ : ฮน โ†’ ฯƒ} {โ„ฌ : ฮน โ†’ ฯ„} [GradedRing ๐’œ] [GradedRing โ„ฌ] (f : ๐’œ โ†’+*แต โ„ฌ) {J : HomogeneousIdeal โ„ฌ} :
      (comap f J).toIdeal = Ideal.comap f J.toIdeal
      source
      ๐Ÿ“ coverage
      @[simp]
      theorem HomogeneousIdeal.coe_comap {A : Type u_1} {B : Type u_2} {ฯƒ : Type u_4} {ฯ„ : Type u_5} {ฮน : Type u_7} [Semiring A] [Semiring B] [SetLike ฯƒ A] [SetLike ฯ„ B] [AddSubmonoidClass ฯƒ A] [AddSubmonoidClass ฯ„ B] [DecidableEq ฮน] [AddMonoid ฮน] {๐’œ : ฮน โ†’ ฯƒ} {โ„ฌ : ฮน โ†’ ฯ„} [GradedRing ๐’œ] [GradedRing โ„ฌ] (f : ๐’œ โ†’+*แต โ„ฌ) {J : HomogeneousIdeal โ„ฌ} :
      โ†‘(comap f J) = โ‡‘f โปยน' โ†‘J
      source
      ๐Ÿ“ coverage
      @[simp]
      theorem HomogeneousIdeal.toIdeal_map {A : Type u_1} {B : Type u_2} {ฯƒ : Type u_4} {ฯ„ : Type u_5} {ฮน : Type u_7} [Semiring A] [Semiring B] [SetLike ฯƒ A] [SetLike ฯ„ B] [AddSubmonoidClass ฯƒ A] [AddSubmonoidClass ฯ„ B] [DecidableEq ฮน] [AddMonoid ฮน] {๐’œ : ฮน โ†’ ฯƒ} {โ„ฌ : ฮน โ†’ ฯ„} [GradedRing ๐’œ] [GradedRing โ„ฌ] (f : ๐’œ โ†’+*แต โ„ฌ) {I : HomogeneousIdeal ๐’œ} :
      (map f I).toIdeal = Ideal.map f I.toIdeal
      source
      ๐Ÿ“ coverage
      instance HomogeneousIdeal.isPrime_comap {A : Type u_1} {B : Type u_2} {ฯƒ : Type u_4} {ฯ„ : Type u_5} {ฮน : Type u_7} [Semiring A] [Semiring B] [SetLike ฯƒ A] [SetLike ฯ„ B] [AddSubmonoidClass ฯƒ A] [AddSubmonoidClass ฯ„ B] [DecidableEq ฮน] [AddMonoid ฮน] {๐’œ : ฮน โ†’ ฯƒ} {โ„ฌ : ฮน โ†’ ฯ„} [GradedRing ๐’œ] [GradedRing โ„ฌ] (f : ๐’œ โ†’+*แต โ„ฌ) {J : HomogeneousIdeal โ„ฌ} [J.toIdeal.IsPrime] :
      (comap f J).toIdeal.IsPrime
      source
      ๐Ÿ“ coverage
      @[simp]
      theorem HomogeneousIdeal.map_id {A : Type u_1} {ฯƒ : Type u_4} {ฮน : Type u_7} [Semiring A] [SetLike ฯƒ A] [AddSubmonoidClass ฯƒ A] [DecidableEq ฮน] [AddMonoid ฮน] {๐’œ : ฮน โ†’ ฯƒ} [GradedRing ๐’œ] {I : HomogeneousIdeal ๐’œ} :
      map (GradedRingHom.id ๐’œ) I = I
      source
      ๐Ÿ“ coverage
      theorem HomogeneousIdeal.map_map {A : Type u_1} {B : Type u_2} {C : Type u_3} {ฯƒ : Type u_4} {ฯ„ : Type u_5} {ฯ‰ : Type u_6} {ฮน : Type u_7} [Semiring A] [Semiring B] [Semiring C] [SetLike ฯƒ A] [SetLike ฯ„ B] [SetLike ฯ‰ C] [AddSubmonoidClass ฯƒ A] [AddSubmonoidClass ฯ„ B] [AddSubmonoidClass ฯ‰ C] [DecidableEq ฮน] [AddMonoid ฮน] {๐’œ : ฮน โ†’ ฯƒ} {โ„ฌ : ฮน โ†’ ฯ„} {๐’ž : ฮน โ†’ ฯ‰} [GradedRing ๐’œ] [GradedRing โ„ฌ] [GradedRing ๐’ž] (f : ๐’œ โ†’+*แต โ„ฌ) (g : โ„ฌ โ†’+*แต ๐’ž) {I : HomogeneousIdeal ๐’œ} :
      map g (map f I) = map (g.comp f) I
      source
      ๐Ÿ“ coverage
      theorem HomogeneousIdeal.map_comp {A : Type u_1} {B : Type u_2} {C : Type u_3} {ฯƒ : Type u_4} {ฯ„ : Type u_5} {ฯ‰ : Type u_6} {ฮน : Type u_7} [Semiring A] [Semiring B] [Semiring C] [SetLike ฯƒ A] [SetLike ฯ„ B] [SetLike ฯ‰ C] [AddSubmonoidClass ฯƒ A] [AddSubmonoidClass ฯ„ B] [AddSubmonoidClass ฯ‰ C] [DecidableEq ฮน] [AddMonoid ฮน] {๐’œ : ฮน โ†’ ฯƒ} {โ„ฌ : ฮน โ†’ ฯ„} {๐’ž : ฮน โ†’ ฯ‰} [GradedRing ๐’œ] [GradedRing โ„ฌ] [GradedRing ๐’ž] (f : ๐’œ โ†’+*แต โ„ฌ) (g : โ„ฌ โ†’+*แต ๐’ž) {I : HomogeneousIdeal ๐’œ} :
      map (g.comp f) I = map g (map f I)
      source
      ๐Ÿ“ coverage
      @[simp]
      theorem HomogeneousIdeal.comap_id {A : Type u_1} {ฯƒ : Type u_4} {ฮน : Type u_7} [Semiring A] [SetLike ฯƒ A] [AddSubmonoidClass ฯƒ A] [DecidableEq ฮน] [AddMonoid ฮน] {๐’œ : ฮน โ†’ ฯƒ} [GradedRing ๐’œ] {I : HomogeneousIdeal ๐’œ} :
      comap (GradedRingHom.id ๐’œ) I = I
      source
      ๐Ÿ“ coverage
      theorem HomogeneousIdeal.comap_comap {A : Type u_1} {B : Type u_2} {C : Type u_3} {ฯƒ : Type u_4} {ฯ„ : Type u_5} {ฯ‰ : Type u_6} {ฮน : Type u_7} [Semiring A] [Semiring B] [Semiring C] [SetLike ฯƒ A] [SetLike ฯ„ B] [SetLike ฯ‰ C] [AddSubmonoidClass ฯƒ A] [AddSubmonoidClass ฯ„ B] [AddSubmonoidClass ฯ‰ C] [DecidableEq ฮน] [AddMonoid ฮน] {๐’œ : ฮน โ†’ ฯƒ} {โ„ฌ : ฮน โ†’ ฯ„} {๐’ž : ฮน โ†’ ฯ‰} [GradedRing ๐’œ] [GradedRing โ„ฌ] [GradedRing ๐’ž] (f : ๐’œ โ†’+*แต โ„ฌ) (g : โ„ฌ โ†’+*แต ๐’ž) {K : HomogeneousIdeal ๐’ž} :
      comap f (comap g K) = comap (g.comp f) K
      source
      ๐Ÿ“ coverage
      theorem HomogeneousIdeal.irrelevant_le_map_comp {A : Type u_1} {B : Type u_2} {C : Type u_3} {ฯƒ : Type u_4} {ฯ„ : Type u_5} {ฯ‰ : Type u_6} {ฮน : Type u_7} [Semiring A] [Semiring B] [Semiring C] [SetLike ฯƒ A] [SetLike ฯ„ B] [SetLike ฯ‰ C] [AddSubmonoidClass ฯƒ A] [AddSubmonoidClass ฯ„ B] [AddSubmonoidClass ฯ‰ C] [DecidableEq ฮน] [AddCommMonoid ฮน] [PartialOrder ฮน] [CanonicallyOrderedAdd ฮน] {๐’œ : ฮน โ†’ ฯƒ} {โ„ฌ : ฮน โ†’ ฯ„} {๐’ž : ฮน โ†’ ฯ‰} [GradedRing ๐’œ] [GradedRing โ„ฌ] [GradedRing ๐’ž] {f : ๐’œ โ†’+*แต โ„ฌ} {g : โ„ฌ โ†’+*แต ๐’ž} (hf : irrelevant โ„ฌ โ‰ค map f (irrelevant ๐’œ)) (hg : irrelevant ๐’ž โ‰ค map g (irrelevant โ„ฌ)) :
      irrelevant ๐’ž โ‰ค map (g.comp f) (irrelevant ๐’œ)