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_2 + 1} ) r = PUnit.unit

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

Equations

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

theorem ULift.algebraMap_eq {R : Type u} {A : Type w} [CommSemiring R] [Semiring A] [Algebra R A] (r : R) : (algebraMap R (ULift.{u_2, 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_2, 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_2} {A : Type u_3} [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_2} [CommRing R] (S : Subring R) : algebraMap (↥S) R = S.subtype

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

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

def Algebra.algebraMapSubmonoid {R : Type u} [CommSemiring R] (S : Type u_2) [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_2} [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 (R : Type u) {A : Type w} [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 = let __spread.0 := inferInstance; let __spread.1 := Module.addCommMonoidToAddCommGroup R; Ring.mk ⋯ SubNegMonoid.zsmul ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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' : 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) : 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 algebraNat {R : Type u_1} [Semiring R] : Algebra ℕ R

Semiring ⥤ ℕ-Alg

Equations

• algebraNat = Algebra.mk (Nat.castRingHom R) ⋯ ⋯

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

Equations

• ⋯ = ⋯

@[simp]

theorem RingHom.map_rat_algebraMap {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] [Algebra ℚ R] [Algebra ℚ S] (f : R →+* S) (r : ℚ) : f ((algebraMap ℚ R) r) = (algebraMap ℚ S) r

instance algebraRat {α : Type u_1} [DivisionRing α] [CharZero α] : Algebra ℚ α

Equations

• algebraRat = Algebra.mk (Rat.castHom α) ⋯ ⋯

instance instAlgebraNNRatRat : Algebra ℚ≥0 ℚ

The rational numbers are an algebra over the non-negative rationals.

Equations

• instAlgebraNNRatRat = NNRat.coeHom.toAlgebra

@[simp]

theorem algebraMap_rat_rat : algebraMap ℚ ℚ = RingHom.id ℚ

instance algebra_rat_subsingleton {α : Type u_1} [Semiring α] : Subsingleton (Algebra ℚ α)

Equations

• ⋯ = ⋯

@[instance 99]

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

Ring ⥤ ℤ-Alg

Equations

• algebraInt 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

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

Equations

• ⋯ = ⋯

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)

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)

@[instance 100]

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

Equations

• ⋯ = ⋯

@[instance 100]

instance NoZeroSMulDivisors.CharZero.noZeroSMulDivisors_int {R : Type u_1} [Ring R] [NoZeroDivisors R] [CharZero R] : NoZeroSMulDivisors ℤ R

Equations

• ⋯ = ⋯

@[instance 100]

instance NoZeroSMulDivisors.Algebra.noZeroSMulDivisors {R : Type u_1} {A : Type u_2} [Field R] [Semiring A] [Algebra R A] [Nontrivial A] [NoZeroDivisors A] : NoZeroSMulDivisors R A

Equations

• ⋯ = ⋯

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 intCast_smul {k : Type u_5} {V : Type u_6} [CommRing k] [AddCommGroup V] [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) [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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

@[instance 200]

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

Equations

• ⋯ = ⋯

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.