Lemmas about different kinds of "lifts" to SkewMonoidAlgebra.

def SkewMonoidAlgebra.liftNCAlgHom {k : Type u_1} {G : Type u_2} [CommSemiring k] [Monoid G] {A : Type u_4} {B : Type u_5} [Semiring A] [Algebra k A] [Semiring B] [Algebra k B] [MulSemiringAction G A] [SMulCommClass G k A] (f : A →ₐ[k] B) (g : G →* B) (h_comm : ∀ {x : A} {y : G}, f (y • x) * g y = g y * f x) : SkewMonoidAlgebra A G →ₐ[k] B

liftNCRingHom as an AlgHom, for when f is an AlgHom

def SkewMonoidAlgebra.lift (k : Type u_1) (G : Type u_2) [CommSemiring k] [Monoid G] (A : Type u_4) [Semiring A] [Algebra k A] [MulSemiringAction G k] [SMulCommClass G k k] : (G →* A) ≃ (SkewMonoidAlgebra k G →ₐ[k] A)

Any monoid homomorphism G →* A can be lifted to an algebra homomorphism SkewMonoidAlgebra k G →ₐ[k] A.

theorem SkewMonoidAlgebra.lift_apply' {k : Type u_1} {G : Type u_2} [CommSemiring k] [Monoid G] {A : Type u_4} [Semiring A] [Algebra k A] [MulSemiringAction G k] [SMulCommClass G k k] (F : G →* A) (f : SkewMonoidAlgebra k G) : ((lift k G A) F) f = f.sum fun (a : G) (b : k) => (algebraMap k A) b * F a

theorem SkewMonoidAlgebra.lift_apply {k : Type u_1} {G : Type u_2} [CommSemiring k] [Monoid G] {A : Type u_4} [Semiring A] [Algebra k A] [MulSemiringAction G k] [SMulCommClass G k k] (F : G →* A) (f : SkewMonoidAlgebra k G) : ((lift k G A) F) f = f.sum fun (a : G) (b : k) => b • F a

theorem SkewMonoidAlgebra.lift_def {k : Type u_1} {G : Type u_2} [CommSemiring k] [Monoid G] {A : Type u_4} [Semiring A] [Algebra k A] [MulSemiringAction G k] [SMulCommClass G k k] (F : G →* A) : ⇑((lift k G A) F) = ⇑(liftNC ↑(algebraMap k A) ⇑F)

@[simp]

theorem SkewMonoidAlgebra.lift_symm_apply {k : Type u_1} {G : Type u_2} [CommSemiring k] [Monoid G] {A : Type u_4} [Semiring A] [Algebra k A] [MulSemiringAction G k] [SMulCommClass G k k] (F : SkewMonoidAlgebra k G →ₐ[k] A) (x : G) : ((lift k G A).symm F) x = F (single x 1)

theorem SkewMonoidAlgebra.lift_of {k : Type u_1} {G : Type u_2} [CommSemiring k] [Monoid G] {A : Type u_4} [Semiring A] [Algebra k A] [MulSemiringAction G k] [SMulCommClass G k k] (F : G →* A) (x : G) : ((lift k G A) F) ((of k G) x) = F x

@[simp]

theorem SkewMonoidAlgebra.lift_single {k : Type u_1} {G : Type u_2} [CommSemiring k] [Monoid G] {A : Type u_4} [Semiring A] [Algebra k A] [MulSemiringAction G k] [SMulCommClass G k k] (F : G →* A) (a : G) (b : k) : ((lift k G A) F) (single a b) = b • F a

theorem SkewMonoidAlgebra.lift_unique' {k : Type u_1} {G : Type u_2} [CommSemiring k] [Monoid G] {A : Type u_4} [Semiring A] [Algebra k A] [MulSemiringAction G k] [SMulCommClass G k k] (F : SkewMonoidAlgebra k G →ₐ[k] A) : F = (lift k G A) ((↑F).comp (of k G))

theorem SkewMonoidAlgebra.lift_unique {k : Type u_1} {G : Type u_2} [CommSemiring k] [Monoid G] {A : Type u_4} [Semiring A] [Algebra k A] [MulSemiringAction G k] [SMulCommClass G k k] (F : SkewMonoidAlgebra k G →ₐ[k] A) (f : SkewMonoidAlgebra k G) : F f = f.sum fun (a : G) (b : k) => b • F (single a 1)

Decomposition of a k-algebra homomorphism from SkewMonoidAlgebra k G by its values on F (single a 1).

