Homomorphisms of graded (semi)rings

This file defines bundled homomorphisms of graded (semi)rings. We use the same structure GradedRingHom 𝒜 ℬ, a.k.a. 𝒜 →+*ᵍ ℬ, for both types of homomorphisms.

We do not define a separate class of graded ring homomorphisms; instead, we use [FunLike F A B] [GradedFunLike F 𝒜 ℬ] [RingHomClass F A B].

Main definitions

• GradedRingHom: Graded (semi)ring homomorphisms. Ring homomorphism which preserves the grading.

Notation

• →+*ᵍ: Graded (semi)ring hom.

Implementation notes

• We don't really need the fact that they are graded rings until the theorem DirectSum.decompose_map which describes how the decomposition interacts with the map.

structure GradedRingHom {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_6} {τ : Type u_7} [Semiring A] [Semiring B] [SetLike σ A] [SetLike τ B] (𝒜 : ι → σ) (ℬ : ι → τ) extends A →+* B : Type (max u_2 u_3)

Bundled graded (semi)ring homomorphisms. Use GradedRingHom for the namespace and other identifiers, and 𝒜 →+*ᵍ ℬ for the notation.

• toFun : A → B
• map_one' : (↑↑↑self).toFun 1 = 1
• map_mul' (x y : A) : (↑↑↑self).toFun (x * y) = (↑↑↑self).toFun x * (↑↑↑self).toFun y
• map_zero' : (↑↑↑self).toFun 0 = 0
• map_add' (x y : A) : (↑↑↑self).toFun (x + y) = (↑↑↑self).toFun x + (↑↑↑self).toFun y
• map_mem {i : ι} {x : A} : x ∈ 𝒜 i → ↑self x ∈ ℬ i

def «term_→+*ᵍ_» : Lean.TrailingParserDescr

Bundled graded (semi)ring homomorphisms. Use GradedRingHom for the namespace and other identifiers, and 𝒜 →+*ᵍ ℬ for the notation.

Equations

• «term_→+*ᵍ_» = Lean.ParserDescr.trailingNode `«term_→+*ᵍ_» 25 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " →+*ᵍ ") (Lean.ParserDescr.cat `term 0))

def GradedRingHom.ofClass {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_6} {τ : Type u_7} [Semiring A] [Semiring B] [SetLike σ A] [SetLike τ B] {𝒜 : ι → σ} {ℬ : ι → τ} {F : Type u_10} [FunLike F A B] [GradedFunLike F 𝒜 ℬ] [RingHomClass F A B] (f : F) : 𝒜 →+*ᵍ ℬ

Turn an element of a type F satisfying [FunLike F A B] [GradedFunLike F 𝒜 ℬ] [RingHomClass F A B] into an actual GradedRingHom.

This should not be used directly. In the future, Mathlib will prefer structural projections over these general constructions from hom classes.

Equations

• ↑f = { toRingHom := ↑f, map_mem := ⋯ }

@[implicit_reducible]

instance GradedRingHom.instFunLike {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_6} {τ : Type u_7} [Semiring A] [Semiring B] [SetLike σ A] [SetLike τ B] {𝒜 : ι → σ} {ℬ : ι → τ} : FunLike (𝒜 →+*ᵍ ℬ) A B

Equations

