algebra.group_action_hom

source

@[nolint]

structure mul_action_hom (M' : Type u_1) (X : Type u_2) [has_scalar M' X] (Y : Type u_3) [has_scalar M' Y] :

Type (max u_2 u_3)

to_fun : X → Y
map_smul' : ∀ (m : M') (x : X), self.to_fun (m • x) = m • self.to_fun x

Equivariant functions.

source

@[protected, instance]

def mul_action_hom.has_coe_to_fun (M' : Type u_1) (X : Type u_2) [has_scalar M' X] (Y : Type u_3) [has_scalar M' Y] :

has_coe_to_fun (X →[M'] Y) (λ (_x : X →[M'] Y), X → Y)

Equations

mul_action_hom.has_coe_to_fun M' X Y = {coe := mul_action_hom.to_fun _inst_2}

source

@[simp]

theorem mul_action_hom.map_smul {M' : Type u_1} {X : Type u_2} [has_scalar M' X] {Y : Type u_3} [has_scalar M' Y] (f : X →[M'] Y) (m : M') (x : X) :

⇑f (m • x) = m • ⇑f x

source

@[ext]

theorem mul_action_hom.ext {M' : Type u_1} {X : Type u_2} [has_scalar M' X] {Y : Type u_3} [has_scalar M' Y] {f g : X →[M'] Y} :

(∀ (x : X), ⇑f x = ⇑g x) → f = g

source

theorem mul_action_hom.ext_iff {M' : Type u_1} {X : Type u_2} [has_scalar M' X] {Y : Type u_3} [has_scalar M' Y] {f g : X →[M'] Y} :

f = g ↔ ∀ (x : X), ⇑f x = ⇑g x

source

@[protected]

theorem mul_action_hom.congr_fun {M' : Type u_1} {X : Type u_2} [has_scalar M' X] {Y : Type u_3} [has_scalar M' Y] {f g : X →[M'] Y} (h : f = g) (x : X) :

⇑f x = ⇑g x

source

@[protected]

def mul_action_hom.id (M' : Type u_1) {X : Type u_2} [has_scalar M' X] :

X →[M'] X

The identity map as an equivariant map.

Equations

mul_action_hom.id M' = {to_fun := id X, map_smul' := _}

source

@[simp]

theorem mul_action_hom.id_apply (M' : Type u_1) {X : Type u_2} [has_scalar M' X] (x : X) :

