# Further basic results about Algebra. #

This file could usefully be split further.

instance PUnit.algebra {R : Type u} [] :
Equations
• PUnit.algebra = Algebra.mk { toFun := fun (x : R) => PUnit.unit, map_one' := , map_mul' := , map_zero' := , map_add' := }
@[simp]
theorem Algebra.algebraMap_pUnit {R : Type u} [] (r : R) :
instance ULift.algebra {R : Type u} {A : Type w} [] [] [Algebra R A] :
Algebra R ()
Equations
• One or more equations did not get rendered due to their size.
theorem ULift.algebraMap_eq {R : Type u} {A : Type w} [] [] [Algebra R A] (r : R) :
(algebraMap R ()) r = { down := () r }
@[simp]
theorem ULift.down_algebraMap {R : Type u} {A : Type w} [] [] [Algebra R A] (r : R) :
((algebraMap R ()) r).down = () r
instance Algebra.ofSubsemiring {R : Type u} {A : Type w} [] [] [Algebra R A] (S : ) :
Algebra (S) A

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

Equations
theorem Algebra.algebraMap_ofSubsemiring {R : Type u} [] (S : ) :
algebraMap (S) R = S.subtype
theorem Algebra.coe_algebraMap_ofSubsemiring {R : Type u} [] (S : ) :
(algebraMap (S) R) = Subtype.val
theorem Algebra.algebraMap_ofSubsemiring_apply {R : Type u} [] (S : ) (x : S) :
(algebraMap (S) R) x = x
instance Algebra.ofSubring {R : Type u_2} {A : Type u_3} [] [Ring A] [Algebra R A] (S : ) :
Algebra (S) A

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

Equations
theorem Algebra.algebraMap_ofSubring {R : Type u_2} [] (S : ) :
algebraMap (S) R = S.subtype
theorem Algebra.coe_algebraMap_ofSubring {R : Type u_2} [] (S : ) :
(algebraMap (S) R) = Subtype.val
theorem Algebra.algebraMap_ofSubring_apply {R : Type u_2} [] (S : ) (x : S) :
(algebraMap (S) R) x = x
def Algebra.algebraMapSubmonoid {R : Type u} [] (S : Type u_2) [] [Algebra R S] (M : ) :

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

Equations
Instances For
theorem Algebra.mem_algebraMapSubmonoid_of_mem {R : Type u} [] {S : Type u_2} [] [Algebra R S] {M : } (x : M) :
() x
theorem Algebra.mul_sub_algebraMap_commutes {R : Type u} {A : Type w} [] [Ring A] [Algebra R A] (x : A) (r : R) :
x * (x - () r) = (x - () r) * x
theorem Algebra.mul_sub_algebraMap_pow_commutes {R : Type u} {A : Type w} [] [Ring A] [Algebra R A] (x : A) (r : R) (n : ) :
x * (x - () r) ^ n = (x - () r) ^ n * x
@[reducible, inline]
abbrev Algebra.semiringToRing (R : Type u) {A : Type w} [] [] [Algebra R A] :

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

Equations
• = let __spread.0 := inferInstance; let __spread.1 := ; Ring.mk SubNegMonoid.zsmul
Instances For
instance Module.End.instAlgebra (R : Type u) (S : Type v) (M : Type w) [] [] [] [Module R M] [Module S M] [] [SMul R S] [] :
Algebra R ()
Equations
theorem Module.algebraMap_end_eq_smul_id (R : Type u) (S : Type v) (M : Type w) [] [] [] [Module R M] [Module S M] [] [SMul R S] [] (a : R) :
(algebraMap R ()) a = a LinearMap.id
@[simp]
theorem Module.algebraMap_end_apply (R : Type u) (S : Type v) (M : Type w) [] [] [] [Module R M] [Module S M] [] [SMul R S] [] (a : R) (m : M) :
((algebraMap R ()) a) m = a m
@[simp]
theorem Module.ker_algebraMap_end (K : Type u) (V : Type v) [] [] [Module K V] (a : K) (ha : a 0) :
theorem Module.End_algebraMap_isUnit_inv_apply_eq_iff {R : Type u} (S : Type v) {M : Type w} [] [] [] [Module R M] [Module S M] [] [SMul R S] [] {x : R} (h : IsUnit ((algebraMap R ()) x)) (m : 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} [] [] [] [Module R M] [Module S M] [] [SMul R S] [] {x : R} (h : IsUnit ((algebraMap R ()) x)) (m : 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} [] [] [] [Algebra R A] [Algebra R B] (f : A →ₗ[R] B) (a : A) (r : R) :
f (() r * a) = () 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} [] [] [] [Algebra R A] [Algebra R B] (f : A →ₗ[R] B) (a : A) (r : R) :
f (a * () r) = f a * () r
@[instance 99]
instance algebraNat {R : Type u_1} [] :

