Lifting monoid algebras

This file defines liftNC. For the definition of MonoidAlgebra.lift, see Mathlib/Algebra/MonoidAlgebra/Basic.lean.

Main results

• MonoidAlgebra.liftNC, AddMonoidAlgebra.liftNC: lift a homomorphism f : k →+ R and a function g : G → R to a homomorphism MonoidAlgebra k G →+ R.

Multiplicative monoids

def MonoidAlgebra.liftNC {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] [NonUnitalNonAssocSemiring R] (f : k →+ R) (g : G → R) : MonoidAlgebra k G →+ R

A non-commutative version of MonoidAlgebra.lift: given an additive homomorphism f : k →+ R and a homomorphism g : G → R, returns the additive homomorphism from MonoidAlgebra k G such that liftNC f g (single a b) = f b * g a. If f is a ring homomorphism and the range of either f or g is in center of R, then the result is a ring homomorphism. If R is a k-algebra and f = algebraMap k R, then the result is an algebra homomorphism called MonoidAlgebra.lift.

Equations

• MonoidAlgebra.liftNC f g = Finsupp.liftAddHom fun (x : G) => (AddMonoidHom.mulRight (g x)).comp f

@[simp]

theorem MonoidAlgebra.liftNC_single {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] [NonUnitalNonAssocSemiring R] (f : k →+ R) (g : G → R) (a : G) (b : k) : (liftNC f g) (single a b) = f b * g a

theorem MonoidAlgebra.liftNC_mul {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] [Mul G] [Semiring R] {g_hom : Type u_6} [FunLike g_hom G R] [MulHomClass g_hom G R] (f : k →+* R) (g : g_hom) (a b : MonoidAlgebra k G) (h_comm : ∀ {x y : G}, y ∈ a.support → Commute (f (b x)) (g y)) : (liftNC ↑f ⇑g) (a * b) = (liftNC ↑f ⇑g) a * (liftNC ↑f ⇑g) b

@[simp]

theorem MonoidAlgebra.liftNC_one {k : Type u₁} {G : Type u₂} {R : Type u_2} [NonAssocSemiring R] [Semiring k] [One G] {g_hom : Type u_6} [FunLike g_hom G R] [OneHomClass g_hom G R] (f : k →+* R) (g : g_hom) : (liftNC ↑f ⇑g) 1 = 1

Semiring structure

def MonoidAlgebra.liftNCRingHom {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] [Monoid G] [Semiring R] (f : k →+* R) (g : G →* R) (h_comm : ∀ (x : k) (y : G), Commute (f x) (g y)) : MonoidAlgebra k G →+* R

liftNC as a RingHom, for when f x and g y commute

Equations