def SkewMonoidAlgebra.mapDomainAlgHom {G : Type u_2} [Monoid G] (k : Type u_6) (A : Type u_7) [CommSemiring k] [Semiring A] [Algebra k A] {H : Type u_8} {F : Type u_9} [Monoid H] [FunLike F G H] [MonoidHomClass F G H] [MulSemiringAction G A] [MulSemiringAction H A] [SMulCommClass G k A] [SMulCommClass H k A] {f : F} (hf : ∀ (a : G) (x : A), a • x = f a • x) : SkewMonoidAlgebra A G →ₐ[k] SkewMonoidAlgebra A H

If f : G → H is a multiplicative homomorphism between two monoids, then mapDomain f is an algebra homomorphism between their monoid algebras.

@[simp]

theorem SkewMonoidAlgebra.mapDomainAlgHom_apply {G : Type u_2} [Monoid G] (k : Type u_6) (A : Type u_7) [CommSemiring k] [Semiring A] [Algebra k A] {H : Type u_8} {F : Type u_9} [Monoid H] [FunLike F G H] [MonoidHomClass F G H] [MulSemiringAction G A] [MulSemiringAction H A] [SMulCommClass G k A] [SMulCommClass H k A] {f : F} (hf : ∀ (a : G) (x : A), a • x = f a • x) (a✝ : SkewMonoidAlgebra A G) : (mapDomainAlgHom k A hf) a✝ = a✝.sum fun (a : G) => single (f a)

def SkewMonoidAlgebra.equivMapDomain {k : Type u_1} {G : Type u_2} {H : Type u_3} [AddCommMonoid k] (f : G ≃ H) (l : SkewMonoidAlgebra k G) : SkewMonoidAlgebra k H

Given f : G ≃ H, we can map l : SkewMonoidAlgebra k G to equivMapDomain f l : SkewMonoidAlgebra k H (computably) by mapping the support forwards and the function backwards.

@[simp]

theorem SkewMonoidAlgebra.coeff_equivMapDomain {k : Type u_1} {G : Type u_2} {H : Type u_3} [AddCommMonoid k] (f : G ≃ H) (l : SkewMonoidAlgebra k G) (b : H) : (equivMapDomain f l).coeff b = l.coeff (f.symm b)

theorem SkewMonoidAlgebra.toFinsupp_equivMapDomain {k : Type u_1} {G : Type u_2} {H : Type u_3} [AddCommMonoid k] (f : G ≃ H) (l : SkewMonoidAlgebra k G) : (equivMapDomain f l).toFinsupp = Finsupp.equivMapDomain f l.toFinsupp

theorem SkewMonoidAlgebra.equivMapDomain_eq_mapDomain {k : Type u_1} {G : Type u_2} {H : Type u_3} [AddCommMonoid k] (f : G ≃ H) (l : SkewMonoidAlgebra k G) : equivMapDomain f l = (mapDomain ⇑f) l

