Theorems · Definition · group theory

SpecialLinearGroup.baseChange

{R : Type u_1} →
  {V : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup V] →
        [inst_2 : Module R V] →
          {S : Type u_3} →
            [inst_3 : CommRing S] →
              [inst_4 : Algebra R S] →
                [Module.Free R V] →
                  [Module.Finite R V] → SpecialLinearGroup R V →* SpecialLinearGroup S (TensorProduct R S V)

By base change, an R-algebra S induces a group homomorphism from SpecialLinearGroup R V to SpecialLinearGroup S (S ⊗[R] V).

Defined in

Mathlib.LinearAlgebra.SpecialLinearGroup

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupModuleCommRingAlgebraModule.FreeModule.Finite