⇑(mul_action_hom.id M') x = x

source

def mul_action_hom.comp {M' : Type u_1} {X : Type u_2} [has_scalar M' X] {Y : Type u_3} [has_scalar M' Y] {Z : Type u_4} [has_scalar M' Z] (g : Y →[M'] Z) (f : X →[M'] Y) :

X →[M'] Z

Composition of two equivariant maps.

Equations

g.comp f = {to_fun := ⇑g ∘ ⇑f, map_smul' := _}

source

@[simp]

theorem mul_action_hom.comp_apply {M' : Type u_1} {X : Type u_2} [has_scalar M' X] {Y : Type u_3} [has_scalar M' Y] {Z : Type u_4} [has_scalar M' Z] (g : Y →[M'] Z) (f : X →[M'] Y) (x : X) :

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

source

@[simp]

theorem mul_action_hom.id_comp {M' : Type u_1} {X : Type u_2} [has_scalar M' X] {Y : Type u_3} [has_scalar M' Y] (f : X →[M'] Y) :

(mul_action_hom.id M').comp f = f

source

@[simp]

theorem mul_action_hom.comp_id {M' : Type u_1} {X : Type u_2} [has_scalar M' X] {Y : Type u_3} [has_scalar M' Y] (f : X →[M'] Y) :

f.comp (mul_action_hom.id M') = f

source

def mul_action_hom.inverse {M : Type u_5} [monoid M] {A : Type u_6} [add_monoid A] [distrib_mul_action M A] {B : Type u_8} [add_monoid B] [distrib_mul_action M B] (f : A →[M] B) (g : B → A) (h₁ : function.left_inverse g ⇑f) (h₂ : function.right_inverse g ⇑f) :

B →[M] A

The inverse of a bijective equivariant map is equivariant.

Equations

f.inverse g h₁ h₂ = {to_fun := g, map_smul' := _}

source

@[simp]

theorem mul_action_hom.inverse_to_fun {M : Type u_5} [monoid M] {A : Type u_6} [add_monoid A] [distrib_mul_action M A] {B : Type u_8} [add_monoid B] [distrib_mul_action M B] (f : A →[M] B) (g : B → A) (h₁ : function.left_inverse g ⇑f) (h₂ : function.right_inverse g ⇑f) (ᾰ : B) :

⇑(f.inverse g h₁ h₂) ᾰ = g ᾰ

source

def mul_action_hom.to_quotient {G : Type u_16} [group G] (H : subgroup G) :

G →[G] G ⧸ H

The canonical map to the left cosets.

Equations

mul_action_hom.to_quotient H = {to_fun := coe coe_to_lift, map_smul' := _}

source

@[simp]

theorem mul_action_hom.to_quotient_apply {G : Type u_16} [group G] (H : subgroup G) (g : G) :

⇑(mul_action_hom.to_quotient H) g = ↑g

source

def distrib_mul_action_hom.to_mul_action_hom {M : Type u_5} [monoid M] {A : Type u_6} [add_monoid A] [distrib_mul_action M A] {B : Type u_8} [add_monoid B] [distrib_mul_action M B] (self : A →+[M] B) :

A →[M] B

Reinterpret an equivariant additive monoid homomorphism as an equivariant function.

source

def distrib_mul_action_hom.to_add_monoid_hom {M : Type u_5} [monoid M] {A : Type u_6} [add_monoid A] [distrib_mul_action M A] {B : Type u_8} [add_monoid B] [distrib_mul_action M B] (self : A →+[M] B) :

A →+ B

Reinterpret an equivariant additive monoid homomorphism as an additive monoid homomorphism.

source

structure distrib_mul_action_hom (M : Type u_5) [monoid M] (A : Type u_6) [add_monoid A] [distrib_mul_action M A] (B : Type u_8) [add_monoid B] [distrib_mul_action M B] :

Type (max u_6 u_8)

to_fun : A → B
map_smul' : ∀ (m : M) (x : A), self.to_fun (m • x) = m • self.to_fun x
map_zero' : self.to_fun 0 = 0
map_add' : ∀ (x y : A), self.to_fun (x + y) = self.to_fun x + self.to_fun y

Equivariant additive monoid homomorphisms.

source

@[protected, instance]

def distrib_mul_action_hom.has_coe (M : Type u_5) [monoid M] (A : Type u_6) [add_monoid A] [distrib_mul_action M A] (B : Type u_8) [add_monoid B] [distrib_mul_action M B] :

has_coe (A →+[M] B) (A →+ B)

Equations

distrib_mul_action_hom.has_coe M A B = {coe := distrib_mul_action_hom.to_add_monoid_hom _inst_10}

source

@[protected, instance]

def distrib_mul_action_hom.has_coe' (M : Type u_5) [monoid M] (A : Type u_6) [add_monoid A] [distrib_mul_action M A] (B : Type u_8) [add_monoid B] [distrib_mul_action M B] :

has_coe (A →+[M] B) (A →[M] B)

Equations

distrib_mul_action_hom.has_coe' M A B = {coe := distrib_mul_action_hom.to_mul_action_hom _inst_10}

source

@[protected, instance]

def distrib_mul_action_hom.has_coe_to_fun (M : Type u_5) [monoid M] (A : Type u_6) [add_monoid A] [distrib_mul_action M A] (B : Type u_8) [add_monoid B] [distrib_mul_action M B] :

has_coe_to_fun (A →+[M] B) (λ (_x : A →+[M] B), A → B)

Equations

distrib_mul_action_hom.has_coe_to_fun M A B = {coe := distrib_mul_action_hom.to_fun _inst_10}

source

@[simp]

theorem distrib_mul_action_hom.to_fun_eq_coe {M : Type u_5} [monoid M] {A : Type u_6} [add_monoid A] [distrib_mul_action M A] {B : Type u_8} [add_monoid B] [distrib_mul_action M B] (f : A →+[M] B) :

f.to_fun = ⇑f

source

@[norm_cast]

theorem distrib_mul_action_hom.coe_fn_coe {M : Type u_5} [monoid M] {A : Type u_6} [add_monoid A] [distrib_mul_action M A] {B : Type u_8} [add_monoid B] [distrib_mul_action M B] (f : A →+[M] B) :

⇑↑f = ⇑f

source

@[norm_cast]

theorem distrib_mul_action_hom.coe_fn_coe' {M : Type u_5} [monoid M] {A : Type u_6} [add_monoid A] [distrib_mul_action M A] {B : Type u_8} [add_monoid B] [distrib_mul_action M B] (f : A →+[M] B) :

⇑↑f = ⇑f

source

@[ext]

theorem distrib_mul_action_hom.ext {M : Type u_5} [monoid M] {A : Type u_6} [add_monoid A] [distrib_mul_action M A] {B : Type u_8} [add_monoid B] [distrib_mul_action M B] {f g : A →+[M] B} :

(∀ (x : A), ⇑f x = ⇑g x) → f = g

source

theorem distrib_mul_action_hom.ext_iff {M : Type u_5} [monoid M] {A : Type u_6} [add_monoid A] [distrib_mul_action M A] {B : Type u_8} [add_monoid B] [distrib_mul_action M B] {f g : A →+[M] B} :

f = g ↔ ∀ (x : A), ⇑f x = ⇑g x

source

@[protected]

theorem distrib_mul_action_hom.congr_fun {M : Type u_5} [monoid M] {A : Type u_6} [add_monoid A] [distrib_mul_action M A] {B : Type u_8} [add_monoid B] [distrib_mul_action M B] {f g : A →+[M] B} (h : f = g) (x : A) :

⇑f x = ⇑g x

source

theorem distrib_mul_action_hom.to_mul_action_hom_injective {M : Type u_5} [monoid M] {A : Type u_6} [add_monoid A] [distrib_mul_action M A] {B : Type u_8} [add_monoid B] [distrib_mul_action M B] {f g : A →+[M] B} (h : ↑f = ↑g) :

f = g

source

theorem distrib_mul_action_hom.to_add_monoid_hom_injective {M : Type u_5} [monoid M] {A : Type u_6} [add_monoid A] [distrib_mul_action M A] {B : Type u_8} [add_monoid B] [distrib_mul_action M B] {f g : A →+[M] B} (h : ↑f = ↑g) :

f = g

source

@[simp]

theorem distrib_mul_action_hom.map_zero {M : Type u_5} [monoid M] {A : Type u_6} [add_monoid A] [distrib_mul_action M A] {B : Type u_8} [add_monoid B] [distrib_mul_action M B] (f : A →+[M] B) :

⇑f 0 = 0

source

@[simp]

theorem distrib_mul_action_hom.map_add {M : Type u_5} [monoid M] {A : Type u_6} [add_monoid A] [distrib_mul_action M A] {B : Type u_8} [add_monoid B] [distrib_mul_action M B] (f : A →+[M] B) (x y : A) :

⇑f (x + y) = ⇑f x + ⇑f y

source

@[simp]

theorem distrib_mul_action_hom.map_neg {M : Type u_5} [monoid M] (A' : Type u_7) [add_group A'] [distrib_mul_action M A'] (B' : Type u_9) [add_group B'] [distrib_mul_action M B'] (f : A' →+[M] B') (x : A') :

⇑f (-x) = -⇑f x

source

@[simp]

theorem distrib_mul_action_hom.map_sub {M : Type u_5} [monoid M] (A' : Type u_7) [add_group A'] [distrib_mul_action M A'] (B' : Type u_9) [add_group B'] [distrib_mul_action M B'] (f : A' →+[M] B') (x y : A') :

⇑f (x - y) = ⇑f x - ⇑f y

source

@[simp]

theorem distrib_mul_action_hom.map_smul {M : Type u_5} [monoid M] {A : Type u_6} [add_monoid A] [distrib_mul_action M A] {B : Type u_8} [add_monoid B] [distrib_mul_action M B] (f : A →+[M] B) (m : M) (x : A) :

⇑f (m • x) = m • ⇑f x

source

@[protected]

def distrib_mul_action_hom.id (M : Type u_5) [monoid M] {A : Type u_6} [add_monoid A] [distrib_mul_action M A] :

A →+[M] A

The identity map as an equivariant additive monoid homomorphism.

Equations

distrib_mul_action_hom.id M = {to_fun := id A, map_smul' := _, map_zero' := _, map_add' := _}

source

@[simp]

theorem distrib_mul_action_hom.id_apply (M : Type u_5) [monoid M] {A : Type u_6} [add_monoid A] [distrib_mul_action M A] (x : A) :

⇑(distrib_mul_action_hom.id M) x = x

source

@[protected, instance]

def distrib_mul_action_hom.has_zero {M : Type u_5} [monoid M] {A : Type u_6} [add_monoid A] [distrib_mul_action M A] {B : Type u_8} [add_monoid B] [distrib_mul_action M B] :

has_zero (A →+[M] B)

Equations

distrib_mul_action_hom.has_zero = {zero := {to_fun := 0.to_fun, map_smul' := _, map_zero' := _, map_add' := _}}

source

@[protected, instance]

def distrib_mul_action_hom.has_one {M : Type u_5} [monoid M] {A : Type u_6} [add_monoid A] [distrib_mul_action M A] :

has_one (A →+[M] A)

Equations

distrib_mul_action_hom.has_one = {one := distrib_mul_action_hom.id M _inst_6}

source

@[simp]

theorem distrib_mul_action_hom.coe_zero {M : Type u_5} [monoid M] {A : Type u_6} [add_monoid A] [distrib_mul_action M A] {B : Type u_8} [add_monoid B] [distrib_mul_action M B] :

⇑0 = 0

source

@[simp]

theorem distrib_mul_action_hom.coe_one {M : Type u_5} [monoid M] {A : Type u_6} [add_monoid A] [distrib_mul_action M A] :

⇑1 = id

source

theorem distrib_mul_action_hom.zero_apply {M : Type u_5} [monoid M] {A : Type u_6} [add_monoid A] [distrib_mul_action M A] {B : Type u_8} [add_monoid B] [distrib_mul_action M B] (a : A) :

⇑0 a = 0

source

theorem distrib_mul_action_hom.one_apply {M : Type u_5} [monoid M] {A : Type u_6} [add_monoid A] [distrib_mul_action M A] (a : A) :

⇑1 a = a

source

@[protected, instance]

def distrib_mul_action_hom.inhabited {M : Type u_5} [monoid M] {A : Type u_6} [add_monoid A] [distrib_mul_action M A] {B : Type u_8} [add_monoid B] [distrib_mul_action M B] :

inhabited (A →+[M] B)

Equations

distrib_mul_action_hom.inhabited = {default := 0}

source

def distrib_mul_action_hom.comp {M : Type u_5} [monoid M] {A : Type u_6} [add_monoid A] [distrib_mul_action M A] {B : Type u_8} [add_monoid B] [distrib_mul_action M B] {C : Type u_10} [add_monoid C] [distrib_mul_action M C] (g : B →+[M] C) (f : A →+[M] B) :

A →+[M] C

Composition of two equivariant additive monoid homomorphisms.

Equations

g.comp f = {to_fun := (↑g.comp ↑f).to_fun, map_smul' := _, map_zero' := _, map_add' := _}

source

@[simp]

theorem distrib_mul_action_hom.comp_apply {M : Type u_5} [monoid M] {A : Type u_6} [add_monoid A] [distrib_mul_action M A] {B : Type u_8} [add_monoid B] [distrib_mul_action M B] {C : Type u_10} [add_monoid C] [distrib_mul_action M C] (g : B →+[M] C) (f : A →+[M] B) (x : A) :

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

source

@[simp]

theorem distrib_mul_action_hom.id_comp {M : Type u_5} [monoid M] {A : Type u_6} [add_monoid A] [distrib_mul_action M A] {B : Type u_8} [add_monoid B] [distrib_mul_action M B] (f : A →+[M] B) :

(distrib_mul_action_hom.id M).comp f = f

source

@[simp]

theorem distrib_mul_action_hom.comp_id {M : Type u_5} [monoid M] {A : Type u_6} [add_monoid A] [distrib_mul_action M A] {B : Type u_8} [add_monoid B] [distrib_mul_action M B] (f : A →+[M] B) :

f.comp (distrib_mul_action_hom.id M) = f

source

def distrib_mul_action_hom.inverse {M : Type u_5} [monoid M] {A : Type u_6} [add_monoid A] [distrib_mul_action M A] {B : Type u_8} [add_monoid B] [distrib_mul_action M B] (f : A →+[M] B) (g : B → A) (h₁ : function.left_inverse g ⇑f) (h₂ : function.right_inverse g ⇑f) :

B →+[M] A

The inverse of a bijective distrib_mul_action_hom is a distrib_mul_action_hom.

Equations

f.inverse g h₁ h₂ = {to_fun := g, map_smul' := _, map_zero' := _, map_add' := _}

source

@[simp]

theorem distrib_mul_action_hom.inverse_to_fun {M : Type u_5} [monoid M] {A : Type u_6} [add_monoid A] [distrib_mul_action M A] {B : Type u_8} [add_monoid B] [distrib_mul_action M B] (f : A →+[M] B) (g : B → A) (h₁ : function.left_inverse g ⇑f) (h₂ : function.right_inverse g ⇑f) (ᾰ : B) :

⇑(f.inverse g h₁ h₂) ᾰ = g ᾰ

source

@[ext]

theorem distrib_mul_action_hom.ext_ring {M' : Type u_1} {R : Type u_11} [semiring R] [add_monoid M'] [distrib_mul_action R M'] {f g : R →+[R] M'} (h : ⇑f 1 = ⇑g 1) :

f = g

source

theorem distrib_mul_action_hom.ext_ring_iff {M' : Type u_1} {R : Type u_11} [semiring R] [add_monoid M'] [distrib_mul_action R M'] {f g : R →+[R] M'} :

f = g ↔ ⇑f 1 = ⇑g 1

source

def mul_semiring_action_hom.to_distrib_mul_action_hom {M : Type u_5} [monoid M] {R : Type u_11} [semiring R] [mul_semiring_action M R] {S : Type u_13} [semiring S] [mul_semiring_action M S] (self : R →+*[M] S) :

R →+[M] S

Reinterpret an equivariant ring homomorphism as an equivariant additive monoid homomorphism.

source

def mul_semiring_action_hom.to_ring_hom {M : Type u_5} [monoid M] {R : Type u_11} [semiring R] [mul_semiring_action M R] {S : Type u_13} [semiring S] [mul_semiring_action M S] (self : R →+*[M] S) :

R →+* S

Reinterpret an equivariant ring homomorphism as a ring homomorphism.

source

@[nolint]

structure mul_semiring_action_hom (M : Type u_5) [monoid M] (R : Type u_11) [semiring R] [mul_semiring_action M R] (S : Type u_13) [semiring S] [mul_semiring_action M S] :

Type (max u_11 u_13)

to_fun : R → S
map_smul' : ∀ (m : M) (x : R), self.to_fun (m • x) = m • self.to_fun x
map_zero' : self.to_fun 0 = 0
map_add' : ∀ (x y : R), self.to_fun (x + y) = self.to_fun x + self.to_fun y
map_one' : self.to_fun 1 = 1
map_mul' : ∀ (x y : R), self.to_fun (x * y) = (self.to_fun x) * self.to_fun y

Equivariant ring homomorphisms.

source

@[protected, instance]

def mul_semiring_action_hom.has_coe (M : Type u_5) [monoid M] (R : Type u_11) [semiring R] [mul_semiring_action M R] (S : Type u_13) [semiring S] [mul_semiring_action M S] :

has_coe (R →+*[M] S) (R →+* S)

Equations

mul_semiring_action_hom.has_coe M R S = {coe := mul_semiring_action_hom.to_ring_hom _inst_20}

source

@[protected, instance]

def mul_semiring_action_hom.has_coe' (M : Type u_5) [monoid M] (R : Type u_11) [semiring R] [mul_semiring_action M R] (S : Type u_13) [semiring S] [mul_semiring_action M S] :

has_coe (R →+*[M] S) (R →+[M] S)

Equations

mul_semiring_action_hom.has_coe' M R S = {coe := mul_semiring_action_hom.to_distrib_mul_action_hom _inst_20}

source

@[protected, instance]

def mul_semiring_action_hom.has_coe_to_fun (M : Type u_5) [monoid M] (R : Type u_11) [semiring R] [mul_semiring_action M R] (S : Type u_13) [semiring S] [mul_semiring_action M S] :

has_coe_to_fun (R →+*[M] S) (λ (_x : R →+*[M] S), R → S)

Equations

mul_semiring_action_hom.has_coe_to_fun M R S = {coe := λ (c : R →+*[M] S), c.to_fun}

source

@[norm_cast]

theorem mul_semiring_action_hom.coe_fn_coe {M : Type u_5} [monoid M] {R : Type u_11} [semiring R] [mul_semiring_action M R] {S : Type u_13} [semiring S] [mul_semiring_action M S] (f : R →+*[M] S) :

⇑↑f = ⇑f

source

@[norm_cast]

theorem mul_semiring_action_hom.coe_fn_coe' {M : Type u_5} [monoid M] {R : Type u_11} [semiring R] [mul_semiring_action M R] {S : Type u_13} [semiring S] [mul_semiring_action M S] (f : R →+*[M] S) :

⇑↑f = ⇑f

source

@[ext]

theorem mul_semiring_action_hom.ext {M : Type u_5} [monoid M] {R : Type u_11} [semiring R] [mul_semiring_action M R] {S : Type u_13} [semiring S] [mul_semiring_action M S] {f g : R →+*[M] S} :

(∀ (x : R), ⇑f x = ⇑g x) → f = g

source

theorem mul_semiring_action_hom.ext_iff {M : Type u_5} [monoid M] {R : Type u_11} [semiring R] [mul_semiring_action M R] {S : Type u_13} [semiring S] [mul_semiring_action M S] {f g : R →+*[M] S} :

f = g ↔ ∀ (x : R), ⇑f x = ⇑g x

source

@[simp]

theorem mul_semiring_action_hom.map_zero {M : Type u_5} [monoid M] {R : Type u_11} [semiring R] [mul_semiring_action M R] {S : Type u_13} [semiring S] [mul_semiring_action M S] (f : R →+*[M] S) :

⇑f 0 = 0

source

@[simp]

theorem mul_semiring_action_hom.map_add {M : Type u_5} [monoid M] {R : Type u_11} [semiring R] [mul_semiring_action M R] {S : Type u_13} [semiring S] [mul_semiring_action M S] (f : R →+*[M] S) (x y : R) :

⇑f (x + y) = ⇑f x + ⇑f y

source

@[simp]

theorem mul_semiring_action_hom.map_neg {M : Type u_5} [monoid M] (R' : Type u_12) [ring R'] [mul_semiring_action M R'] (S' : Type u_14) [ring S'] [mul_semiring_action M S'] (f : R' →+*[M] S') (x : R') :

⇑f (-x) = -⇑f x

source

@[simp]

theorem mul_semiring_action_hom.map_sub {M : Type u_5} [monoid M] (R' : Type u_12) [ring R'] [mul_semiring_action M R'] (S' : Type u_14) [ring S'] [mul_semiring_action M S'] (f : R' →+*[M] S') (x y : R') :

⇑f (x - y) = ⇑f x - ⇑f y

source

@[simp]

theorem mul_semiring_action_hom.map_one {M : Type u_5} [monoid M] {R : Type u_11} [semiring R] [mul_semiring_action M R] {S : Type u_13} [semiring S] [mul_semiring_action M S] (f : R →+*[M] S) :

⇑f 1 = 1

source

@[simp]

theorem mul_semiring_action_hom.map_mul {M : Type u_5} [monoid M] {R : Type u_11} [semiring R] [mul_semiring_action M R] {S : Type u_13} [semiring S] [mul_semiring_action M S] (f : R →+*[M] S) (x y : R) :

⇑f (x * y) = (⇑f x) * ⇑f y

source

@[simp]

theorem mul_semiring_action_hom.map_smul {M : Type u_5} [monoid M] {R : Type u_11} [semiring R] [mul_semiring_action M R] {S : Type u_13} [semiring S] [mul_semiring_action M S] (f : R →+*[M] S) (m : M) (x : R) :

⇑f (m • x) = m • ⇑f x

source

@[protected]

def mul_semiring_action_hom.id (M : Type u_5) [monoid M] {R : Type u_11} [semiring R] [mul_semiring_action M R] :

R →+*[M] R

The identity map as an equivariant ring homomorphism.

Equations

mul_semiring_action_hom.id M = {to_fun := id R, map_smul' := _, map_zero' := _, map_add' := _, map_one' := _, map_mul' := _}

source

@[simp]

theorem mul_semiring_action_hom.id_apply (M : Type u_5) [monoid M] {R : Type u_11} [semiring R] [mul_semiring_action M R] (x : R) :

⇑(mul_semiring_action_hom.id M) x = x

source

def mul_semiring_action_hom.comp {M : Type u_5} [monoid M] {R : Type u_11} [semiring R] [mul_semiring_action M R] {S : Type u_13} [semiring S] [mul_semiring_action M S] {T : Type u_15} [semiring T] [mul_semiring_action M T] (g : S →+*[M] T) (f : R →+*[M] S) :

R →+*[M] T

Composition of two equivariant additive monoid homomorphisms.

Equations

g.comp f = {to_fun := (↑g.comp ↑f).to_fun, map_smul' := _, map_zero' := _, map_add' := _, map_one' := _, map_mul' := _}

source

@[simp]

theorem mul_semiring_action_hom.comp_apply {M : Type u_5} [monoid M] {R : Type u_11} [semiring R] [mul_semiring_action M R] {S : Type u_13} [semiring S] [mul_semiring_action M S] {T : Type u_15} [semiring T] [mul_semiring_action M T] (g : S →+*[M] T) (f : R →+*[M] S) (x : R) :

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

source

@[simp]

theorem mul_semiring_action_hom.id_comp {M : Type u_5} [monoid M] {R : Type u_11} [semiring R] [mul_semiring_action M R] {S : Type u_13} [semiring S] [mul_semiring_action M S] (f : R →+*[M] S) :

(mul_semiring_action_hom.id M).comp f = f

source

@[simp]

theorem mul_semiring_action_hom.comp_id {M : Type u_5} [monoid M] {R : Type u_11} [semiring R] [mul_semiring_action M R] {S : Type u_13} [semiring S] [mul_semiring_action M S] (f : R →+*[M] S) :

f.comp (mul_semiring_action_hom.id M) = f

source

def is_invariant_subring.subtype_hom (M : Type u_5) [monoid M] {R' : Type u_12} [ring R'] [mul_semiring_action M R'] (U : subring R') [is_invariant_subring M U] :

↥U →+*[M] R'

The canonical inclusion from an invariant subring.

Equations

is_invariant_subring.subtype_hom M U = {to_fun := U.subtype.to_fun, map_smul' := _, map_zero' := _, map_add' := _, map_one' := _, map_mul' := _}

source

@[simp]

theorem is_invariant_subring.coe_subtype_hom (M : Type u_5) [monoid M] {R' : Type u_12} [ring R'] [mul_semiring_action M R'] (U : subring R') [is_invariant_subring M U] :

⇑(is_invariant_subring.subtype_hom M U) = coe

source

@[simp]

theorem is_invariant_subring.coe_subtype_hom' (M : Type u_5) [monoid M] {R' : Type u_12} [ring R'] [mul_semiring_action M R'] (U : subring R') [is_invariant_subring M U] :

↑(is_invariant_subring.subtype_hom M U) = U.subtype

mathlib documentation

Equivariant homomorphisms #

Main definitions #

Notations #