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)
:
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
(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 = 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)
:
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)
:
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
Equations
- ⋯ = ⋯
@[simp]
A special case of eq_intCast' that happens to be true definitionally
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))
:
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)
@[instance 100]
instance
NoZeroSMulDivisors.CharZero.noZeroSMulDivisors_nat
{R : Type u_1}
[Semiring R]
[NoZeroDivisors R]
[CharZero R]
:
Equations
- ⋯ = ⋯
@[instance 100]
instance
NoZeroSMulDivisors.CharZero.noZeroSMulDivisors_int
{R : Type u_1}
[Ring R]
[NoZeroDivisors R]
[CharZero R]
:
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
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]
:
@[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_4}
{A : Type u_5}
[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)
:
def
LinearMap.ltoFun
(R : Type u)
(M : Type v)
(A : Type w)
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
[CommSemiring A]
[Algebra R 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))
:
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)
:
If R →+* S is surjective, then R-linear maps are also S-linear.
Equations
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)
:
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)