Project.Grading.GradedRingHom

source

structure GradedRingHom {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_4} {τ : Type u_5} [CommSemiring A] [SetLike σ A] (𝒜 : ι → σ) [CommSemiring B] [SetLike τ B] (ℬ : ι → τ) extends A →+* B :

Type (max u_2 u_3)

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
map_mem' {i : ι} {x : A} : x ∈ 𝒜 i → (↑↑self.toRingHom).toFun x ∈ ℬ i

Instances For

source

def Graded.«term_→+*_» :

Lean.TrailingParserDescr

Equations

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

Instances For

source

instance GradedRingHom.instFunLike {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_4} {τ : Type u_5} [CommSemiring A] [SetLike σ A] (𝒜 : ι → σ) [CommSemiring B] [SetLike τ B] (ℬ : ι → τ) :

FunLike (GradedRingHom 𝒜 ℬ) A B

Equations

GradedRingHom.instFunLike 𝒜 ℬ = { coe := fun (f : GradedRingHom 𝒜 ℬ) => (↑↑f.toRingHom).toFun, coe_injective' := ⋯ }

source

instance GradedRingHom.instRingHomClass {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_4} {τ : Type u_5} [CommSemiring A] [SetLike σ A] (𝒜 : ι → σ) [CommSemiring B] [SetLike τ B] (ℬ : ι → τ) :

RingHomClass (GradedRingHom 𝒜 ℬ) A B

source

theorem GradedRingHom.map_mem {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_4} {τ : Type u_5} [CommSemiring A] [SetLike σ A] {𝒜 : ι → σ} [CommSemiring B] [SetLike τ B] {ℬ : ι → τ} (f : GradedRingHom 𝒜 ℬ) {i : ι} {x : A} (hx : x ∈ 𝒜 i) :

f x ∈ ℬ i

source

theorem GradedRingHom.map_homogeneous {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_4} {τ : Type u_5} [CommSemiring A] [SetLike σ A] {𝒜 : ι → σ} [CommSemiring B] [SetLike τ B] {ℬ : ι → τ} (f : GradedRingHom 𝒜 ℬ) {a : A} (hom_a : SetLike.Homogeneous 𝒜 a) :

SetLike.Homogeneous ℬ (f a)

source

def GradedRingHom.asDirectSum {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_4} {τ : Type u_5} [AddCommMonoid ι] [DecidableEq ι] [CommSemiring A] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [GradedRing 𝒜] [CommSemiring B] [SetLike τ B] [AddSubmonoidClass τ B] {ℬ : ι → τ} [GradedRing ℬ] (f : GradedRingHom 𝒜 ℬ) :

(DirectSum ι fun (i : ι) => ↥(𝒜 i)) →+* DirectSum ι fun (i : ι) => ↥(ℬ i)

Equations

f.asDirectSum = DirectSum.toSemiring (fun (i : ι) => { toFun := fun (x : ↥(𝒜 i)) => (DirectSum.of (fun (i : ι) => ↥(ℬ i)) i) ⟨f ↑x, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }) ⋯ ⋯

Instances For

source

@[simp]

theorem GradedRingHom.asDirectSum_apply_of {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_4} {τ : Type u_5} [AddCommMonoid ι] [DecidableEq ι] [CommSemiring A] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [GradedRing 𝒜] [CommSemiring B] [SetLike τ B] [AddSubmonoidClass τ B] {ℬ : ι → τ} [GradedRing ℬ] (f : GradedRingHom 𝒜 ℬ) {i : ι} (x : ↥(𝒜 i)) :

f.asDirectSum ((DirectSum.of (fun (i : ι) => ↥(𝒜 i)) i) x) = (DirectSum.of (fun (i : ι) => ↥(ℬ i)) i) ⟨f ↑x, ⋯⟩

source

theorem GradedRingHom.commutes {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_4} {τ : Type u_5} [AddCommMonoid ι] [DecidableEq ι] [CommSemiring A] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [GradedRing 𝒜] [CommSemiring B] [SetLike τ B] [AddSubmonoidClass τ B] {ℬ : ι → τ} [GradedRing ℬ] (f : GradedRingHom 𝒜 ℬ) :

⇑(DirectSum.decompose ℬ) ∘ ⇑f = ⇑f.asDirectSum ∘ ⇑(DirectSum.decompose 𝒜)

source

theorem GradedRingHom.commutes_apply {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_4} {τ : Type u_5} [AddCommMonoid ι] [DecidableEq ι] [CommSemiring A] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [GradedRing 𝒜] [CommSemiring B] [SetLike τ B] [AddSubmonoidClass τ B] {ℬ : ι → τ} [GradedRing ℬ] (f : GradedRingHom 𝒜 ℬ) (x : A) :

(DirectSum.decompose ℬ) (f x) = f.asDirectSum ((DirectSum.decompose 𝒜) x)

source

@[simp]

theorem GradedRingHom.decompose_apply_decompose {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_4} {τ : Type u_5} [AddCommMonoid ι] [DecidableEq ι] [CommSemiring A] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [GradedRing 𝒜] [CommSemiring B] [SetLike τ B] [AddSubmonoidClass τ B] {ℬ : ι → τ} [GradedRing ℬ] (f : GradedRingHom 𝒜 ℬ) (x : A) (i : ι) :

(DirectSum.decompose ℬ) (f ↑(((DirectSum.decompose 𝒜) x) i)) = (DirectSum.of (fun (i : ι) => ↥(ℬ i)) i) ⟨f ↑(((DirectSum.decompose 𝒜) x) i), ⋯⟩

source

theorem GradedRingHom.homogeneous_of_apply_homogeneous {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_4} {τ : Type u_5} [AddCommMonoid ι] [DecidableEq ι] [CommSemiring A] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [GradedRing 𝒜] [CommSemiring B] [SetLike τ B] [AddSubmonoidClass τ B] {ℬ : ι → τ} [GradedRing ℬ] (f : GradedRingHom 𝒜 ℬ) {i : ι} {a : A} (hom : f a ∈ ℬ i) :

∃ a' ∈ 𝒜 i, f a' = f a

source

structure GradedRingEquiv {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_4} {τ : Type u_5} [CommSemiring A] [SetLike σ A] (𝒜 : ι → σ) [CommSemiring B] [SetLike τ B] (ℬ : ι → τ) extends A ≃+* B :

Type (max u_2 u_3)

toFun : A → B
invFun : B → A
left_inv : Function.LeftInverse self.invFun self.toFun
right_inv : Function.RightInverse self.invFun self.toFun
map_mul' (x y : A) : self.toFun (x * y) = self.toFun x * self.toFun y
map_add' (x y : A) : self.toFun (x + y) = self.toFun x + self.toFun y
map_mem' {i : ι} {x : A} : x ∈ 𝒜 i → self.toFun x ∈ ℬ i
inv_mem' {i : ι} {y : B} : y ∈ ℬ i → self.invFun y ∈ 𝒜 i

Instances For

source

def Graded.«term_≃+*_» :

Lean.TrailingParserDescr

Equations

Graded.«term_≃+*_» = Lean.ParserDescr.trailingNode `Graded.«term_≃+*_» 25 26 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "≃+*") (Lean.ParserDescr.cat `term 26))