• GradedRingHom.instFunLike = { coe := fun (f : 𝒜 →+*ᵍ ℬ) => (↑↑↑f).toFun, coe_injective' := ⋯ }

instance GradedRingHom.instGradedFunLike {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_6} {τ : Type u_7} [Semiring A] [Semiring B] [SetLike σ A] [SetLike τ B] {𝒜 : ι → σ} {ℬ : ι → τ} : GradedFunLike (𝒜 →+*ᵍ ℬ) 𝒜 ℬ

instance GradedRingHom.instRingHomClass {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_6} {τ : Type u_7} [Semiring A] [Semiring B] [SetLike σ A] [SetLike τ B] {𝒜 : ι → σ} {ℬ : ι → τ} : RingHomClass (𝒜 →+*ᵍ ℬ) A B

@[simp]

theorem GradedRingHom.toRingHom_eq_toRingHom {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_6} {τ : Type u_7} [Semiring A] [Semiring B] [SetLike σ A] [SetLike τ B] {𝒜 : ι → σ} {ℬ : ι → τ} (f : 𝒜 →+*ᵍ ℬ) : ↑f = ↑f

@[simp]

theorem GradedRingHom.coe_toRingHom {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_6} {τ : Type u_7} [Semiring A] [Semiring B] [SetLike σ A] [SetLike τ B] {𝒜 : ι → σ} {ℬ : ι → τ} (f : 𝒜 →+*ᵍ ℬ) : ⇑↑f = ⇑f

@[simp]

theorem GradedRingHom.coe_mk {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_6} {τ : Type u_7} [Semiring A] [Semiring B] [SetLike σ A] [SetLike τ B] {𝒜 : ι → σ} {ℬ : ι → τ} (f : A →+* B) (h : ∀ {i : ι} {x : A}, x ∈ 𝒜 i → f x ∈ ℬ i) : ⇑{ toRingHom := f, map_mem := h } = ⇑f

@[simp]

theorem GradedRingHom.coe_ofClass {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_6} {τ : Type u_7} [Semiring A] [Semiring B] [SetLike σ A] [SetLike τ B] {𝒜 : ι → σ} {ℬ : ι → τ} {F : Type u_10} [FunLike F A B] [GradedFunLike F 𝒜 ℬ] [RingHomClass F A B] (f : F) : ⇑↑f = ⇑f

@[implicit_reducible]

instance GradedRingHom.coeToRingHom {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_6} {τ : Type u_7} [Semiring A] [Semiring B] [SetLike σ A] [SetLike τ B] {𝒜 : ι → σ} {ℬ : ι → τ} : CoeOut (𝒜 →+*ᵍ ℬ) (A →+* B)

Equations

• GradedRingHom.coeToRingHom = { coe := GradedRingHom.toRingHom }

def GradedRingHom.copy {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_6} {τ : Type u_7} [Semiring A] [Semiring B] [SetLike σ A] [SetLike τ B] {𝒜 : ι → σ} {ℬ : ι → τ} (f : 𝒜 →+*ᵍ ℬ) (f' : A → B) (h : f' = ⇑f) : 𝒜 →+*ᵍ ℬ

Copy of a GradedRingHom with a new toFun equal to the old one. Useful to fix definitional equalities.

Equations

• f.copy f' h = { toRingHom := (↑f).copy f' h, map_mem := ⋯ }

@[simp]