theorem SkewMonoidAlgebra.equivMapDomain_trans {k : Type u_1} {G : Type u_2} [AddCommMonoid k] {G' : Type u_4} {G'' : Type u_5} (f : G ≃ G') (g : G' ≃ G'') (l : SkewMonoidAlgebra k G) : equivMapDomain (f.trans g) l = equivMapDomain g (equivMapDomain f l)

@[simp]

theorem SkewMonoidAlgebra.equivMapDomain_refl {k : Type u_1} {G : Type u_2} [AddCommMonoid k] (l : SkewMonoidAlgebra k G) : equivMapDomain (Equiv.refl G) l = l

@[simp]

theorem SkewMonoidAlgebra.equivMapDomain_single {k : Type u_1} {G : Type u_2} {H : Type u_3} [AddCommMonoid k] (f : G ≃ H) (a : G) (b : k) : equivMapDomain f (single a b) = single (f a) b

def SkewMonoidAlgebra.domCongr {G : Type u_2} {H : Type u_3} {A : Type u_4} [AddCommMonoid A] (e : G ≃ H) : SkewMonoidAlgebra A G ≃+ SkewMonoidAlgebra A H

Given AddCommMonoid A and e : G ≃ H, domCongr e is the corresponding Equiv between SkewMonoidAlgebra A G and SkewMonoidAlgebra A H.

@[simp]

theorem SkewMonoidAlgebra.domCongr_apply {G : Type u_2} {H : Type u_3} {A : Type u_4} [AddCommMonoid A] (e : G ≃ H) (l : SkewMonoidAlgebra A G) : (domCongr e) l = equivMapDomain e l

def SkewMonoidAlgebra.domLCongr {k : Type u_1} {G : Type u_2} {H : Type u_3} {A : Type u_4} [Semiring k] [AddCommMonoid A] [Module k A] (e : G ≃ H) : SkewMonoidAlgebra A G ≃ₗ[k] SkewMonoidAlgebra A H

An equivalence of domains induces a linear equivalence of finitely supported functions.

This is domCongr as a LinearEquiv.

def SkewMonoidAlgebra.domCongrAlg (k : Type u_1) {G : Type u_2} {H : Type u_3} (A : Type u_4) [Monoid G] [Monoid H] [Semiring A] [CommSemiring k] [Algebra k A] [MulSemiringAction G A] [MulSemiringAction H A] [SMulCommClass G k A] [SMulCommClass H k A] {e : G ≃* H} (he : ∀ (a : G) (x : A), a • x = e a • x) : SkewMonoidAlgebra A G ≃ₐ[k] SkewMonoidAlgebra A H

If e : G ≃* H is a multiplicative equivalence between two monoids and ∀ (a : G) (x : A), a • x = (e a) • x, then SkewMonoidAlgebra.domCongr e is an algebra equivalence between their skew monoid algebras.

theorem SkewMonoidAlgebra.domCongrAlg_toAlgHom (k : Type u_1) {G : Type u_2} {H : Type u_3} (A : Type u_4) [Monoid G] [Monoid H] [Semiring A] [CommSemiring k] [Algebra k A] [MulSemiringAction G A] [MulSemiringAction H A] [SMulCommClass G k A] [SMulCommClass H k A] {e : G ≃* H} (he : ∀ (a : G) (x : A), a • x = e a • x) : ↑(domCongrAlg k A he) = mapDomainAlgHom k A he

@[simp]

theorem SkewMonoidAlgebra.domCongrAlg_apply (k : Type u_1) {G : Type u_2} {H : Type u_3} (A : Type u_4) [Monoid G] [Monoid H] [Semiring A] [CommSemiring k] [Algebra k A] [MulSemiringAction G A] [MulSemiringAction H A] [SMulCommClass G k A] [SMulCommClass H k A] {e : G ≃* H} (he : ∀ (a : G) (x : A), a • x = e a • x) (f : SkewMonoidAlgebra A G) (h : H) : ((domCongrAlg k A he) f).coeff h = f.coeff (e.symm h)

@[simp]

theorem SkewMonoidAlgebra.domCongr_support (k : Type u_1) {G : Type u_2} {H : Type u_3} (A : Type u_4) [Monoid G] [Monoid H] [Semiring A] [CommSemiring k] [Algebra k A] [MulSemiringAction G A] [MulSemiringAction H A] [SMulCommClass G k A] [SMulCommClass H k A] {e : G ≃* H} (he : ∀ (a : G) (x : A), a • x = e a • x) (f : SkewMonoidAlgebra A G) : ((domCongrAlg k A he) f).support = Finset.map (↑e).toEmbedding f.support

@[simp]

theorem SkewMonoidAlgebra.domCongr_single (k : Type u_1) {G : Type u_2} {H : Type u_3} (A : Type u_4) [Monoid G] [Monoid H] [Semiring A] [CommSemiring k] [Algebra k A] [MulSemiringAction G A] [MulSemiringAction H A] [SMulCommClass G k A] [SMulCommClass H k A] {e : G ≃* H} (he : ∀ (a : G) (x : A), a • x = e a • x) (g : G) (a : A) : (domCongrAlg k A he) (single g a) = single (e g) a

theorem SkewMonoidAlgebra.domCongr_refl (k : Type u_1) {G : Type u_2} (A : Type u_4) [Monoid G] [Semiring A] [CommSemiring k] [Algebra k A] [MulSemiringAction G A] [SMulCommClass G k A] : domCongrAlg k A ⋯ = AlgEquiv.refl

@[simp]

theorem SkewMonoidAlgebra.domCongr_symm (k : Type u_1) {G : Type u_2} {H : Type u_3} (A : Type u_4) [Monoid G] [Monoid H] [Semiring A] [CommSemiring k] [Algebra k A] [MulSemiringAction G A] [MulSemiringAction H A] [SMulCommClass G k A] [SMulCommClass H k A] {e : G ≃* H} (he : ∀ (a : G) (x : A), a • x = e a • x) : (domCongrAlg k A he).symm = domCongrAlg k A ⋯

def SkewMonoidAlgebra.submoduleOfSmulMem {k : Type u_1} {G : Type u_2} [Semiring k] [Monoid G] [MulSemiringAction G k] {V : Type u_4} [AddCommMonoid V] [Module k V] [Module (SkewMonoidAlgebra k G) V] [IsScalarTower k (SkewMonoidAlgebra k G) V] (W : Submodule k V) (h : ∀ (g : G), ∀ v ∈ W, (of k G) g • v ∈ W) : Submodule (SkewMonoidAlgebra k G) V

A submodule over k which is stable under scalar multiplication by elements of G is a submodule over SkewMonoidAlgebra k G