• MonoidAlgebra.liftNCRingHom f g h_comm = { toFun := (↑(MonoidAlgebra.liftNC ↑f ⇑g)).toFun, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem MonoidAlgebra.liftNCRingHom_single {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] [Monoid G] [Semiring R] (f : k →+* R) (g : G →* R) (h_comm : ∀ (x : k) (y : G), Commute (f x) (g y)) (a : G) (b : k) : (liftNCRingHom f g h_comm) (single a b) = f b * g a

noncomputable def MonoidAlgebra.mapRangeRingHom {R : Type u_2} {S : Type u_3} (M : Type u_5) [Semiring R] [Semiring S] [Monoid M] (f : R →+* S) : MonoidAlgebra R M →+* MonoidAlgebra S M

The ring homomorphism of monoid algebras induced by a homomorphism of the base rings.

Equations

• MonoidAlgebra.mapRangeRingHom M f = MonoidAlgebra.liftNCRingHom (MonoidAlgebra.singleOneRingHom.comp f) (MonoidAlgebra.of S M) ⋯

@[simp]

theorem MonoidAlgebra.mapRangeRingHom_apply {R : Type u_2} {S : Type u_3} {M : Type u_5} [Semiring R] [Semiring S] [Monoid M] (f : R →+* S) (x : MonoidAlgebra R M) (m : M) : ((mapRangeRingHom M f) x) m = f (x m)

@[simp]

theorem MonoidAlgebra.mapRangeRingHom_single {R : Type u_2} {S : Type u_3} {M : Type u_5} [Semiring R] [Semiring S] [Monoid M] (f : R →+* S) (a : M) (b : R) : (mapRangeRingHom M f) (single a b) = single a (f b)

@[simp]

theorem MonoidAlgebra.mapRangeRingHom_id {R : Type u_2} {M : Type u_5} [Semiring R] [Monoid M] : mapRangeRingHom M (RingHom.id R) = RingHom.id (MonoidAlgebra R M)

@[simp]

theorem MonoidAlgebra.mapRangeRingHom_comp {R : Type u_2} {S : Type u_3} {T : Type u_4} {M : Type u_5} [Semiring R] [Semiring S] [Semiring T] [Monoid M] (f : S →+* T) (g : R →+* S) : mapRangeRingHom M (f.comp g) = (mapRangeRingHom M f).comp (mapRangeRingHom M g)

Additive monoids

def AddMonoidAlgebra.liftNC {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] [NonUnitalNonAssocSemiring R] (f : k →+ R) (g : Multiplicative G → R) : AddMonoidAlgebra k G →+ R

A non-commutative version of AddMonoidAlgebra.lift: given an additive homomorphism f : k →+ R and a map g : Multiplicative G → R, returns the additive homomorphism from k[G] such that liftNC f g (single a b) = f b * g a. If f is a ring homomorphism and the range of either f or g is in center of R, then the result is a ring homomorphism. If R is a k-algebra and f = algebraMap k R, then the result is an algebra homomorphism called AddMonoidAlgebra.lift.

Equations

• AddMonoidAlgebra.liftNC f g = Finsupp.liftAddHom fun (x : G) => (AddMonoidHom.mulRight (g (Multiplicative.ofAdd x))).comp f

@[simp]

theorem AddMonoidAlgebra.liftNC_single {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] [NonUnitalNonAssocSemiring R] (f : k →+ R) (g : Multiplicative G → R) (a : G) (b : k) : (liftNC f g) (single a b) = f b * g (Multiplicative.ofAdd a)

theorem AddMonoidAlgebra.liftNC_mul {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] [Add G] [Semiring R] {g_hom : Type u_6} [FunLike g_hom (Multiplicative G) R] [MulHomClass g_hom (Multiplicative G) R] (f : k →+* R) (g : g_hom) (a b : AddMonoidAlgebra k G) (h_comm : ∀ {x y : G}, y ∈ a.support → Commute (f (b x)) (g (Multiplicative.ofAdd y))) : (liftNC ↑f ⇑g) (a * b) = (liftNC ↑f ⇑g) a * (liftNC ↑f ⇑g) b

@[simp]

theorem AddMonoidAlgebra.liftNC_one {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] [Zero G] [NonAssocSemiring R] {g_hom : Type u_6} [FunLike g_hom (Multiplicative G) R] [OneHomClass g_hom (Multiplicative G) R] (f : k →+* R) (g : g_hom) : (liftNC ↑f ⇑g) 1 = 1

Semiring structure

def AddMonoidAlgebra.liftNCRingHom {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] [AddMonoid G] [Semiring R] (f : k →+* R) (g : Multiplicative G →* R) (h_comm : ∀ (x : k) (y : Multiplicative G), Commute (f x) (g y)) : AddMonoidAlgebra k G →+* R

liftNC as a RingHom, for when f and g commute

Equations

• AddMonoidAlgebra.liftNCRingHom f g h_comm = { toFun := (↑(AddMonoidAlgebra.liftNC ↑f ⇑g)).toFun, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem AddMonoidAlgebra.liftNCRingHom_single {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] [AddMonoid G] [Semiring R] (f : k →+* R) (g : Multiplicative G →* R) (h_comm : ∀ (x : k) (y : Multiplicative G), Commute (f x) (g y)) (a : G) (b : k) : (liftNCRingHom f g h_comm) (single a b) = f b * g (Multiplicative.ofAdd a)

noncomputable def AddMonoidAlgebra.mapRangeRingHom {R : Type u_2} {S : Type u_3} (M : Type u_5) [Semiring R] [Semiring S] [AddMonoid M] (f : R →+* S) : AddMonoidAlgebra R M →+* AddMonoidAlgebra S M

The ring homomorphism of monoid algebras induced by a homomorphism of the base rings.

Equations

• AddMonoidAlgebra.mapRangeRingHom M f = AddMonoidAlgebra.liftNCRingHom (AddMonoidAlgebra.singleZeroRingHom.comp f) (AddMonoidAlgebra.of S M) ⋯

@[simp]

theorem AddMonoidAlgebra.mapRangeRingHom_apply {R : Type u_2} {S : Type u_3} {M : Type u_5} [Semiring R] [Semiring S] [AddMonoid M] (f : R →+* S) (x : AddMonoidAlgebra R M) (m : M) : ((mapRangeRingHom M f) x) m = f (x m)

@[simp]

theorem AddMonoidAlgebra.mapRangeRingHom_single {R : Type u_2} {S : Type u_3} {M : Type u_5} [Semiring R] [Semiring S] [AddMonoid M] (f : R →+* S) (a : M) (b : R) : (mapRangeRingHom M f) (single a b) = single a (f b)

@[simp]

theorem AddMonoidAlgebra.mapRangeRingHom_id {R : Type u_2} {M : Type u_5} [Semiring R] [AddMonoid M] : mapRangeRingHom M (RingHom.id R) = RingHom.id (AddMonoidAlgebra R M)

@[simp]

theorem AddMonoidAlgebra.mapRangeRingHom_comp {R : Type u_2} {S : Type u_3} {T : Type u_4} {M : Type u_5} [Semiring R] [Semiring S] [Semiring T] [AddMonoid M] (f : S →+* T) (g : R →+* S) : mapRangeRingHom M (f.comp g) = (mapRangeRingHom M f).comp (mapRangeRingHom M g)