Semiring ⥤ ℕ-Alg

Equations
• algebraNat =
instance nat_algebra_subsingleton {R : Type u_1} [] :
Equations
• =
@[instance 99]
instance algebraInt (R : Type u_1) [Ring R] :

Ring ⥤ ℤ-Alg

Equations
@[simp]
theorem algebraMap_int_eq (R : Type u_1) [Ring R] :

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

instance int_algebra_subsingleton {R : Type u_1} [Ring R] :
Equations
• =
theorem NoZeroSMulDivisors.of_algebraMap_injective {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] [] (h : Function.Injective ()) :

If algebraMap R A is injective and A has no zero divisors, R-multiples in A are zero only if one of the factors is zero.

Cannot be an instance because there is no Injective (algebraMap R A) typeclass.

theorem NoZeroSMulDivisors.algebraMap_injective (R : Type u_1) (A : Type u_2) [] [Ring A] [] [Algebra R A] [] :
theorem NeZero.of_noZeroSMulDivisors (R : Type u_1) (A : Type u_2) (n : ) [] [NeZero n] [Ring A] [] [Algebra R A] [] :
NeZero n
@[instance 100]
Equations
• =
@[instance 100]
Equations
• =
@[instance 100]
instance NoZeroSMulDivisors.Algebra.noZeroSMulDivisors {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] [] [] :
Equations
• =
theorem algebra_compatible_smul {R : Type u_1} [] (A : Type u_2) [] [Algebra R A] {M : Type u_3} [] [Module A M] [Module R M] [] (r : R) (m : M) :
r m = () r m
@[simp]
theorem algebraMap_smul {R : Type u_1} [] (A : Type u_2) [] [Algebra R A] {M : Type u_3} [] [Module A M] [Module R M] [] (r : R) (m : M) :
() r m = r m
theorem intCast_smul {k : Type u_5} {V : Type u_6} [] [] [Module k V] (r : ) (x : V) :
r x = r x
theorem NoZeroSMulDivisors.trans (R : Type u_5) (A : Type u_6) (M : Type u_7) [] [Ring A] [] [Algebra R A] [] [Module R M] [Module A M] [] [] [] :
@[instance 120]
instance IsScalarTower.to_smulCommClass {R : Type u_1} [] {A : Type u_2} [] [Algebra R A] {M : Type u_3} [] [Module A M] [Module R M] [] :
Equations
• =
@[instance 110]
instance IsScalarTower.to_smulCommClass' {R : Type u_1} [] {A : Type u_2} [] [Algebra R A] {M : Type u_3} [] [Module A M] [Module R M] [] :
Equations
• =
@[instance 200]
instance Algebra.to_smulCommClass {R : Type u_5} {A : Type u_6} [] [] [Algebra R A] :
Equations
• =
theorem smul_algebra_smul_comm {R : Type u_1} [] {A : Type u_2} [] [Algebra R A] {M : Type u_3} [] [Module A M] [Module R M] [] (r : R) (a : A) (m : M) :
a r m = r a m
def LinearMap.ltoFun (R : Type u) (M : Type v) (A : Type w) [] [] [Module R M] [] [Algebra R A] :
(M →ₗ[R] A) →ₗ[A] MA

