R-linear homomorphisms of graded algebras

This file defines bundled R-linear homomorphisms of graded R-algebras.

Main definitions

• GradedAlgHom R 𝒜 ℬ: the type of R-linear homomorphisms of R-graded algebras 𝒜 to ℬ.

Notation

• 𝒜 →ₐᵍ[R] ℬ : R-linear graded homomorphism from 𝒜 to ℬ.

structure GradedAlgHom (R : Type u_1) {A : Type u_2} {B : Type u_3} {ι : Type u_4} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [DecidableEq ι] [AddMonoid ι] (𝒜 : ι → Submodule R A) (ℬ : ι → Submodule R B) [GradedAlgebra 𝒜] [GradedAlgebra ℬ] extends A →ₐ[R] B, 𝒜 →+*ᵍ ℬ : Type (max u_2 u_3)

An R-linear homomorphism of graded algebras, denoted 𝒜 →ₐᵍ[R] ℬ.

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

def «term_→ₐᵍ[_]_» : Lean.TrailingParserDescr

An R-linear homomorphism of graded algebras, denoted 𝒜 →ₐᵍ[R] ℬ.

Equations

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

def GradedAlgHom.ofClass {R : Type u_1} {A : Type u_6} {B : Type u_7} {ι : Type u_10} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [DecidableEq ι] [AddMonoid ι] {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [GradedAlgebra 𝒜] [GradedAlgebra ℬ] {F : Type u_11} [FunLike F A B] [GradedFunLike F 𝒜 ℬ] [AlgHomClass F R A B] (f : F) : 𝒜 →ₐᵍ[R] ℬ

Turn an element of a type F satisfying [FunLike F A B] [GradedFunLike F 𝒜 ℬ] [AlgHomClass F R A B] into an actual GradedAlgHom.

In future mathlib this will be deprioritised in favour of using structural projections.

Equations

• GradedAlgHom.ofClass f = { toAlgHom := ↑f, map_mem := ⋯ }

@[implicit_reducible]

instance GradedAlgHom.instFunLike {R : Type u_1} {A : Type u_6} {B : Type u_7} {ι : Type u_10} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [DecidableEq ι] [AddMonoid ι] {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [GradedAlgebra 𝒜] [GradedAlgebra ℬ] : FunLike (𝒜 →ₐᵍ[R] ℬ) A B

Equations

• GradedAlgHom.instFunLike = { coe := fun (f : 𝒜 →ₐᵍ[R] ℬ) => (↑↑f.toRingHom).toFun, coe_injective' := ⋯ }

instance GradedAlgHom.instGradedFunLikeSubmodule {R : Type u_1} {A : Type u_6} {B : Type u_7} {ι : Type u_10} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [DecidableEq ι] [AddMonoid ι] {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [GradedAlgebra 𝒜] [GradedAlgebra ℬ] : GradedFunLike (𝒜 →ₐᵍ[R] ℬ) 𝒜 ℬ

instance GradedAlgHom.instAlgHomClass {R : Type u_1} {A : Type u_6} {B : Type u_7} {ι : Type u_10} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [DecidableEq ι] [AddMonoid ι] {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [GradedAlgebra 𝒜] [GradedAlgebra ℬ] : AlgHomClass (𝒜 →ₐᵍ[R] ℬ) R A B

@[simp]

theorem GradedAlgHom.toAlgHom_ofClass {R : Type u_1} {A : Type u_6} {B : Type u_7} {ι : Type u_10} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [DecidableEq ι] [AddMonoid ι] {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [GradedAlgebra 𝒜] [GradedAlgebra ℬ] {F : Type u_11} [FunLike F A B] [GradedFunLike F 𝒜 ℬ] [AlgHomClass F R A B] (f : F) : ↑(ofClass f) = ↑f

@[simp]

theorem GradedAlgHom.toGradedRingHom_ofClass {R : Type u_1} {A : Type u_6} {B : Type u_7} {ι : Type u_10} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [DecidableEq ι] [AddMonoid ι] {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [GradedAlgebra 𝒜] [GradedAlgebra ℬ] {F : Type u_11} [FunLike F A B] [GradedFunLike F 𝒜 ℬ] [AlgHomClass F R A B] (f : F) : (ofClass f).toGradedRingHom = ↑f

@[simp]

theorem GradedAlgHom.coe_ofClass {R : Type u_1} {A : Type u_6} {B : Type u_7} {ι : Type u_10} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [DecidableEq ι] [AddMonoid ι] {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [GradedAlgebra 𝒜] [GradedAlgebra ℬ] {F : Type u_11} [FunLike F A B] [GradedFunLike F 𝒜 ℬ] [AlgHomClass F R A B] (f : F) : ⇑(ofClass f) = ⇑f

@[simp]

theorem GradedAlgHom.coe_toAlgHom {R : Type u_1} {A : Type u_6} {B : Type u_7} {ι : Type u_10} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [DecidableEq ι] [AddMonoid ι] {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [GradedAlgebra 𝒜] [GradedAlgebra ℬ] (f : 𝒜 →ₐᵍ[R] ℬ) : ⇑f.toAlgHom = ⇑f

@[simp]

theorem GradedAlgHom.coe_mk {R : Type u_1} {A : Type u_6} {B : Type u_7} {ι : Type u_10} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [DecidableEq ι] [AddMonoid ι] {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [GradedAlgebra 𝒜] [GradedAlgebra ℬ] {f : A →ₐ[R] B} (h : ∀ {i : ι} {x : A}, x ∈ 𝒜 i → f.toRingHom x ∈ ℬ i) : ⇑{ toAlgHom := f, map_mem := h } = ⇑f

theorem GradedAlgHom.coe_mks {R : Type u_1} {A : Type u_6} {B : Type u_7} {ι : Type u_10} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [DecidableEq ι] [AddMonoid ι] {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [GradedAlgebra 𝒜] [GradedAlgebra ℬ] {f : A → B} (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₅ : ∀ (r : R), (↑↑{ toFun := f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄ }).toFun ((algebraMap R A) r) = (algebraMap R B) r) (h₆ : ∀ {i : ι} {x : A}, x ∈ 𝒜 i → { toFun := f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄, commutes' := h₅ }.toRingHom x ∈ ℬ i) : ⇑{ toFun := f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄, commutes' := h₅, map_mem := h₆ } = f

@[simp]

theorem GradedAlgHom.coe_algHom_mk {R : Type u_1} {A : Type u_6} {B : Type u_7} {ι : Type u_10} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [DecidableEq ι] [AddMonoid ι] {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [GradedAlgebra 𝒜] [GradedAlgebra ℬ] {f : A →ₐ[R] B} (h : ∀ {i : ι} {x : A}, x ∈ 𝒜 i → f.toRingHom x ∈ ℬ i) : ↑{ toAlgHom := f, map_mem := h } = f

theorem GradedAlgHom.coe_fn_injective {R : Type u_1} {A : Type u_6} {B : Type u_7} {ι : Type u_10} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [DecidableEq ι] [AddMonoid ι] {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [GradedAlgebra 𝒜] [GradedAlgebra ℬ] : Function.Injective DFunLike.coe

theorem GradedAlgHom.coe_fn_inj {R : Type u_1} {A : Type u_6} {B : Type u_7} {ι : Type u_10} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [DecidableEq ι] [AddMonoid ι] {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [GradedAlgebra 𝒜] [GradedAlgebra ℬ] {f₁ f₂ : 𝒜 →ₐᵍ[R] ℬ} : ⇑f₁ = ⇑f₂ ↔ f₁ = f₂

theorem GradedAlgHom.coe_algHom_injective {R : Type u_1} {A : Type u_6} {B : Type u_7} {ι : Type u_10} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [DecidableEq ι] [AddMonoid ι] {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [GradedAlgebra 𝒜] [GradedAlgebra ℬ] : Function.Injective AlgHomClass.toAlgHom

theorem GradedAlgHom.toGradedRingHom_injective {R : Type u_1} {A : Type u_6} {B : Type u_7} {ι : Type u_10} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [DecidableEq ι] [AddMonoid ι] {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [GradedAlgebra 𝒜] [GradedAlgebra ℬ] : Function.Injective toGradedRingHom

theorem GradedAlgHom.coe_linearMap_injective {R : Type u_1} {A : Type u_6} {B : Type u_7} {ι : Type u_10} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [DecidableEq ι] [AddMonoid ι] {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [GradedAlgebra 𝒜] [GradedAlgebra ℬ] : Function.Injective fun (x : 𝒜 →ₐᵍ[R] ℬ) => ↑x

theorem GradedAlgHom.coe_ringHom_injective {R : Type u_1} {A : Type u_6} {B : Type u_7} {ι : Type u_10} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [DecidableEq ι] [AddMonoid ι] {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [GradedAlgebra 𝒜] [GradedAlgebra ℬ] : Function.Injective RingHomClass.toRingHom

theorem GradedAlgHom.coe_monoidHom_injective {R : Type u_1} {A : Type u_6} {B : Type u_7} {ι : Type u_10} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [DecidableEq ι] [AddMonoid ι] {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [GradedAlgebra 𝒜] [GradedAlgebra ℬ] : Function.Injective MonoidHomClass.toMonoidHom

theorem GradedAlgHom.coe_addMonoidHom_injective {R : Type u_1} {A : Type u_6} {B : Type u_7} {ι : Type u_10} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [DecidableEq ι] [AddMonoid ι] {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [GradedAlgebra 𝒜] [GradedAlgebra ℬ] : Function.Injective AddMonoidHomClass.toAddMonoidHom

theorem GradedAlgHom.congr_fun {R : Type u_1} {A : Type u_6} {B : Type u_7} {ι : Type u_10} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [DecidableEq ι] [AddMonoid ι] {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [GradedAlgebra 𝒜] [GradedAlgebra ℬ] {f₁ f₂ : 𝒜 →ₐᵍ[R] ℬ} (H : f₁ = f₂) (x : A) : f₁ x = f₂ x

Consider using congr($H x) instead.

theorem GradedAlgHom.congr_arg {R : Type u_1} {A : Type u_6} {B : Type u_7} {ι : Type u_10} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [DecidableEq ι] [AddMonoid ι] {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [GradedAlgebra 𝒜] [GradedAlgebra ℬ] (f : 𝒜 →ₐᵍ[R] ℬ) {x y : A} (h : x = y) : f x = f y

Consider using congr(f $h) instead.

theorem GradedAlgHom.ext {R : Type u_1} {A : Type u_6} {B : Type u_7} {ι : Type u_10} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [DecidableEq ι] [AddMonoid ι] {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [GradedAlgebra 𝒜] [GradedAlgebra ℬ] {f₁ f₂ : 𝒜 →ₐᵍ[R] ℬ} (H : ∀ (x : A), f₁ x = f₂ x) : f₁ = f₂

theorem GradedAlgHom.ext_iff {R : Type u_1} {A : Type u_6} {B : Type u_7} {ι : Type u_10} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [DecidableEq ι] [AddMonoid ι] {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [GradedAlgebra 𝒜] [GradedAlgebra ℬ] {f₁ f₂ : 𝒜 →ₐᵍ[R] ℬ} : f₁ = f₂ ↔ ∀ (x : A), f₁ x = f₂ x

@[simp]

theorem GradedAlgHom.mk_coe {R : Type u_1} {A : Type u_6} {B : Type u_7} {ι : Type u_10} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [DecidableEq ι] [AddMonoid ι] {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [GradedAlgebra 𝒜] [GradedAlgebra ℬ] {f : 𝒜 →ₐᵍ[R] ℬ} (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₅ : ∀ (r : R), (↑↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄ }).toFun ((algebraMap R A) r) = (algebraMap R B) r) (h₆ : ∀ {i : ι} {x : A}, x ∈ 𝒜 i → { toFun := ⇑f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄, commutes' := h₅ }.toRingHom x ∈ ℬ i) : { toFun := ⇑f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄, commutes' := h₅, map_mem := h₆ } = f

@[simp]

theorem GradedAlgHom.commutes {R : Type u_1} {A : Type u_6} {B : Type u_7} {ι : Type u_10} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [DecidableEq ι] [AddMonoid ι] {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [GradedAlgebra 𝒜] [GradedAlgebra ℬ] (f : 𝒜 →ₐᵍ[R] ℬ) (r : R) : f ((algebraMap R A) r) = (algebraMap R B) r

theorem GradedAlgHom.comp_ofId {R : Type u_1} {A : Type u_6} {B : Type u_7} {ι : Type u_10} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [DecidableEq ι] [AddMonoid ι] {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [GradedAlgebra 𝒜] [GradedAlgebra ℬ] (f : 𝒜 →ₐᵍ[R] ℬ) : (↑f).comp (Algebra.ofId R A) = Algebra.ofId R B

def GradedAlgHom.mk' {R : Type u_1} {A : Type u_6} {B : Type u_7} {ι : Type u_10} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [DecidableEq ι] [AddMonoid ι] {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [GradedAlgebra 𝒜] [GradedAlgebra ℬ] (f : 𝒜 →+*ᵍ ℬ) (h : ∀ (c : R) (x : A), f (c • x) = c • f x) : 𝒜 →ₐᵍ[R] ℬ

If a GradedRingHom is R-linear, then it is a GradedAlgHom.

Equations

• GradedAlgHom.mk' f h = { toAlgHom := AlgHom.mk' (↑f) h, map_mem := ⋯ }

@[simp]

theorem GradedAlgHom.coe_mk' {R : Type u_1} {A : Type u_6} {B : Type u_7} {ι : Type u_10} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [DecidableEq ι] [AddMonoid ι] {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [GradedAlgebra 𝒜] [GradedAlgebra ℬ] (f : 𝒜 →+*ᵍ ℬ) (h : ∀ (c : R) (x : A), f (c • x) = c • f x) : ⇑(mk' f h) = ⇑f

def GradedAlgHom.id (R : Type u_1) {A : Type u_6} {ι : Type u_10} [CommSemiring R] [Semiring A] [Algebra R A] [DecidableEq ι] [AddMonoid ι] (𝒜 : ι → Submodule R A) [GradedAlgebra 𝒜] : 𝒜 →ₐᵍ[R] 𝒜

Identity map as a GradedAlgHom.

Equations

• GradedAlgHom.id R 𝒜 = { toAlgHom := AlgHom.id R A, map_mem := ⋯ }

@[simp]

theorem GradedAlgHom.id_apply (R : Type u_1) {A : Type u_6} {ι : Type u_10} [CommSemiring R] [Semiring A] [Algebra R A] [DecidableEq ι] [AddMonoid ι] (𝒜 : ι → Submodule R A) [GradedAlgebra 𝒜] (a : A) : (GradedAlgHom.id R 𝒜) a = a

@[simp]

theorem GradedAlgHom.coe_id (R : Type u_1) {A : Type u_6} {ι : Type u_10} [CommSemiring R] [Semiring A] [Algebra R A] [DecidableEq ι] [AddMonoid ι] (𝒜 : ι → Submodule R A) [GradedAlgebra 𝒜] : ⇑(GradedAlgHom.id R 𝒜) = id

@[simp]

theorem GradedAlgHom.id_toAlgHom (R : Type u_1) {A : Type u_6} {ι : Type u_10} [CommSemiring R] [Semiring A] [Algebra R A] [DecidableEq ι] [AddMonoid ι] (𝒜 : ι → Submodule R A) [GradedAlgebra 𝒜] : ↑(GradedAlgHom.id R 𝒜) = AlgHom.id R A

def GradedAlgHom.comp {R : Type u_1} {A : Type u_6} {B : Type u_7} {C : Type u_8} {ι : Type u_10} [CommSemiring R] [Semiring A] [Semiring B] [Semiring C] [Algebra R A] [Algebra R B] [Algebra R C] [DecidableEq ι] [AddMonoid ι] {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} {𝒞 : ι → Submodule R C} [GradedAlgebra 𝒜] [GradedAlgebra ℬ] [GradedAlgebra 𝒞] (g : ℬ →ₐᵍ[R] 𝒞) (f : 𝒜 →ₐᵍ[R] ℬ) : 𝒜 →ₐᵍ[R] 𝒞

If g and f are R-linear graded algebra homomorphisms with the domain of g equal to the codomain of f, then g.comp f is the graded algebra homomorphism x ↦ g (f x).

Equations

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

@[simp]

theorem GradedAlgHom.comp_apply {R : Type u_1} {A : Type u_6} {B : Type u_7} {C : Type u_8} {ι : Type u_10} [CommSemiring R] [Semiring A] [Semiring B] [Semiring C] [Algebra R A] [Algebra R B] [Algebra R C] [DecidableEq ι] [AddMonoid ι] {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} {𝒞 : ι → Submodule R C} [GradedAlgebra 𝒜] [GradedAlgebra ℬ] [GradedAlgebra 𝒞] (g : ℬ →ₐᵍ[R] 𝒞) (f : 𝒜 →ₐᵍ[R] ℬ) (a✝ : A) : (g.comp f) a✝ = g (f a✝)

@[simp]

theorem GradedAlgHom.coe_comp {R : Type u_1} {A : Type u_6} {B : Type u_7} {C : Type u_8} {ι : Type u_10} [CommSemiring R] [Semiring A] [Semiring B] [Semiring C] [Algebra R A] [Algebra R B] [Algebra R C] [DecidableEq ι] [AddMonoid ι] {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [GradedAlgebra 𝒜] [GradedAlgebra ℬ] (g : B →ₐ[R] C) (f : 𝒜 →ₐᵍ[R] ℬ) : ⇑(g.comp ↑f) = ⇑g ∘ ⇑f

theorem GradedAlgHom.comp_toGradedRingHom {R : Type u_1} {A : Type u_6} {B : Type u_7} {C : Type u_8} {ι : Type u_10} [CommSemiring R] [Semiring A] [Semiring B] [Semiring C] [Algebra R A] [Algebra R B] [Algebra R C] [DecidableEq ι] [AddMonoid ι] {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} {𝒞 : ι → Submodule R C} [GradedAlgebra 𝒜] [GradedAlgebra ℬ] [GradedAlgebra 𝒞] (g : ℬ →ₐᵍ[R] 𝒞) (f : 𝒜 →ₐᵍ[R] ℬ) : (g.comp f).toGradedRingHom = g.toGradedRingHom.comp f.toGradedRingHom

theorem GradedAlgHom.comp_toAlgHom {R : Type u_1} {A : Type u_6} {B : Type u_7} {C : Type u_8} {ι : Type u_10} [CommSemiring R] [Semiring A] [Semiring B] [Semiring C] [Algebra R A] [Algebra R B] [Algebra R C] [DecidableEq ι] [AddMonoid ι] {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} {𝒞 : ι → Submodule R C} [GradedAlgebra 𝒜] [GradedAlgebra ℬ] [GradedAlgebra 𝒞] (g : ℬ →ₐᵍ[R] 𝒞) (f : 𝒜 →ₐᵍ[R] ℬ) : ↑(g.comp f) = (↑g).comp ↑f

@[simp]

theorem GradedAlgHom.comp_id {R : Type u_1} {A : Type u_6} {B : Type u_7} {ι : Type u_10} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [DecidableEq ι] [AddMonoid ι] {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [GradedAlgebra 𝒜] [GradedAlgebra ℬ] (f : 𝒜 →ₐᵍ[R] ℬ) : f.comp (GradedAlgHom.id R 𝒜) = f

@[simp]

theorem GradedAlgHom.id_comp {R : Type u_1} {A : Type u_6} {B : Type u_7} {ι : Type u_10} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [DecidableEq ι] [AddMonoid ι] {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [GradedAlgebra 𝒜] [GradedAlgebra ℬ] (f : 𝒜 →ₐᵍ[R] ℬ) : (GradedAlgHom.id R ℬ).comp f = f

theorem GradedAlgHom.comp_assoc {R : Type u_1} {A : Type u_6} {B : Type u_7} {C : Type u_8} {D : Type u_9} {ι : Type u_10} [CommSemiring R] [Semiring A] [Semiring B] [Semiring C] [Semiring D] [Algebra R A] [Algebra R B] [Algebra R C] [Algebra R D] [DecidableEq ι] [AddMonoid ι] {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} {𝒞 : ι → Submodule R C} {𝒟 : ι → Submodule R D} [GradedAlgebra 𝒜] [GradedAlgebra ℬ] [GradedAlgebra 𝒞] [GradedAlgebra 𝒟] (fCD : 𝒞 →ₐᵍ[R] 𝒟) (fBC : ℬ →ₐᵍ[R] 𝒞) (fAB : 𝒜 →ₐᵍ[R] ℬ) : (fCD.comp fBC).comp fAB = fCD.comp (fBC.comp fAB)

@[implicit_reducible]

instance GradedAlgHom.instMonoid {R : Type u_1} {A : Type u_6} {ι : Type u_10} [CommSemiring R] [Semiring A] [Algebra R A] [DecidableEq ι] [AddMonoid ι] {𝒜 : ι → Submodule R A} [GradedAlgebra 𝒜] : Monoid (𝒜 →ₐᵍ[R] 𝒜)

Equations

• GradedAlgHom.instMonoid = { mul := GradedAlgHom.comp, mul_assoc := ⋯, one := GradedAlgHom.id R 𝒜, one_mul := ⋯, mul_one := ⋯, npow_zero := ⋯, npow_succ := ⋯ }

theorem GradedAlgHom.toOne_one {R : Type u_1} {A : Type u_6} {ι : Type u_10} [CommSemiring R] [Semiring A] [Algebra R A] [DecidableEq ι] [AddMonoid ι] {𝒜 : ι → Submodule R A} [GradedAlgebra 𝒜] : 1 = GradedAlgHom.id R 𝒜

theorem GradedAlgHom.toSemigroup_toMul_mul {R : Type u_1} {A : Type u_6} {ι : Type u_10} [CommSemiring R] [Semiring A] [Algebra R A] [DecidableEq ι] [AddMonoid ι] {𝒜 : ι → Submodule R A} [GradedAlgebra 𝒜] (g f : 𝒜 →ₐᵍ[R] 𝒜) : g * f = g.comp f

@[simp]

theorem GradedAlgHom.coe_one {R : Type u_1} {A : Type u_6} {ι : Type u_10} [CommSemiring R] [Semiring A] [Algebra R A] [DecidableEq ι] [AddMonoid ι] {𝒜 : ι → Submodule R A} [GradedAlgebra 𝒜] : ⇑1 = id

@[simp]

theorem GradedAlgHom.coe_mul {R : Type u_1} {A : Type u_6} {ι : Type u_10} [CommSemiring R] [Semiring A] [Algebra R A] [DecidableEq ι] [AddMonoid ι] {𝒜 : ι → Submodule R A} [GradedAlgebra 𝒜] (f g : 𝒜 →ₐᵍ[R] 𝒜) : ⇑(f * g) = ⇑f ∘ ⇑g

@[simp]

theorem GradedAlgHom.coe_pow {R : Type u_1} {A : Type u_6} {ι : Type u_10} [CommSemiring R] [Semiring A] [Algebra R A] [DecidableEq ι] [AddMonoid ι] {𝒜 : ι → Submodule R A} [GradedAlgebra 𝒜] (f : 𝒜 →ₐᵍ[R] 𝒜) (n : ℕ) : ⇑(f ^ n) = (⇑f)^[n]

theorem GradedAlgHom.cancel_right {R : Type u_1} {A : Type u_6} {B : Type u_7} {C : Type u_8} {ι : Type u_10} [CommSemiring R] [Semiring A] [Semiring B] [Semiring C] [Algebra R A] [Algebra R B] [Algebra R C] [DecidableEq ι] [AddMonoid ι] {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} {𝒞 : ι → Submodule R C} [GradedAlgebra 𝒜] [GradedAlgebra ℬ] [GradedAlgebra 𝒞] {g₁ g₂ : ℬ →ₐᵍ[R] 𝒞} {f : 𝒜 →ₐᵍ[R] ℬ} (hf : Function.Surjective ⇑f) : g₁.comp f = g₂.comp f ↔ g₁ = g₂

theorem GradedAlgHom.cancel_left {R : Type u_1} {A : Type u_6} {B : Type u_7} {C : Type u_8} {ι : Type u_10} [CommSemiring R] [Semiring A] [Semiring B] [Semiring C] [Algebra R A] [Algebra R B] [Algebra R C] [DecidableEq ι] [AddMonoid ι] {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} {𝒞 : ι → Submodule R C} [GradedAlgebra 𝒜] [GradedAlgebra ℬ] [GradedAlgebra 𝒞] {g₁ g₂ : 𝒜 →ₐᵍ[R] ℬ} {f : ℬ →ₐᵍ[R] 𝒞} (hf : Function.Injective ⇑f) : f.comp g₁ = f.comp g₂ ↔ g₁ = g₂

def GradedAlgHom.toEnd {R : Type u_1} {A : Type u_6} {ι : Type u_10} [CommSemiring R] [Semiring A] [Algebra R A] [DecidableEq ι] [AddMonoid ι] {𝒜 : ι → Submodule R A} [GradedAlgebra 𝒜] : (𝒜 →ₐᵍ[R] 𝒜) →* A →ₐ[R] A

We enrich the existing function toAlgHom with the structure of a MonoidHom, to produce a bundled function that we now call toEnd.

Equations

• GradedAlgHom.toEnd = { toFun := GradedAlgHom.toAlgHom, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem GradedAlgHom.toEnd_apply {R : Type u_1} {A : Type u_6} {ι : Type u_10} [CommSemiring R] [Semiring A] [Algebra R A] [DecidableEq ι] [AddMonoid ι] {𝒜 : ι → Submodule R A} [GradedAlgebra 𝒜] (self : 𝒜 →ₐᵍ[R] 𝒜) : toEnd self = self.toAlgHom

@[implicit_reducible]

instance GradedAlgHom.instUnique {R : Type u_1} {A : Type u_6} {B : Type u_7} {ι : Type u_10} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [DecidableEq ι] [AddMonoid ι] {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [GradedAlgebra 𝒜] [GradedAlgebra ℬ] [Subsingleton B] : Unique (𝒜 →ₐᵍ[R] ℬ)

Equations

• GradedAlgHom.instUnique = { default := let __src := default; { toAlgHom := __src, map_mem := ⋯ }, uniq := ⋯ }

@[simp]

theorem GradedAlgHom.default_apply {R : Type u_1} {A : Type u_6} {B : Type u_7} {ι : Type u_10} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [DecidableEq ι] [AddMonoid ι] {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [GradedAlgebra 𝒜] [GradedAlgebra ℬ] [Subsingleton B] (x : A) : default x = 0

def GradedAlgHom.restrictScalars {R : Type u_1} {A : Type u_6} {B : Type u_7} {ι : Type u_10} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [DecidableEq ι] [AddMonoid ι] {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [GradedAlgebra 𝒜] [GradedAlgebra ℬ] (R₀ : Type u_11) [CommSemiring R₀] [Algebra R₀ R] [Algebra R₀ A] [Algebra R₀ B] [IsScalarTower R₀ R A] [IsScalarTower R₀ R B] (f : 𝒜 →ₐᵍ[R] ℬ) : (fun (x : ι) => Submodule.restrictScalars R₀ (𝒜 x)) →ₐᵍ[R₀] fun (x : ι) => Submodule.restrictScalars R₀ (ℬ x)

Restrict the base ring to a "smaller" ring.

Equations

• ↑R₀ f = { toAlgHom := AlgHom.restrictScalars R₀ f.toAlgHom, map_mem := ⋯ }

@[simp]

theorem GradedAlgHom.restrictScalars_apply {R : Type u_1} {A : Type u_6} {B : Type u_7} {ι : Type u_10} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [DecidableEq ι] [AddMonoid ι] {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [GradedAlgebra 𝒜] [GradedAlgebra ℬ] (R₀ : Type u_11) [CommSemiring R₀] [Algebra R₀ R] [Algebra R₀ A] [Algebra R₀ B] [IsScalarTower R₀ R A] [IsScalarTower R₀ R B] (f : 𝒜 →ₐᵍ[R] ℬ) (a✝ : A) : (↑R₀ f) a✝ = f a✝

@[simp]

theorem GradedAlgHom.coe_restrictScalars {R : Type u_1} {A : Type u_6} {B : Type u_7} {ι : Type u_10} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [DecidableEq ι] [AddMonoid ι] {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [GradedAlgebra 𝒜] [GradedAlgebra ℬ] (R₀ : Type u_11) [CommSemiring R₀] [Algebra R₀ R] [Algebra R₀ A] [Algebra R₀ B] [IsScalarTower R₀ R A] [IsScalarTower R₀ R B] (f : 𝒜 →ₐᵍ[R] ℬ) : ⇑(↑R₀ f) = ⇑f

@[simp]

theorem GradedAlgHom.restrictScalars_coe_algHom {R : Type u_1} {A : Type u_6} {B : Type u_7} {ι : Type u_10} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [DecidableEq ι] [AddMonoid ι] {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [GradedAlgebra 𝒜] [GradedAlgebra ℬ] (R₀ : Type u_11) [CommSemiring R₀] [Algebra R₀ R] [Algebra R₀ A] [Algebra R₀ B] [IsScalarTower R₀ R A] [IsScalarTower R₀ R B] (f : 𝒜 →ₐᵍ[R] ℬ) : AlgHom.restrictScalars R₀ ↑f = ↑(↑R₀ f)

@[simp]

theorem GradedAlgHom.restrictScalars_coe_linearMap {R : Type u_1} {A : Type u_6} {B : Type u_7} {ι : Type u_10} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [DecidableEq ι] [AddMonoid ι] {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [GradedAlgebra 𝒜] [GradedAlgebra ℬ] (R₀ : Type u_11) [CommSemiring R₀] [Algebra R₀ R] [Algebra R₀ A] [Algebra R₀ B] [IsScalarTower R₀ R A] [IsScalarTower R₀ R B] (f : 𝒜 →ₐᵍ[R] ℬ) : ↑R₀ ↑f = ↑(↑R₀ f)

theorem GradedAlgHom.restrictScalars_injective {R : Type u_1} {A : Type u_6} {B : Type u_7} {ι : Type u_10} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [DecidableEq ι] [AddMonoid ι] {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [GradedAlgebra 𝒜] [GradedAlgebra ℬ] (R₀ : Type u_11) [CommSemiring R₀] [Algebra R₀ R] [Algebra R₀ A] [Algebra R₀ B] [IsScalarTower R₀ R A] [IsScalarTower R₀ R B] : Function.Injective ↑R₀