theorem GradedRingHom.coe_copy {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_6} {τ : Type u_7} [Semiring A] [Semiring B] [SetLike σ A] [SetLike τ B] {𝒜 : ι → σ} {ℬ : ι → τ} (f : 𝒜 →+*ᵍ ℬ) (f' : A → B) (h : f' = ⇑f) : ⇑(f.copy f' h) = f'

theorem GradedRingHom.copy_eq {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_6} {τ : Type u_7} [Semiring A] [Semiring B] [SetLike σ A] [SetLike τ B] {𝒜 : ι → σ} {ℬ : ι → τ} (f : 𝒜 →+*ᵍ ℬ) (f' : A → B) (h : f' = ⇑f) : f.copy f' h = f

theorem GradedRingHom.congr_fun {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_6} {τ : Type u_7} [Semiring A] [Semiring B] [SetLike σ A] [SetLike τ B] {𝒜 : ι → σ} {ℬ : ι → τ} {f g : 𝒜 →+*ᵍ ℬ} (h : f = g) (x : A) : f x = g x

theorem GradedRingHom.congr_arg {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_6} {τ : Type u_7} [Semiring A] [Semiring B] [SetLike σ A] [SetLike τ B] {𝒜 : ι → σ} {ℬ : ι → τ} (f : 𝒜 →+*ᵍ ℬ) {x y : A} (h : x = y) : f x = f y

theorem GradedRingHom.coe_inj {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_6} {τ : Type u_7} [Semiring A] [Semiring B] [SetLike σ A] [SetLike τ B] {𝒜 : ι → σ} {ℬ : ι → τ} ⦃f g : 𝒜 →+*ᵍ ℬ⦄ (h : ⇑f = ⇑g) : f = g

theorem GradedRingHom.ext {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_6} {τ : Type u_7} [Semiring A] [Semiring B] [SetLike σ A] [SetLike τ B] {𝒜 : ι → σ} {ℬ : ι → τ} ⦃f g : 𝒜 →+*ᵍ ℬ⦄ : (∀ (x : A), f x = g x) → f = g

theorem GradedRingHom.ext_iff {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_6} {τ : Type u_7} [Semiring A] [Semiring B] [SetLike σ A] [SetLike τ B] {𝒜 : ι → σ} {ℬ : ι → τ} {f g : 𝒜 →+*ᵍ ℬ} : f = g ↔ ∀ (x : A), f x = g x

@[simp]

theorem GradedRingHom.mk_coe {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_6} {τ : Type u_7} [Semiring A] [Semiring B] [SetLike σ A] [SetLike τ B] {𝒜 : ι → σ} {ℬ : ι → τ} (f : 𝒜 →+*ᵍ ℬ) (h₁ : f 1 = 1) (h₂ : ∀ (x y : A), { toFun := ⇑f, map_one' := h₁ }.toFun (x * y) = { toFun := ⇑f, map_one' := h₁ }.toFun x * { toFun := ⇑f, map_one' := h₁ }.toFun y) (h₃ : (↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂ }).toFun 0 = 0) (h₄ : ∀ (x y : A), (↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂ }).toFun (x + y) = (↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂ }).toFun x + (↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂ }).toFun y) (h₅ : ∀ {i : ι} {x : A}, x ∈ 𝒜 i → { toFun := ⇑f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄ } x ∈ ℬ i) : { toFun := ⇑f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄, map_mem := h₅ } = f

theorem GradedRingHom.coe_ringHom_injective {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_6} {τ : Type u_7} [Semiring A] [Semiring B] [SetLike σ A] [SetLike τ B] {𝒜 : ι → σ} {ℬ : ι → τ} : Function.Injective fun (f : 𝒜 →+*ᵍ ℬ) => ↑f

theorem GradedRingHom.map_zero {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_6} {τ : Type u_7} [Semiring A] [Semiring B] [SetLike σ A] [SetLike τ B] {𝒜 : ι → σ} {ℬ : ι → τ} (f : 𝒜 →+*ᵍ ℬ) : f 0 = 0

Graded ring homomorphisms map zero to zero.

theorem GradedRingHom.map_one {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_6} {τ : Type u_7} [Semiring A] [Semiring B] [SetLike σ A] [SetLike τ B] {𝒜 : ι → σ} {ℬ : ι → τ} (f : 𝒜 →+*ᵍ ℬ) : f 1 = 1

Graded ring homomorphisms map one to one.

theorem GradedRingHom.map_add {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_6} {τ : Type u_7} [Semiring A] [Semiring B] [SetLike σ A] [SetLike τ B] {𝒜 : ι → σ} {ℬ : ι → τ} (f : 𝒜 →+*ᵍ ℬ) (a b : A) : f (a + b) = f a + f b

Graded ring homomorphisms preserve addition.

theorem GradedRingHom.map_mul {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_6} {τ : Type u_7} [Semiring A] [Semiring B] [SetLike σ A] [SetLike τ B] {𝒜 : ι → σ} {ℬ : ι → τ} (f : 𝒜 →+*ᵍ ℬ) (a b : A) : f (a * b) = f a * f b

Graded ring homomorphisms preserve multiplication.

theorem GradedRingHom.map_neg {ι : Type u_1} {A : Type u_10} {B : Type u_11} {σ : Type u_12} {τ : Type u_13} [Ring A] [Ring B] [SetLike σ A] [SetLike τ B] (𝒜 : ι → σ) (ℬ : ι → τ) (f : 𝒜 →+*ᵍ ℬ) (x : A) : f (-x) = -f x

Graded ring homomorphisms preserve additive inverse.

theorem GradedRingHom.map_sub {ι : Type u_1} {A : Type u_10} {B : Type u_11} {σ : Type u_12} {τ : Type u_13} [Ring A] [Ring B] [SetLike σ A] [SetLike τ B] (𝒜 : ι → σ) (ℬ : ι → τ) (f : 𝒜 →+*ᵍ ℬ) (x y : A) : f (x - y) = f x - f y

Graded ring homomorphisms preserve subtraction.

def GradedRingHom.id {ι : Type u_1} {A : Type u_2} {σ : Type u_6} [Semiring A] [SetLike σ A] (𝒜 : ι → σ) : 𝒜 →+*ᵍ 𝒜

The identity graded ring homomorphism from a graded ring to itself.

Equations

• GradedRingHom.id 𝒜 = { toRingHom := RingHom.id A, map_mem := ⋯ }

@[simp]

theorem GradedRingHom.coe_id {ι : Type u_1} {A : Type u_2} {σ : Type u_6} [Semiring A] [SetLike σ A] {𝒜 : ι → σ} : ⇑(id 𝒜) = _root_.id

@[simp]

theorem GradedRingHom.id_apply {ι : Type u_1} {A : Type u_2} {σ : Type u_6} [Semiring A] [SetLike σ A] {𝒜 : ι → σ} (x : A) : (id 𝒜) x = x

@[simp]

theorem GradedRingHom.toRingHom_id {ι : Type u_1} {A : Type u_2} {σ : Type u_6} [Semiring A] [SetLike σ A] {𝒜 : ι → σ} : ↑(id 𝒜) = RingHom.id A

def GradedRingHom.comp {ι : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} {σ : Type u_6} {τ : Type u_7} {ψ : Type u_8} [Semiring A] [Semiring B] [Semiring C] [SetLike σ A] [SetLike τ B] [SetLike ψ C] {𝒜 : ι → σ} {ℬ : ι → τ} {𝒞 : ι → ψ} (g : ℬ →+*ᵍ 𝒞) (f : 𝒜 →+*ᵍ ℬ) : 𝒜 →+*ᵍ 𝒞

Composition of graded ring homomorphisms is a graded ring homomorphism.

Equations

• g.comp f = { toRingHom := (↑g).comp ↑f, map_mem := ⋯ }

theorem GradedRingHom.comp_assoc {ι : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} {σ : Type u_6} {τ : Type u_7} {ψ : Type u_8} {ω : Type u_9} [Semiring A] [Semiring B] [Semiring C] [Semiring D] [SetLike σ A] [SetLike τ B] [SetLike ψ C] [SetLike ω D] {𝒜 : ι → σ} {ℬ : ι → τ} {𝒞 : ι → ψ} {𝒟 : ι → ω} (h : 𝒞 →+*ᵍ 𝒟) (g : ℬ →+*ᵍ 𝒞) (f : 𝒜 →+*ᵍ ℬ) : (h.comp g).comp f = h.comp (g.comp f)

Composition of graded ring homomorphisms is associative.

@[simp]

theorem GradedRingHom.coe_comp {ι : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} {σ : Type u_6} {τ : Type u_7} {ψ : Type u_8} [Semiring A] [Semiring B] [Semiring C] [SetLike σ A] [SetLike τ B] [SetLike ψ C] {𝒜 : ι → σ} {ℬ : ι → τ} {𝒞 : ι → ψ} (hnp : ℬ →+*ᵍ 𝒞) (hmn : 𝒜 →+*ᵍ ℬ) : ⇑(hnp.comp hmn) = ⇑hnp ∘ ⇑hmn

theorem GradedRingHom.comp_apply {ι : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} {σ : Type u_6} {τ : Type u_7} {ψ : Type u_8} [Semiring A] [Semiring B] [Semiring C] [SetLike σ A] [SetLike τ B] [SetLike ψ C] {𝒜 : ι → σ} {ℬ : ι → τ} {𝒞 : ι → ψ} (hnp : ℬ →+*ᵍ 𝒞) (hmn : 𝒜 →+*ᵍ ℬ) (x : A) : (hnp.comp hmn) x = hnp (hmn x)

@[simp]

theorem GradedRingHom.comp_id {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_6} {τ : Type u_7} [Semiring A] [Semiring B] [SetLike σ A] [SetLike τ B] {𝒜 : ι → σ} {ℬ : ι → τ} (f : 𝒜 →+*ᵍ ℬ) : f.comp (id 𝒜) = f

@[simp]

theorem GradedRingHom.id_comp {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_6} {τ : Type u_7} [Semiring A] [Semiring B] [SetLike σ A] [SetLike τ B] {𝒜 : ι → σ} {ℬ : ι → τ} (f : 𝒜 →+*ᵍ ℬ) : (id ℬ).comp f = f

@[implicit_reducible]

instance GradedRingHom.instOne {ι : Type u_1} {A : Type u_2} {σ : Type u_6} [Semiring A] [SetLike σ A] {𝒜 : ι → σ} : One (𝒜 →+*ᵍ 𝒜)

Equations

• GradedRingHom.instOne = { one := GradedRingHom.id 𝒜 }

@[implicit_reducible]

instance GradedRingHom.instMul {ι : Type u_1} {A : Type u_2} {σ : Type u_6} [Semiring A] [SetLike σ A] {𝒜 : ι → σ} : Mul (𝒜 →+*ᵍ 𝒜)

Equations

• GradedRingHom.instMul = { mul := GradedRingHom.comp }

theorem GradedRingHom.one_def {ι : Type u_1} {A : Type u_2} {σ : Type u_6} [Semiring A] [SetLike σ A] {𝒜 : ι → σ} : 1 = id 𝒜

theorem GradedRingHom.mul_def {ι : Type u_1} {A : Type u_2} {σ : Type u_6} [Semiring A] [SetLike σ A] {𝒜 : ι → σ} (f g : 𝒜 →+*ᵍ 𝒜) : f * g = f.comp g

@[simp]

theorem GradedRingHom.coe_one {ι : Type u_1} {A : Type u_2} {σ : Type u_6} [Semiring A] [SetLike σ A] {𝒜 : ι → σ} : ⇑1 = _root_.id

@[simp]

theorem GradedRingHom.coe_mul {ι : Type u_1} {A : Type u_2} {σ : Type u_6} [Semiring A] [SetLike σ A] {𝒜 : ι → σ} (f g : 𝒜 →+*ᵍ 𝒜) : ⇑(f * g) = ⇑f ∘ ⇑g

@[implicit_reducible]

instance GradedRingHom.instMonoid {ι : Type u_1} {A : Type u_2} {σ : Type u_6} [Semiring A] [SetLike σ A] {𝒜 : ι → σ} : Monoid (𝒜 →+*ᵍ 𝒜)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem GradedRingHom.coe_pow {ι : Type u_1} {A : Type u_2} {σ : Type u_6} [Semiring A] [SetLike σ A] {𝒜 : ι → σ} (f : 𝒜 →+*ᵍ 𝒜) (n : ℕ) : ⇑(f ^ n) = (⇑f)^[n]

@[simp]

theorem GradedRingHom.cancel_right {ι : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} {σ : Type u_6} {τ : Type u_7} {ψ : Type u_8} [Semiring A] [Semiring B] [Semiring C] [SetLike σ A] [SetLike τ B] [SetLike ψ C] {𝒜 : ι → σ} {ℬ : ι → τ} {𝒞 : ι → ψ} {g₁ g₂ : ℬ →+*ᵍ 𝒞} {f : 𝒜 →+*ᵍ ℬ} (hf : Function.Surjective ⇑f) : g₁.comp f = g₂.comp f ↔ g₁ = g₂

@[simp]

theorem GradedRingHom.cancel_left {ι : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} {σ : Type u_6} {τ : Type u_7} {ψ : Type u_8} [Semiring A] [Semiring B] [Semiring C] [SetLike σ A] [SetLike τ B] [SetLike ψ C] {𝒜 : ι → σ} {ℬ : ι → τ} {𝒞 : ι → ψ} {g : ℬ →+*ᵍ 𝒞} {f₁ f₂ : 𝒜 →+*ᵍ ℬ} (hg : Function.Injective ⇑g) : g.comp f₁ = g.comp f₂ ↔ f₁ = f₂

def GradedRingHom.gradedAddHom {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_6} {τ : Type u_7} [Semiring A] [Semiring B] [SetLike σ A] [SetLike τ B] {𝒜 : ι → σ} {ℬ : ι → τ} [AddSubmonoidClass σ A] [AddSubmonoidClass τ B] (f : 𝒜 →+*ᵍ ℬ) (i : ι) : ↥(𝒜 i) →+ ↥(ℬ i)

A graded ring homomorphism descends to an additive homomorphism on each indexed component.

Equations

• f.gradedAddHom i = { toFun := fun (x : ↥(𝒜 i)) => ⟨f ↑x, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem GradedRingHom.gradedAddHom_apply_coe {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_6} {τ : Type u_7} [Semiring A] [Semiring B] [SetLike σ A] [SetLike τ B] {𝒜 : ι → σ} {ℬ : ι → τ} [AddSubmonoidClass σ A] [AddSubmonoidClass τ B] (f : 𝒜 →+*ᵍ ℬ) (i : ι) (x : ↥(𝒜 i)) : ↑((f.gradedAddHom i) x) = f ↑x

def GradedRingHom.gradedZeroRingHom {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_6} {τ : Type u_7} [Semiring A] [Semiring B] [SetLike σ A] [SetLike τ B] {𝒜 : ι → σ} {ℬ : ι → τ} [AddSubmonoidClass σ A] [AddSubmonoidClass τ B] [AddMonoid ι] [SetLike.GradedMonoid 𝒜] [SetLike.GradedMonoid ℬ] (f : 𝒜 →+*ᵍ ℬ) : ↥(𝒜 0) →+* ↥(ℬ 0)

A graded ring homomorphism descends to a ring homomorphism on the zeroth component.

Equations

• f.gradedZeroRingHom = { toFun := (↑(f.gradedAddHom 0)).toFun, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem GradedRingHom.gradedZeroRingHom_apply_coe {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_6} {τ : Type u_7} [Semiring A] [Semiring B] [SetLike σ A] [SetLike τ B] {𝒜 : ι → σ} {ℬ : ι → τ} [AddSubmonoidClass σ A] [AddSubmonoidClass τ B] [AddMonoid ι] [SetLike.GradedMonoid 𝒜] [SetLike.GradedMonoid ℬ] (f : 𝒜 →+*ᵍ ℬ) (a✝ : ↥(𝒜 0)) : ↑(f.gradedZeroRingHom a✝) = f ↑a✝

theorem DirectSum.decompose_map {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_6} {τ : Type u_7} [Semiring A] [Semiring B] [SetLike σ A] [SetLike τ B] [DecidableEq ι] [AddMonoid ι] [AddSubmonoidClass σ A] [AddSubmonoidClass τ B] (𝒜 : ι → σ) (ℬ : ι → τ) [GradedRing 𝒜] [GradedRing ℬ] {F : Type u_10} [FunLike F A B] [GradedFunLike F 𝒜 ℬ] [RingHomClass F A B] (f : F) {x : A} : (decompose ℬ) (f x) = (map (↑f).gradedAddHom) ((decompose 𝒜) x)

theorem map_directSumDecompose {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_6} {τ : Type u_7} [Semiring A] [Semiring B] [SetLike σ A] [SetLike τ B] [DecidableEq ι] [AddMonoid ι] [AddSubmonoidClass σ A] [AddSubmonoidClass τ B] (𝒜 : ι → σ) (ℬ : ι → τ) [GradedRing 𝒜] [GradedRing ℬ] {F : Type u_10} [FunLike F A B] [GradedFunLike F 𝒜 ℬ] [RingHomClass F A B] (f : F) {x : A} {i : ι} : f ↑(((DirectSum.decompose 𝒜) x) i) = ↑(((DirectSum.decompose ℬ) (f x)) i)

@[simp]

theorem GradedRingHom.map_directSumDecompose {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_6} {τ : Type u_7} [Semiring A] [Semiring B] [SetLike σ A] [SetLike τ B] [DecidableEq ι] [AddMonoid ι] [AddSubmonoidClass σ A] [AddSubmonoidClass τ B] (𝒜 : ι → σ) (ℬ : ι → τ) [GradedRing 𝒜] [GradedRing ℬ] (f : 𝒜 →+*ᵍ ℬ) {x : A} {i : ι} : f ↑(((DirectSum.decompose 𝒜) x) i) = ↑(((DirectSum.decompose ℬ) (f x)) i)