A-linearly coerce an R-linear map from M to A to a function, given an algebra A over a commutative semiring R and M a module over R.

Equations
• = { toFun := fun (f : M →ₗ[R] A) => f.toFun, map_add' := , map_smul' := }
Instances For

TODO: The following lemmas no longer involve Algebra at all, and could be moved closer to Algebra/Module/Submodule.lean. Currently this is tricky because ker, range, , and are all defined in LinearAlgebra/Basic.lean.

@[simp]
theorem LinearMap.ker_restrictScalars (R : Type u_1) {S : Type u_2} {M : Type u_3} {N : Type u_4} [] [] [SMul R S] [] [Module R M] [Module S M] [] [] [Module R N] [Module S N] [] (f : M →ₗ[S] N) :
LinearMap.ker (R f) =
@[reducible, inline]
abbrev Invertible.algebraMapOfInvertibleAlgebraMap {R : Type u_1} {A : Type u_2} {B : Type u_3} [] [] [] [Algebra R A] [Algebra R B] (f : A →ₗ[R] B) (hf : f 1 = 1) {r : R} (h : Invertible (() r)) :
Invertible (() 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
• = { invOf := f (() r), invOf_mul_self := , mul_invOf_self := }
Instances For
theorem IsUnit.algebraMap_of_algebraMap {R : Type u_1} {A : Type u_2} {B : Type u_3} [] [] [] [Algebra R A] [Algebra R B] (f : A →ₗ[R] B) (hf : f 1 = 1) {r : R} (h : IsUnit (() r)) :
IsUnit (() 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} [] [] [Algebra F E] (b : F →ₗ[F] E) (hb : ) :

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} [] [] [Algebra F E] (b : F →ₗ[F] E) (hb : ) :

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} [] [] [Algebra F E] (b : F →ₗ[F] E) (hb : ) :

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} [] [] [Algebra F E] (b : F ≃ₗ[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} [] [] [Algebra R S] (h : ) {M : Type u_3} {N : Type u_4} [] [] [Module R M] [Module S M] [] [Module R N] [Module 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.
Instances For
@[reducible, inline]
abbrev LinearMap.extendScalarsOfSurjective {R : Type u_1} {S : Type u_2} [] [] [Algebra R S] (h : ) {M : Type u_3} {N : Type u_4} [] [] [Module R M] [Module S M] [] [Module R N] [Module S N] [] (l : M →ₗ[R] N) :

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

Equations
Instances For
@[simp]
theorem LinearMap.extendScalarsOfSurjective_apply {R : Type u_1} {S : Type u_4} [] [] [Algebra R S] (h : ) {M : Type u_2} {N : Type u_3} [] [] [Module R M] [Module S M] [] [Module R N] [Module S N] [] (l : M →ₗ[R] N) (x : M) :
= l x
def LinearEquiv.extendScalarsOfSurjective {R : Type u_1} {S : Type u_2} [] [] [Algebra R S] (h : ) {M : Type u_3} {N : Type u_4} [] [] [Module R M] [Module S M] [] [Module R N] [Module S N] [] (f : M ≃ₗ[R] N) :

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

Equations
• = let __spread.0 := f; { toAddHom := (__spread.0).toAddHom, map_smul' := , invFun := __spread.0.invFun, left_inv := , right_inv := }
Instances For
@[simp]
theorem LinearEquiv.extendScalarsOfSurjective_apply {R : Type u_1} {S : Type u_4} [] [] [Algebra R S] (h : ) {M : Type u_2} {N : Type u_3} [] [] [Module R M] [Module S M] [] [Module R N] [Module S N] [] (f : M ≃ₗ[R] N) (x : M) :
= f x
@[simp]
theorem LinearEquiv.extendScalarsOfSurjective_symm {R : Type u_1} {S : Type u_4} [] [] [Algebra R S] (h : ) {M : Type u_2} {N : Type u_3} [] [] [Module R M] [Module S M] [] [Module R N] [Module S N] [] (f : M ≃ₗ[R] N) :
.symm =