algebra.hom.centroid - mathlib3 docs

source

structure centroid_hom (α : Type u_3) [non_unital_non_assoc_semiring α] :

Type u_3

to_fun : α → α
map_zero' : self.to_fun 0 = 0
map_add' : ∀ (x y : α), self.to_fun (x + y) = self.to_fun x + self.to_fun y
map_mul_left' : ∀ (a b : α), self.to_fun (a * b) = a * self.to_fun b
map_mul_right' : ∀ (a b : α), self.to_fun (a * b) = self.to_fun a * b

The type of centroid homomorphisms from α to α.

Instances for centroid_hom

source

@[nolint]

def centroid_hom.to_add_monoid_hom {α : Type u_3} [non_unital_non_assoc_semiring α] (self : centroid_hom α) :

α →+ α

source

@[instance]

def centroid_hom_class.to_add_monoid_hom_class (F : Type u_3) (α : out_param (Type u_4)) [non_unital_non_assoc_semiring α] [self : centroid_hom_class F α] :

add_monoid_hom_class F α α

source

@[class]

structure centroid_hom_class (F : Type u_3) (α : out_param (Type u_4)) [non_unital_non_assoc_semiring α] :

Type (max u_3 u_4)

coe : F → Π (a : α), (λ (_x : α), α) a
coe_injective' : function.injective centroid_hom_class.coe
map_add : ∀ (f : F) (x y : α), ⇑f (x + y) = ⇑f x + ⇑f y
map_zero : ∀ (f : F), ⇑f 0 = 0
map_mul_left : ∀ (f : F) (a b : α), ⇑f (a * b) = a * ⇑f b
map_mul_right : ∀ (f : F) (a b : α), ⇑f (a * b) = ⇑f a * b

centroid_hom_class F α states that F is a type of centroid homomorphisms.

You should extend this class when you extend centroid_hom.

Instances of this typeclass

centroid_hom.centroid_hom_class

Instances of other typeclasses for centroid_hom_class

centroid_hom_class.has_sizeof_inst

source

@[protected, instance]

def centroid_hom.has_coe_t {F : Type u_1} {α : Type u_2} [non_unital_non_assoc_semiring α] [centroid_hom_class F α] :

has_coe_t F (centroid_hom α)

Equations

centroid_hom.has_coe_t = {coe := λ (f : F), {to_fun := ⇑f, map_zero' := _, map_add' := _, map_mul_left' := _, map_mul_right' := _}}

source

@[protected, instance]

def centroid_hom.centroid_hom_class {α : Type u_2} [non_unital_non_assoc_semiring α] :

centroid_hom_class (centroid_hom α) α

Equations

centroid_hom.centroid_hom_class = {coe := λ (f : centroid_hom α), f.to_fun, coe_injective' := _, map_add := _, map_zero := _, map_mul_left := _, map_mul_right := _}

source

@[protected, instance]

def centroid_hom.has_coe_to_fun {α : Type u_2} [non_unital_non_assoc_semiring α] :

has_coe_to_fun (centroid_hom α) (λ (_x : centroid_hom α), α → α)

Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun directly.

Equations

centroid_hom.has_coe_to_fun = fun_like.has_coe_to_fun

source

@[simp]

theorem centroid_hom.to_fun_eq_coe {α : Type u_2} [non_unital_non_assoc_semiring α] {f : centroid_hom α} :

f.to_fun = ⇑f

source

@[ext]

theorem centroid_hom.ext {α : Type u_2} [non_unital_non_assoc_semiring α] {f g : centroid_hom α} (h : ∀ (a : α), ⇑f a = ⇑g a) :

f = g

source

@[simp, norm_cast]

theorem centroid_hom.coe_to_add_monoid_hom {α : Type u_2} [non_unital_non_assoc_semiring α] (f : centroid_hom α) :

⇑↑f = ⇑f

source

@[simp]

theorem centroid_hom.to_add_monoid_hom_eq_coe {α : Type u_2} [non_unital_non_assoc_semiring α] (f : centroid_hom α) :

f.to_add_monoid_hom = ↑f

source

theorem centroid_hom.coe_to_add_monoid_hom_injective {α : Type u_2} [non_unital_non_assoc_semiring α] :

function.injective coe

source

def centroid_hom.to_End {α : Type u_2} [non_unital_non_assoc_semiring α] (f : centroid_hom α) :

add_monoid.End α

Turn a centroid homomorphism into an additive monoid endomorphism.

Equations

f.to_End = ↑f

source

theorem centroid_hom.to_End_injective {α : Type u_2} [non_unital_non_assoc_semiring α] :

function.injective centroid_hom.to_End

source

@[protected]

def centroid_hom.copy {α : Type u_2} [non_unital_non_assoc_semiring α] (f : centroid_hom α) (f' : α → α) (h : f' = ⇑f) :

centroid_hom α

Copy of a centroid_hom with a new to_fun equal to the old one. Useful to fix definitional equalities.

Equations

f.copy f' h = {to_fun := f', map_zero' := _, map_add' := _, map_mul_left' := _, map_mul_right' := _}

