Further basic results about Algebra.

This file could usefully be split further.

@[implicit_reducible]

instance PUnit.algebra {R : Type u_1} [CommSemiring R] : Algebra R PUnit.{v + 1}

Equations

• PUnit.algebra = { toSMul := PUnit.smul, algebraMap := { toFun := fun (x : R) => PUnit.unit, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }, commutes' := ⋯, smul_def' := ⋯ }

@[simp]

theorem Algebra.algebraMap_pUnit {R : Type u_1} [CommSemiring R] (r : R) : (algebraMap R PUnit.{u_4 + 1}) r = PUnit.unit

@[implicit_reducible]

instance ULift.algebra {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] : Algebra R (ULift.{u_4, u_2} A)

Equations

• One or more equations did not get rendered due to their size.

theorem ULift.algebraMap_eq {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (r : R) : (algebraMap R (ULift.{u_4, u_2} A)) r = { down := (algebraMap R A) r }

@[simp]

theorem ULift.down_algebraMap {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (r : R) : ((algebraMap R (ULift.{u_4, u_2} A)) r).down = (algebraMap R A) r

@[implicit_reducible]

def ULift.algebra' (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] : Algebra (ULift.{u, u_1} R) A

If A is an R-algebra, it is also a ULift R-algebra. In particular, Ulift A is a ULift R algebra. This is not an instance, because it causes a non-reducible diamond in the case where A = Ulift R.

Equations

• ULift.algebra' R A = { toSMul := ULift.module.toSMul, algebraMap := (algebraMap R A).comp ULift.ringEquiv.toRingHom, commutes' := ⋯, smul_def' := ⋯ }

@[simp]

theorem ULift.algebraMap_apply' {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (r : ULift.{u_4, u_1} R) : (algebraMap (ULift.{u_4, u_1} R) A) r = (algebraMap R A) r.down

This references the ULift.algebra' instance.

@[implicit_reducible, instance 900]

instance Algebra.ofSubsemiring {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] {C : Type u_4} [SetLike C R] [SubsemiringClass C R] (S : C) : Algebra (↥S) A

Algebra over a subsemiring. This builds upon Subsemiring.module.

Equations

• Algebra.ofSubsemiring S = { toSMul := DistribMulAction.toDistribSMul.toSMul, algebraMap := (algebraMap R A).comp (Subsemiring.ofClass S).subtype, commutes' := ⋯, smul_def' := ⋯ }

theorem Algebra.algebraMap_ofSubsemiring {R : Type u_1} [CommSemiring R] (S : Subsemiring R) : algebraMap (↥S) R = S.subtype

theorem Algebra.coe_algebraMap_ofSubsemiring {R : Type u_1} [CommSemiring R] {C : Type u_4} [SetLike C R] [SubsemiringClass C R] (S : C) : ⇑(algebraMap (↥S) R) = Subtype.val

theorem Algebra.algebraMap_ofSubsemiring_apply {R : Type u_1} [CommSemiring R] {C : Type u_4} [SetLike C R] [SubsemiringClass C R] (S : C) (x : ↥S) : (algebraMap (↥S) R) x = ↑x

@[implicit_reducible]

instance Algebra.ofSubring {R : Type u_5} {A : Type u_6} [CommRing R] [Ring A] [Algebra R A] (S : Subring R) : Algebra (↥S) A

Algebra over a subring. This builds upon Subring.module.

Equations

• Algebra.ofSubring S = inferInstance

theorem Algebra.algebraMap_ofSubring {R : Type u_5} [CommRing R] (S : Subring R) : algebraMap (↥S) R = S.subtype

@[deprecated Algebra.coe_algebraMap_ofSubsemiring (since := "2025-11-23")]

theorem Algebra.coe_algebraMap_ofSubring {R : Type u_5} [CommRing R] (S : Subring R) : ⇑(algebraMap (↥S) R) = Subtype.val

@[deprecated Algebra.algebraMap_ofSubsemiring_apply (since := "2025-11-23")]

theorem Algebra.algebraMap_ofSubring_apply {R : Type u_5} [CommRing R] (S : Subring R) (x : ↥S) : (algebraMap (↥S) R) x = ↑x

def Algebra.algebraMapSubmonoid {R : Type u_1} [CommSemiring R] (S : Type u_4) [Semiring S] [Algebra R S] (M : Submonoid R) : Submonoid S

Explicit characterization of the submonoid map in the case of an algebra. S is made explicit to help with type inference

Equations

• Algebra.algebraMapSubmonoid S M = Submonoid.map (algebraMap R S) M

theorem Algebra.mem_algebraMapSubmonoid_of_mem {R : Type u_1} [CommSemiring R] {S : Type u_4} [Semiring S] [Algebra R S] {M : Submonoid R} (x : ↥M) : (algebraMap R S) ↑x ∈ algebraMapSubmonoid S M

@[simp]

theorem Algebra.algebraMapSubmonoid_self {R : Type u_1} [CommSemiring R] (M : Submonoid R) : algebraMapSubmonoid R M = M

@[simp]

theorem Algebra.algebraMapSubmonoid_powers {R : Type u_1} [CommSemiring R] {S : Type u_4} [Semiring S] [Algebra R S] (r : R) : algebraMapSubmonoid S (Submonoid.powers r) = Submonoid.powers ((algebraMap R S) r)

theorem Algebra.mul_sub_algebraMap_commutes {R : Type u_1} {A : Type u_2} [CommSemiring R] [Ring A] [Algebra R A] (x : A) (r : R) : x * (x - (algebraMap R A) r) = (x - (algebraMap R A) r) * x

theorem Algebra.mul_sub_algebraMap_pow_commutes {R : Type u_1} {A : Type u_2} [CommSemiring R] [Ring A] [Algebra R A] (x : A) (r : R) (n : ℕ) : x * (x - (algebraMap R A) r) ^ n = (x - (algebraMap R A) r) ^ n * x

@[reducible, inline]

abbrev Algebra.semiringToRing {A : Type u_2} (R : Type u_4) [CommRing R] [Semiring A] [Algebra R A] : Ring A

A Semiring that is an Algebra over a commutative ring carries a natural Ring structure. See note [reducible non-instances].

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev RingHom.commSemiringToCommRing {R : Type u_4} {A : Type u_5} [CommRing R] [CommSemiring A] (φ : R →+* A) : CommRing A

The CommRing structure on a CommSemiring induced by a ring morphism from a CommRing.

Equations

• φ.commSemiringToCommRing = { toRing := Algebra.semiringToRing R, mul_comm := ⋯ }

@[implicit_reducible]

instance Algebra.instSubtypeMemSubringCenter {R : Type u_4} [Ring R] : Algebra (↥(Subring.center R)) R

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Module.End.instAlgebra (R : Type u) (S : Type v) (M : Type w) [CommSemiring R] [Semiring S] [AddCommMonoid M] [Module R M] [Module S M] [SMulCommClass S R M] [SMul R S] [IsScalarTower R S M] : Algebra R (End S M)

Equations

• Module.End.instAlgebra R S M = Algebra.ofModule ⋯ ⋯

theorem Module.algebraMap_end_eq_smul_id (R : Type u) (S : Type v) (M : Type w) [CommSemiring R] [Semiring S] [AddCommMonoid M] [Module R M] [Module S M] [SMulCommClass S R M] [SMul R S] [IsScalarTower R S M] (a : R) : (algebraMap R (End S M)) a = a • LinearMap.id

@[simp]

theorem Module.algebraMap_end_apply (R : Type u) (S : Type v) (M : Type w) [CommSemiring R] [Semiring S] [AddCommMonoid M] [Module R M] [Module S M] [SMulCommClass S R M] [SMul R S] [IsScalarTower R S M] (a : R) (m : M) : ((algebraMap R (End S M)) a) m = a • m

@[simp]

theorem Module.ker_algebraMap_end (K : Type u) (V : Type v) [Semifield K] [AddCommMonoid V] [Module K V] (a : K) (ha : a ≠ 0) : LinearMap.ker ((algebraMap K (End K V)) a) = ⊥

theorem Module.End.algebraMap_isUnit_inv_apply_eq_iff {R : Type u} (S : Type v) {M : Type w} [CommSemiring R] [Semiring S] [AddCommMonoid M] [Module R M] [Module S M] [SMulCommClass S R M] [SMul R S] [IsScalarTower R S M] {x : R} (h : IsUnit ((algebraMap R (End S M)) x)) (m m' : M) : ↑h.unit⁻¹ m = m' ↔ m = x • m'

theorem Module.End.algebraMap_isUnit_inv_apply_eq_iff' {R : Type u} (S : Type v) {M : Type w} [CommSemiring R] [Semiring S] [AddCommMonoid M] [Module R M] [Module S M] [SMulCommClass S R M] [SMul R S] [IsScalarTower R S M] {x : R} (h : IsUnit ((algebraMap R (End S M)) x)) (m m' : M) : m' = ↑h.unit⁻¹ m ↔ m = x • m'

theorem LinearMap.map_algebraMap_mul {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₗ[R] B) (a : A) (r : R) : f ((algebraMap R A) r * a) = (algebraMap R B) r * f a

An alternate statement of LinearMap.map_smul for when algebraMap is more convenient to work with than •.

theorem LinearMap.map_mul_algebraMap {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₗ[R] B) (a : A) (r : R) : f (a * (algebraMap R A) r) = f a * (algebraMap R B) r

@[implicit_reducible, instance 99]

instance Semiring.toNatAlgebra {R : Type u_1} [Semiring R] : Algebra ℕ R

Semiring ⥤ ℕ-Alg

Equations

• Semiring.toNatAlgebra = { toSMul := AddMonoid.toNSMul, algebraMap := Nat.castRingHom R, commutes' := ⋯, smul_def' := ⋯ }

instance nat_algebra_subsingleton {R : Type u_1} [Semiring R] : Subsingleton (Algebra ℕ R)

@[simp]

theorem algebraMap_comp_natCast (R : Type u_2) (A : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] : ⇑(algebraMap R A) ∘ Nat.cast = Nat.cast

@[implicit_reducible, instance 99]

instance Ring.toIntAlgebra (R : Type u_1) [Ring R] : Algebra ℤ R

Ring ⥤ ℤ-Alg

Equations

• Ring.toIntAlgebra R = { toSMul := SubNegMonoid.toZSMul, algebraMap := Int.castRingHom R, commutes' := ⋯, smul_def' := ⋯ }

@[simp]

theorem algebraMap_int_eq (R : Type u_1) [Ring R] : algebraMap ℤ R = Int.castRingHom R

A special case of eq_intCast' that happens to be true definitionally

instance int_algebra_subsingleton {R : Type u_1} [Ring R] : Subsingleton (Algebra ℤ R)

@[simp]

theorem algebraMap_comp_intCast (R : Type u_2) (A : Type u_3) [CommRing R] [Ring A] [Algebra R A] : ⇑(algebraMap R A) ∘ Int.cast = Int.cast

theorem NeZero.of_faithfulSMul (R : Type u_1) (A : Type u_2) [Semiring R] [Semiring A] [Module R A] [IsScalarTower R A A] [FaithfulSMul R A] (n : ℕ) [NeZero ↑n] : NeZero ↑n

theorem faithfulSMul_iff_algebraMap_injective (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] : FaithfulSMul R A ↔ Function.Injective ⇑(algebraMap R A)

theorem FaithfulSMul.algebraMap_injective (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] [FaithfulSMul R A] : Function.Injective ⇑(algebraMap R A)

@[simp]

theorem FaithfulSMul.algebraMap_eq_zero_iff (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] [FaithfulSMul R A] {r : R} : (algebraMap R A) r = 0 ↔ r = 0

@[simp]

theorem FaithfulSMul.algebraMap_eq_one_iff (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] [FaithfulSMul R A] {r : R} : (algebraMap R A) r = 1 ↔ r = 1

@[simp]

theorem algebraMap.coe_inj (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] [FaithfulSMul R A] {a b : R} : ↑a = ↑b ↔ a = b

theorem algebraMap.coe_eq_zero_iff (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] [FaithfulSMul R A] (a : R) : ↑a = 0 ↔ a = 0

@[deprecated algebraMap.coe_eq_zero_iff (since := "2025-10-21")]

theorem algebraMap.lift_map_eq_zero_iff (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] [FaithfulSMul R A] (a : R) : ↑a = 0 ↔ a = 0

theorem Algebra.charZero_of_charZero (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] [FaithfulSMul R A] [CharZero R] : CharZero A

instance instFaithfulSMulNatOfCharZero (R : Type u_1) [CommSemiring R] [CharZero R] : FaithfulSMul ℕ R

instance instFaithfulSMulIntOfCharZero (R : Type u_3) [Ring R] [CharZero R] : FaithfulSMul ℤ R

theorem algebra_compatible_smul {R : Type u_1} [CommSemiring R] (A : Type u_2) [Semiring A] [Algebra R A] {M : Type u_3} [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] (r : R) (m : M) : r • m = (algebraMap R A) r • m

@[simp]

theorem algebraMap_smul {R : Type u_1} [CommSemiring R] (A : Type u_2) [Semiring A] [Algebra R A] {M : Type u_3} [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] (r : R) (m : M) : (algebraMap R A) r • m = r • m

theorem isSMulRegular_algebraMap_iff {R : Type u_1} [CommSemiring R] (A : Type u_2) [Semiring A] [Algebra R A] {M : Type u_3} [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] {r : R} : IsSMulRegular M ((algebraMap R A) r) ↔ IsSMulRegular M r

@[instance 120]

instance IsScalarTower.to_smulCommClass {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [Algebra R A] {M : Type u_3} [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] : SMulCommClass R A M

@[instance 110]

instance IsScalarTower.to_smulCommClass' {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [Algebra R A] {M : Type u_3} [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] : SMulCommClass A R M

@[instance 10000]

instance Algebra.to_smulCommClass {R : Type u_4} {A : Type u_5} [CommSemiring R] [Semiring A] [Algebra R A] : SMulCommClass R A A

This has high priority because it is almost always the right instance when it applies.

@[instance 100]

instance instSMulCommClass {R : Type u_4} {S : Type u_5} {A : Type u_6} [CommSemiring R] [CommSemiring S] [Semiring A] [Algebra R A] [Algebra S A] : SMulCommClass R S A

theorem smul_algebra_smul_comm {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [Algebra R A] {M : Type u_3} [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] (r : R) (a : A) (m : M) : a • r • m = r • a • m

theorem NoZeroDivisors.of_faithfulSMul (R : Type u_1) (A : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] [FaithfulSMul R A] [NoZeroDivisors A] : NoZeroDivisors R

theorem IsCancelMulZero.of_faithfulSMul (R : Type u_1) (A : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] [FaithfulSMul R A] [IsCancelMulZero A] : IsCancelMulZero R

theorem IsDomain.of_faithfulSMul (R : Type u_1) (A : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] [FaithfulSMul R A] [IsDomain A] : IsDomain R

theorem Module.IsTorsionFree.of_faithfulSMul (R : Type u_1) (S : Type u_2) (A : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] [FaithfulSMul R A] [Semiring S] [Module S R] [Module S A] [IsScalarTower S R A] [IsTorsionFree S A] : IsTorsionFree S R

theorem Module.IsTorsionFree.trans_faithfulSMul (R : Type u_1) (A : Type u_3) (M : Type u_4) [CommSemiring R] [Semiring A] [Algebra R A] [FaithfulSMul R A] [Nontrivial R] [IsCancelMulZero A] [AddCommMonoid M] [Module A M] [Module R M] [IsTorsionFree A M] [IsScalarTower R A M] : IsTorsionFree R M

@[instance 100]

instance FaithfulSMul.to_isTorsionFree (R : Type u_1) (A : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] [FaithfulSMul R A] [Nontrivial R] [IsCancelMulZero A] : Module.IsTorsionFree R A

@[instance 101]

instance Module.IsTorsionFree.to_faithfulSMul {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] [IsCancelMulZero R] [Nontrivial A] [IsTorsionFree R A] : FaithfulSMul R A

theorem Module.isTorsionFree_iff_faithfulSMul {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] [IsDomain R] [IsDomain A] : IsTorsionFree R A ↔ FaithfulSMul R A

theorem Module.isTorsionFree_iff_algebraMap_injective {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] [IsDomain R] [IsDomain A] : IsTorsionFree R A ↔ Function.Injective ⇑(algebraMap R A)

@[deprecated Module.isTorsionFree_iff_algebraMap_injective (since := "2026-01-21")]

theorem NoZeroSMulDivisors.iff_algebraMap_injective {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] [IsDomain R] [IsDomain A] : Module.IsTorsionFree R A ↔ Function.Injective ⇑(algebraMap R A)

Alias of Module.isTorsionFree_iff_algebraMap_injective.

@[deprecated Module.isTorsionFree_iff_faithfulSMul (since := "2026-01-21")]

theorem NoZeroSMulDivisors.iff_faithfulSMul {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] [IsDomain R] [IsDomain A] : Module.IsTorsionFree R A ↔ FaithfulSMul R A

Alias of Module.isTorsionFree_iff_faithfulSMul.

@[reducible, inline]

abbrev Invertible.algebraMapOfInvertibleAlgebraMap {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₗ[R] B) (hf : f 1 = 1) {r : R} (h : Invertible ((algebraMap R A) r)) : Invertible ((algebraMap R B) r)

If there is a linear map f : A →ₗ[R] B that preserves 1, then algebraMap R B r is invertible when algebraMap R A r is.

Equations

• Invertible.algebraMapOfInvertibleAlgebraMap f hf h = { invOf := f ⅟((algebraMap R A) r), invOf_mul_self := ⋯, mul_invOf_self := ⋯ }

theorem IsUnit.algebraMap_of_algebraMap {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₗ[R] B) (hf : f 1 = 1) {r : R} (h : IsUnit ((algebraMap R A) r)) : IsUnit ((algebraMap R B) r)

If there is a linear map f : A →ₗ[R] B that preserves 1, then algebraMap R B r is a unit when algebraMap R A r is.

theorem injective_algebraMap_of_linearMap {F : Type u_1} {E : Type u_2} [CommSemiring F] [Semiring E] [Algebra F E] (b : F →ₗ[F] E) (hb : Function.Injective ⇑b) : Function.Injective ⇑(algebraMap F E)

If E is an F-algebra, and there exists an injective F-linear map from F to E, then the algebra map from F to E is also injective.

theorem surjective_algebraMap_of_linearMap {F : Type u_1} {E : Type u_2} [CommSemiring F] [Semiring E] [Algebra F E] (b : F →ₗ[F] E) (hb : Function.Surjective ⇑b) : Function.Surjective ⇑(algebraMap F E)

If E is an F-algebra, and there exists a surjective F-linear map from F to E, then the algebra map from F to E is also surjective.

theorem bijective_algebraMap_of_linearMap {F : Type u_1} {E : Type u_2} [CommSemiring F] [Semiring E] [Algebra F E] (b : F →ₗ[F] E) (hb : Function.Bijective ⇑b) : Function.Bijective ⇑(algebraMap F E)

If E is an F-algebra, and there exists a bijective F-linear map from F to E, then the algebra map from F to E is also bijective.

NOTE: The same result can also be obtained if there are two F-linear maps from F to E, one is injective, the other one is surjective. In this case, use injective_algebraMap_of_linearMap and surjective_algebraMap_of_linearMap separately.

theorem bijective_algebraMap_of_linearEquiv {F : Type u_1} {E : Type u_2} [CommSemiring F] [Semiring E] [Algebra F E] (b : F ≃ₗ[F] E) : Function.Bijective ⇑(algebraMap F E)

If E is an F-algebra, there exists an F-linear isomorphism from F to E (namely, E is a free F-module of rank one), then the algebra map from F to E is bijective.

def LinearMap.extendScalarsOfSurjectiveEquiv {R : Type u_1} {S : Type u_2} [CommSemiring R] [Semiring S] [Algebra R S] {M : Type u_3} {N : Type u_4} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module S M] [IsScalarTower R S M] [Module R N] [Module S N] [IsScalarTower R S N] (h : Function.Surjective ⇑(algebraMap R S)) : (M →ₗ[R] N) ≃ₗ[R] M →ₗ[S] N

If R →+* S is surjective, then S-linear maps between modules are exactly R-linear maps.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev LinearMap.extendScalarsOfSurjective {R : Type u_1} {S : Type u_2} [CommSemiring R] [Semiring S] [Algebra R S] {M : Type u_3} {N : Type u_4} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module S M] [IsScalarTower R S M] [Module R N] [Module S N] [IsScalarTower R S N] (h : Function.Surjective ⇑(algebraMap R S)) (l : M →ₗ[R] N) : M →ₗ[S] N

If R →+* S is surjective, then R-linear maps are also S-linear.

Equations

• LinearMap.extendScalarsOfSurjective h l = (LinearMap.extendScalarsOfSurjectiveEquiv h) l

def LinearEquiv.extendScalarsOfSurjective {R : Type u_1} {S : Type u_2} [CommSemiring R] [Semiring S] [Algebra R S] {M : Type u_3} {N : Type u_4} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module S M] [IsScalarTower R S M] [Module R N] [Module S N] [IsScalarTower R S N] (h : Function.Surjective ⇑(algebraMap R S)) (f : M ≃ₗ[R] N) : M ≃ₗ[S] N

If R →+* S is surjective, then R-linear isomorphisms are also S-linear.

Equations

• LinearEquiv.extendScalarsOfSurjective h f = { toAddHom := (↑f).toAddHom, map_smul' := ⋯, invFun := f.invFun, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem LinearMap.extendScalarsOfSurjective_apply {R : Type u_1} {S : Type u_4} [CommSemiring R] [Semiring S] [Algebra R S] {M : Type u_2} {N : Type u_3} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module S M] [IsScalarTower R S M] [Module R N] [Module S N] [IsScalarTower R S N] (h : Function.Surjective ⇑(algebraMap R S)) (l : M →ₗ[R] N) (x : M) : (extendScalarsOfSurjective h l) x = l x

@[simp]

theorem LinearEquiv.extendScalarsOfSurjective_apply {R : Type u_1} {S : Type u_4} [CommSemiring R] [Semiring S] [Algebra R S] {M : Type u_2} {N : Type u_3} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module S M] [IsScalarTower R S M] [Module R N] [Module S N] [IsScalarTower R S N] (h : Function.Surjective ⇑(algebraMap R S)) (f : M ≃ₗ[R] N) (x : M) : (extendScalarsOfSurjective h f) x = f x

@[simp]

theorem LinearEquiv.extendScalarsOfSurjective_symm {R : Type u_1} {S : Type u_4} [CommSemiring R] [Semiring S] [Algebra R S] {M : Type u_2} {N : Type u_3} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module S M] [IsScalarTower R S M] [Module R N] [Module S N] [IsScalarTower R S N] (h : Function.Surjective ⇑(algebraMap R S)) (f : M ≃ₗ[R] N) : (extendScalarsOfSurjective h f).symm = extendScalarsOfSurjective h f.symm

theorem algebraMap.coe_prod {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [Algebra R A] {ι : Type u_3} {s : Finset ι} (a : ι → R) : ↑(∏ i ∈ s, a i) = ∏ i ∈ s, ↑(a i)

theorem algebraMap.coe_sum {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [Algebra R A] {ι : Type u_3} {s : Finset ι} (a : ι → R) : ↑(∑ i ∈ s, a i) = ∑ i ∈ s, ↑(a i)