Instances For

source

instance GradedRingEquiv.instEquivLike {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_4} {τ : Type u_5} [CommSemiring A] [SetLike σ A] (𝒜 : ι → σ) [CommSemiring B] [SetLike τ B] (ℬ : ι → τ) :

EquivLike (GradedRingEquiv 𝒜 ℬ) A B

Equations

GradedRingEquiv.instEquivLike 𝒜 ℬ = { coe := fun (f : GradedRingEquiv 𝒜 ℬ) => f.toFun, inv := fun (f : GradedRingEquiv 𝒜 ℬ) => f.invFun, left_inv := ⋯, right_inv := ⋯, coe_injective' := ⋯ }

source

theorem GradedRingEquiv.map_mem {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_4} {τ : Type u_5} [CommSemiring A] [SetLike σ A] {𝒜 : ι → σ} [CommSemiring B] [SetLike τ B] {ℬ : ι → τ} (f : GradedRingEquiv 𝒜 ℬ) {i : ι} {x : A} (hx : x ∈ 𝒜 i) :

f x ∈ ℬ i

source

theorem GradedRingEquiv.inv_mem {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_4} {τ : Type u_5} [CommSemiring A] [SetLike σ A] {𝒜 : ι → σ} [CommSemiring B] [SetLike τ B] {ℬ : ι → τ} (f : GradedRingEquiv 𝒜 ℬ) {i : ι} {y : B} (hy : y ∈ ℬ i) :

f.invFun y ∈ 𝒜 i

source

def GradedRingEquiv.toGradedRingHom {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_4} {τ : Type u_5} [CommSemiring A] [SetLike σ A] (𝒜 : ι → σ) [CommSemiring B] [SetLike τ B] (ℬ : ι → τ) (f : GradedRingEquiv 𝒜 ℬ) :

GradedRingHom 𝒜 ℬ

Equations

GradedRingEquiv.toGradedRingHom 𝒜 ℬ f = { toFun := ⇑f, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mem' := ⋯ }

Instances For

source

@[simp]

theorem GradedRingEquiv.toGradedRingHom_toFun {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_4} {τ : Type u_5} [CommSemiring A] [SetLike σ A] (𝒜 : ι → σ) [CommSemiring B] [SetLike τ B] (ℬ : ι → τ) (f : GradedRingEquiv 𝒜 ℬ) (a : A) :

(GradedRingEquiv.toGradedRingHom 𝒜 ℬ f) a = f a

source

def GradedRingEquiv.refl {ι : Type u_1} {A : Type u_2} {σ : Type u_4} [CommSemiring A] [SetLike σ A] (𝒜 : ι → σ) :

GradedRingEquiv 𝒜 𝒜

Equations

GradedRingEquiv.refl 𝒜 = { toRingEquiv := RingEquiv.refl A, map_mem' := ⋯, inv_mem' := ⋯ }

Instances For

source

theorem GradedRingEquiv.refl_toRingEquiv {ι : Type u_1} {A : Type u_2} {σ : Type u_4} [CommSemiring A] [SetLike σ A] (𝒜 : ι → σ) :

(GradedRingEquiv.refl 𝒜).toRingEquiv = RingEquiv.refl A