source

@[simp]

theorem centroid_hom.coe_copy {α : Type u_2} [non_unital_non_assoc_semiring α] (f : centroid_hom α) (f' : α → α) (h : f' = ⇑f) :

⇑(f.copy f' h) = f'

source

theorem centroid_hom.copy_eq {α : Type u_2} [non_unital_non_assoc_semiring α] (f : centroid_hom α) (f' : α → α) (h : f' = ⇑f) :

f.copy f' h = f

source

@[protected]

def centroid_hom.id (α : Type u_2) [non_unital_non_assoc_semiring α] :

centroid_hom α

id as a centroid_hom.

Equations

centroid_hom.id α = {to_fun := (add_monoid_hom.id α).to_fun, map_zero' := _, map_add' := _, map_mul_left' := _, map_mul_right' := _}

source

@[protected, instance]

def centroid_hom.inhabited (α : Type u_2) [non_unital_non_assoc_semiring α] :

inhabited (centroid_hom α)

Equations

centroid_hom.inhabited α = {default := centroid_hom.id α _inst_1}

source

@[simp, norm_cast]

theorem centroid_hom.coe_id (α : Type u_2) [non_unital_non_assoc_semiring α] :

⇑(centroid_hom.id α) = id

source

@[simp, norm_cast]

theorem centroid_hom.coe_to_add_monoid_hom_id (α : Type u_2) [non_unital_non_assoc_semiring α] :

↑(centroid_hom.id α) = add_monoid_hom.id α

source

@[simp]

theorem centroid_hom.id_apply {α : Type u_2} [non_unital_non_assoc_semiring α] (a : α) :

⇑(centroid_hom.id α) a = a

source

def centroid_hom.comp {α : Type u_2} [non_unital_non_assoc_semiring α] (g f : centroid_hom α) :

centroid_hom α

Composition of centroid_homs as a centroid_hom.

Equations

g.comp f = {to_fun := (g.to_add_monoid_hom.comp f.to_add_monoid_hom).to_fun, map_zero' := _, map_add' := _, map_mul_left' := _, map_mul_right' := _}

source

@[simp, norm_cast]

theorem centroid_hom.coe_comp {α : Type u_2} [non_unital_non_assoc_semiring α] (g f : centroid_hom α) :

⇑(g.comp f) = ⇑g ∘ ⇑f

source

@[simp]

theorem centroid_hom.comp_apply {α : Type u_2} [non_unital_non_assoc_semiring α] (g f : centroid_hom α) (a : α) :

⇑(g.comp f) a = ⇑g (⇑f a)

source

@[simp, norm_cast]

theorem centroid_hom.coe_comp_add_monoid_hom {α : Type u_2} [non_unital_non_assoc_semiring α] (g f : centroid_hom α) :

↑(g.comp f) = ↑g.comp ↑f

source

@[simp]

theorem centroid_hom.comp_assoc {α : Type u_2} [non_unital_non_assoc_semiring α] (h g f : centroid_hom α) :

(h.comp g).comp f = h.comp (g.comp f)

source

@[simp]

theorem centroid_hom.comp_id {α : Type u_2} [non_unital_non_assoc_semiring α] (f : centroid_hom α) :

f.comp (centroid_hom.id α) = f

source

@[simp]

theorem centroid_hom.id_comp {α : Type u_2} [non_unital_non_assoc_semiring α] (f : centroid_hom α) :

(centroid_hom.id α).comp f = f

source

theorem centroid_hom.cancel_right {α : Type u_2} [non_unital_non_assoc_semiring α] {g₁ g₂ f : centroid_hom α} (hf : function.surjective ⇑f) :

g₁.comp f = g₂.comp f ↔ g₁ = g₂

source

theorem centroid_hom.cancel_left {α : Type u_2} [non_unital_non_assoc_semiring α] {g f₁ f₂ : centroid_hom α} (hg : function.injective ⇑g) :

g.comp f₁ = g.comp f₂ ↔ f₁ = f₂

source

@[protected, instance]

def centroid_hom.has_zero {α : Type u_2} [non_unital_non_assoc_semiring α] :

has_zero (centroid_hom α)

Equations

centroid_hom.has_zero = {zero := {to_fun := 0.to_fun, map_zero' := _, map_add' := _, map_mul_left' := _, map_mul_right' := _}}

source

@[protected, instance]

def centroid_hom.has_one {α : Type u_2} [non_unital_non_assoc_semiring α] :

has_one (centroid_hom α)

Equations

centroid_hom.has_one = {one := centroid_hom.id α _inst_1}

source

@[protected, instance]

def centroid_hom.has_add {α : Type u_2} [non_unital_non_assoc_semiring α] :

has_add (centroid_hom α)

Equations

centroid_hom.has_add = {add := λ (f g : centroid_hom α), {to_fun := (↑f + ↑g).to_fun, map_zero' := _, map_add' := _, map_mul_left' := _, map_mul_right' := _}}

source

@[protected, instance]

def centroid_hom.has_mul {α : Type u_2} [non_unital_non_assoc_semiring α] :

has_mul (centroid_hom α)

Equations

centroid_hom.has_mul = {mul := centroid_hom.comp _inst_1}

source

@[protected, instance]

def centroid_hom.has_nsmul {α : Type u_2} [non_unital_non_assoc_semiring α] :

has_smul ℕ (centroid_hom α)

Equations

centroid_hom.has_nsmul = {smul := λ (n : ℕ) (f : centroid_hom α), {to_fun := (n • ↑f).to_fun, map_zero' := _, map_add' := _, map_mul_left' := _, map_mul_right' := _}}

source

@[protected, instance]

def centroid_hom.has_npow_nat {α : Type u_2} [non_unital_non_assoc_semiring α] :

has_pow (centroid_hom α) ℕ

Equations

centroid_hom.has_npow_nat = {pow := λ (f : centroid_hom α) (n : ℕ), {to_fun := (f.to_End ^ n).to_fun, map_zero' := _, map_add' := _, map_mul_left' := _, map_mul_right' := _}}

source

@[simp, norm_cast]

theorem centroid_hom.coe_zero {α : Type u_2} [non_unital_non_assoc_semiring α] :

⇑0 = 0

source

@[simp, norm_cast]

theorem centroid_hom.coe_one {α : Type u_2} [non_unital_non_assoc_semiring α] :

⇑1 = id

source

@[simp, norm_cast]

theorem centroid_hom.coe_add {α : Type u_2} [non_unital_non_assoc_semiring α] (f g : centroid_hom α) :

⇑(f + g) = ⇑f + ⇑g

source

@[simp, norm_cast]

theorem centroid_hom.coe_mul {α : Type u_2} [non_unital_non_assoc_semiring α] (f g : centroid_hom α) :

⇑(f * g) = ⇑f ∘ ⇑g

source

@[simp, norm_cast, nolint]

theorem centroid_hom.coe_nsmul {α : Type u_2} [non_unital_non_assoc_semiring α] (f : centroid_hom α) (n : ℕ) :

⇑(n • f) = n • ⇑f

source

@[simp]

theorem centroid_hom.zero_apply {α : Type u_2} [non_unital_non_assoc_semiring α] (a : α) :

⇑0 a = 0

source

@[simp]

theorem centroid_hom.one_apply {α : Type u_2} [non_unital_non_assoc_semiring α] (a : α) :

⇑1 a = a

source

@[simp]

theorem centroid_hom.add_apply {α : Type u_2} [non_unital_non_assoc_semiring α] (f g : centroid_hom α) (a : α) :

⇑(f + g) a = ⇑f a + ⇑g a

source

@[simp]

theorem centroid_hom.mul_apply {α : Type u_2} [non_unital_non_assoc_semiring α] (f g : centroid_hom α) (a : α) :

⇑(f * g) a = ⇑f (⇑g a)

source

@[simp, nolint]

theorem centroid_hom.nsmul_apply {α : Type u_2} [non_unital_non_assoc_semiring α] (f : centroid_hom α) (n : ℕ) (a : α) :

⇑(n • f) a = n • ⇑f a

source

@[simp]

theorem centroid_hom.to_End_zero {α : Type u_2} [non_unital_non_assoc_semiring α] :

0.to_End = 0

source

@[simp]

theorem centroid_hom.to_End_add {α : Type u_2} [non_unital_non_assoc_semiring α] (x y : centroid_hom α) :

(x + y).to_End = x.to_End + y.to_End

source

theorem centroid_hom.to_End_nsmul {α : Type u_2} [non_unital_non_assoc_semiring α] (x : centroid_hom α) (n : ℕ) :

(n • x).to_End = n • x.to_End

source

@[protected, instance]

def centroid_hom.add_comm_monoid {α : Type u_2} [non_unital_non_assoc_semiring α] :

add_comm_monoid (centroid_hom α)

Equations

centroid_hom.add_comm_monoid = function.injective.add_comm_monoid coe centroid_hom.coe_to_add_monoid_hom_injective centroid_hom.to_End_zero centroid_hom.to_End_add centroid_hom.to_End_nsmul

source

@[protected, instance]

def centroid_hom.has_nat_cast {α : Type u_2} [non_unital_non_assoc_semiring α] :

has_nat_cast (centroid_hom α)

Equations

centroid_hom.has_nat_cast = {nat_cast := λ (n : ℕ), n • 1}

source

@[simp, norm_cast]

theorem centroid_hom.coe_nat_cast {α : Type u_2} [non_unital_non_assoc_semiring α] (n : ℕ) :

⇑↑n = n • id

source

theorem centroid_hom.nat_cast_apply {α : Type u_2} [non_unital_non_assoc_semiring α] (n : ℕ) (m : α) :

⇑↑n m = n • m

source

@[simp]

theorem centroid_hom.to_End_one {α : Type u_2} [non_unital_non_assoc_semiring α] :

1.to_End = 1

source

@[simp]

theorem centroid_hom.to_End_mul {α : Type u_2} [non_unital_non_assoc_semiring α] (x y : centroid_hom α) :

(x * y).to_End = x.to_End * y.to_End

source

@[simp]

theorem centroid_hom.to_End_pow {α : Type u_2} [non_unital_non_assoc_semiring α] (x : centroid_hom α) (n : ℕ) :

(x ^ n).to_End = x.to_End ^ n

source

@[simp, norm_cast]

theorem centroid_hom.to_End_nat_cast {α : Type u_2} [non_unital_non_assoc_semiring α] (n : ℕ) :

↑n.to_End = ↑n

source

@[protected, instance]

def centroid_hom.semiring {α : Type u_2} [non_unital_non_assoc_semiring α] :

semiring (centroid_hom α)

Equations

centroid_hom.semiring = function.injective.semiring centroid_hom.to_End centroid_hom.to_End_injective centroid_hom.to_End_zero centroid_hom.to_End_one centroid_hom.to_End_add centroid_hom.to_End_mul centroid_hom.to_End_nsmul centroid_hom.to_End_pow centroid_hom.to_End_nat_cast

source

theorem centroid_hom.comp_mul_comm {α : Type u_2} [non_unital_non_assoc_semiring α] (T S : centroid_hom α) (a b : α) :

(⇑T ∘ ⇑S) (a * b) = (⇑S ∘ ⇑T) (a * b)

source

@[protected, instance]

def centroid_hom.has_neg {α : Type u_2} [non_unital_non_assoc_ring α] :

has_neg (centroid_hom α)

Negation of centroid_homs as a centroid_hom.

Equations

centroid_hom.has_neg = {neg := λ (f : centroid_hom α), {to_fun := (-↑f).to_fun, map_zero' := _, map_add' := _, map_mul_left' := _, map_mul_right' := _}}

source

@[protected, instance]

def centroid_hom.has_sub {α : Type u_2} [non_unital_non_assoc_ring α] :

has_sub (centroid_hom α)

Equations

centroid_hom.has_sub = {sub := λ (f g : centroid_hom α), {to_fun := (↑f - ↑g).to_fun, map_zero' := _, map_add' := _, map_mul_left' := _, map_mul_right' := _}}

source

@[protected, instance]

def centroid_hom.has_zsmul {α : Type u_2} [non_unital_non_assoc_ring α] :

has_smul ℤ (centroid_hom α)

Equations

centroid_hom.has_zsmul = {smul := λ (n : ℤ) (f : centroid_hom α), {to_fun := (n • ↑f).to_fun, map_zero' := _, map_add' := _, map_mul_left' := _, map_mul_right' := _}}

source

@[protected, instance]

def centroid_hom.has_int_cast {α : Type u_2} [non_unital_non_assoc_ring α] :

has_int_cast (centroid_hom α)

Equations

centroid_hom.has_int_cast = {int_cast := λ (z : ℤ), z • 1}

source

@[simp, norm_cast]

theorem centroid_hom.coe_int_cast {α : Type u_2} [non_unital_non_assoc_ring α] (z : ℤ) :

⇑↑z = z • id

source

theorem centroid_hom.int_cast_apply {α : Type u_2} [non_unital_non_assoc_ring α] (z : ℤ) (m : α) :

⇑↑z m = z • m

source

@[simp]

theorem centroid_hom.to_End_neg {α : Type u_2} [non_unital_non_assoc_ring α] (x : centroid_hom α) :

(-x).to_End = -x.to_End

source

@[simp]

theorem centroid_hom.to_End_sub {α : Type u_2} [non_unital_non_assoc_ring α] (x y : centroid_hom α) :

(x - y).to_End = x.to_End - y.to_End

source

theorem centroid_hom.to_End_zsmul {α : Type u_2} [non_unital_non_assoc_ring α] (x : centroid_hom α) (n : ℤ) :

(n • x).to_End = n • x.to_End

source

@[protected, instance]

def centroid_hom.add_comm_group {α : Type u_2} [non_unital_non_assoc_ring α] :

add_comm_group (centroid_hom α)

Equations

centroid_hom.add_comm_group = function.injective.add_comm_group centroid_hom.to_End centroid_hom.add_comm_group._proof_1 centroid_hom.add_comm_group._proof_2 centroid_hom.add_comm_group._proof_3 centroid_hom.to_End_neg centroid_hom.to_End_sub centroid_hom.add_comm_group._proof_4 centroid_hom.to_End_zsmul

source

@[simp, norm_cast]

theorem centroid_hom.coe_neg {α : Type u_2} [non_unital_non_assoc_ring α] (f : centroid_hom α) :

⇑-f = -⇑f

source

@[simp, norm_cast]

theorem centroid_hom.coe_sub {α : Type u_2} [non_unital_non_assoc_ring α] (f g : centroid_hom α) :

⇑(f - g) = ⇑f - ⇑g

source

@[simp]

theorem centroid_hom.neg_apply {α : Type u_2} [non_unital_non_assoc_ring α] (f : centroid_hom α) (a : α) :

(⇑-f) a = -⇑f a

source

@[simp]

theorem centroid_hom.sub_apply {α : Type u_2} [non_unital_non_assoc_ring α] (f g : centroid_hom α) (a : α) :

⇑(f - g) a = ⇑f a - ⇑g a

source

@[simp, norm_cast]

theorem centroid_hom.to_End_int_cast {α : Type u_2} [non_unital_non_assoc_ring α] (z : ℤ) :

↑z.to_End = ↑z

source

@[protected, instance]

def centroid_hom.ring {α : Type u_2} [non_unital_non_assoc_ring α] :

ring (centroid_hom α)

Equations

centroid_hom.ring = function.injective.ring centroid_hom.to_End centroid_hom.ring._proof_1 centroid_hom.ring._proof_2 centroid_hom.ring._proof_3 centroid_hom.ring._proof_4 centroid_hom.ring._proof_5 centroid_hom.to_End_neg centroid_hom.to_End_sub centroid_hom.ring._proof_6 centroid_hom.to_End_zsmul centroid_hom.ring._proof_7 centroid_hom.ring._proof_8 centroid_hom.to_End_int_cast

source

@[reducible]

def centroid_hom.comm_ring {α : Type u_2} [non_unital_ring α] (h : ∀ (a b : α), (∀ (r : α), a * r * b = 0) → a = 0 ∨ b = 0) :

comm_ring (centroid_hom α)

A prime associative ring has commutative centroid.

Equations

centroid_hom.comm_ring h = {add := ring.add centroid_hom.ring, add_assoc := _, zero := ring.zero centroid_hom.ring, zero_add := _, add_zero := _, nsmul := ring.nsmul centroid_hom.ring, nsmul_zero' := _, nsmul_succ' := _, neg := ring.neg centroid_hom.ring, sub := ring.sub centroid_hom.ring, sub_eq_add_neg := _, zsmul := ring.zsmul centroid_hom.ring, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := ring.int_cast centroid_hom.ring, nat_cast := ring.nat_cast centroid_hom.ring, one := ring.one centroid_hom.ring, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := ring.mul centroid_hom.ring, mul_assoc := _, one_mul := _, mul_one := _, npow := ring.npow centroid_hom.ring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _}

mathlib3 documentation

Centroid homomorphisms #

Types of morphisms #

Typeclasses #

References #

Tags #

Centroid homomorphisms #