Theorems · Definition · ring theory

SkewMonoidAlgebra.domCongrAlg

(k : Type u_1) →
  {G : Type u_2} →
    {H : Type u_3} →
      (A : Type u_4) →
        [inst : Monoid G] →
          [inst_1 : Monoid H] →
            [inst_2 : Semiring A] →
              [inst_3 : CommSemiring k] →
                [inst_4 : Algebra k A] →
                  [inst_5 : MulSemiringAction G A] →
                    [inst_6 : MulSemiringAction H A] →
                      [inst_7 : SMulCommClass G k A] →
                        [inst_8 : SMulCommClass H k A] →
                          {e : G ≃* H} →
                            (∀ (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.

Defined in

Mathlib.Algebra.SkewMonoidAlgebra.Lift

Cited by

7 results in Mathlib

Foundations

Depth 87 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MonoidMonoidSemiringCommSemiringAlgebraMulSemiringActionMulSemiringActionSMulCommClassSMulCommClass