Further basic results about Algebra.

This file could usefully be split further.

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

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} [CommSemiring R] (r : R) : (algebraMap R PUnit.{u_1 + 1} ) r = PUnit.unit

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

Equations

• ULift.algebra = Algebra.mk { toFun := fun (r : R) => { down := (algebraMap R A) r }, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } ⋯ ⋯

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

@[simp]

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

instance Algebra.ofSubsemiring {R : Type u} {A : Type w} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subsemiring R) : Algebra (↥S) A

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

Equations

• Algebra.ofSubsemiring S = Algebra.mk ((algebraMap R A).comp S.subtype) ⋯ ⋯

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

theorem Algebra.coe_algebraMap_ofSubsemiring {R : Type u} [CommSemiring R] (S : Subsemiring R) : ⇑(algebraMap (↥S) R) = Subtype.val

theorem Algebra.algebraMap_ofSubsemiring_apply {R : Type u} [CommSemiring R] (S : Subsemiring R) (x : ↥S) : (algebraMap (↥S) R) x = ↑x

instance Algebra.ofSubring {R : Type u_1} {A : Type u_2} [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 = Algebra.mk ((algebraMap R A).comp S.subtype) ⋯ ⋯

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

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

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

def Algebra.algebraMapSubmonoid {R : Type u} [CommSemiring R] (S : Type u_1) [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} [CommSemiring R] {S : Type u_1} [Semiring S] [Algebra R S] {M : Submonoid R} (x : ↥M) : (algebraMap R S) ↑x ∈ Algebra.algebraMapSubmonoid S M

theorem Algebra.mul_sub_algebraMap_commutes {R : Type u} {A : Type w} [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} {A : Type w} [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 w} (R : Type u_1) [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

• Algebra.semiringToRing R = Ring.mk ⋯ SubNegMonoid.zsmul ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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

Equations

• Algebra.instSubtypeMemSubringCenter = Algebra.mk { toFun := Subtype.val, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } ⋯ ⋯

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 (Module.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 (Module.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 (Module.End S M)) a) m = a • m

@[simp]

theorem Module.ker_algebraMap_end (K : Type u) (V : Type v) [Field K] [AddCommGroup V] [Module K V] (a : K) (ha : a ≠ 0) : LinearMap.ker ((algebraMap K (Module.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 (Module.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 (Module.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

@[instance 99]

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

Semiring ⥤ ℕ-Alg

Equations

• Semiring.toNatAlgebra = Algebra.mk (Nat.castRingHom R) ⋯ ⋯

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

@[instance 99]

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

Ring ⥤ ℤ-Alg

Equations

• Ring.toIntAlgebra R = Algebra.mk (Int.castRingHom R) ⋯ ⋯

@[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

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

theorem NoZeroSMulDivisors.of_algebraMap_injective {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] [NoZeroDivisors A] (h : Function.Injective ⇑(algebraMap R A)) : NoZeroSMulDivisors R A

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) [CommRing R] [Ring A] [Nontrivial A] [Algebra R A] [NoZeroSMulDivisors R A] : Function.Injective ⇑(algebraMap R A)

@[simp]

theorem NoZeroSMulDivisors.algebraMap_eq_zero_iff (R : Type u_1) (A : Type u_2) [CommRing R] [Ring A] [Nontrivial A] [Algebra R A] [NoZeroSMulDivisors R A] {r : R} : (algebraMap R A) r = 0 ↔ r = 0

@[simp]

theorem NoZeroSMulDivisors.algebraMap_eq_one_iff (R : Type u_1) (A : Type u_2) [CommRing R] [Ring A] [Nontrivial A] [Algebra R A] [NoZeroSMulDivisors R A] {r : R} : (algebraMap R A) r = 1 ↔ r = 1

theorem NeZero.of_noZeroSMulDivisors (R : Type u_1) (A : Type u_2) (n : ℕ) [CommRing R] [NeZero ↑n] [Ring A] [Nontrivial A] [Algebra R A] [NoZeroSMulDivisors R A] : NeZero ↑n

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

theorem NoZeroSMulDivisors.CharZero.noZeroSMulDivisors_nat {R : Type u_1} [Semiring R] [NoZeroDivisors R] [CharZero R] : NoZeroSMulDivisors ℕ R

theorem NoZeroSMulDivisors.CharZero.noZeroSMulDivisors_int {R : Type u_1} [Ring R] [NoZeroDivisors R] [CharZero R] : NoZeroSMulDivisors ℤ 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 NoZeroSMulDivisors.trans (R : Type u_4) (A : Type u_5) (M : Type u_6) [CommRing R] [Ring A] [IsDomain A] [Algebra R A] [AddCommGroup M] [Module R M] [Module A M] [IsScalarTower R A M] [NoZeroSMulDivisors R A] [NoZeroSMulDivisors A M] : NoZeroSMulDivisors R M

theorem 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

theorem 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

theorem Algebra.to_smulCommClass {R : Type u_4} {A : Type u_5} [CommSemiring R] [Semiring A] [Algebra R A] : SMulCommClass R A 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

def LinearMap.ltoFun (R : Type u) (M : Type v) (A : Type w) [CommSemiring R] [AddCommMonoid M] [Module R M] [CommSemiring A] [Algebra R A] : (M →ₗ[R] A) →ₗ[A] M → A

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

• LinearMap.ltoFun R M A = { toFun := fun (f : M →ₗ[R] A) => f.toFun, map_add' := ⋯, map_smul' := ⋯ }

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} [Semiring R] [Semiring S] [SMul R S] [AddCommMonoid M] [Module R M] [Module S M] [IsScalarTower R S M] [AddCommMonoid N] [Module R N] [Module S N] [IsScalarTower R S N] (f : M →ₗ[S] N) : LinearMap.ker (↑R f) = Submodule.restrictScalars R (LinearMap.ker f)

@[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) : (LinearMap.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) : (LinearEquiv.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) : (LinearEquiv.extendScalarsOfSurjective h f).symm = LinearEquiv.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)