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_mapwhich 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_mem {i : ι} {x : A} : x ∈ 𝒜 i → ↑self x ∈ ℬ i
Instances For
Bundled graded (semi)ring homomorphisms. Use GradedRingHom for the namespace and other
identifiers, and 𝒜 →+*ᵍ ℬ for the notation.
Instances For
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.
Instances For
@[simp]
@[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
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.
Instances For
@[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)
:
@[simp]
@[simp]
@[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.
Instances For
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 : 𝒜 →+*ᵍ ℬ)
:
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)
@[implicit_reducible]
@[implicit_reducible]
@[simp]
@[simp]
@[implicit_reducible]
@[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)
:
@[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)
:
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 : ι)
:
A graded ring homomorphism descends to an additive homomorphism on each indexed component.
Instances For
@[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 : 𝒜 →+*ᵍ ℬ)
:
A graded ring homomorphism descends to a ring homomorphism on the zeroth component.
Instances For
@[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)