Documentation

Mathlib.Algebra.Algebra.Basic

Further basic results about Algebra. #

This file could usefully be split further.

Equations
  • PUnit.algebra = Algebra.mk { toFun := fun (x : R) => PUnit.unit, map_one' := , map_mul' := , map_zero' := , map_add' := }
instance ULift.algebra {R : Type u} {A : Type w} [CommSemiring R] [Semiring A] [Algebra R 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
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
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) :

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.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] :

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

    Equations
    Instances For
      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] :
      Equations
      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) :
      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] :

      Semiring ⥤ ℕ-Alg

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

      Ring ⥤ ℤ-Alg

      Equations
      @[simp]

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

      Equations
      • =

      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 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
      @[instance 100]
      Equations
      • =
      @[instance 100]
      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] :
      @[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] :
      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] :
      Equations
      • =
      @[instance 200]
      instance Algebra.to_smulCommClass {R : Type u_5} {A : Type u_6} [CommSemiring R] [Semiring A] [Algebra R 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] 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
      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} [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) :
        @[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)) :

        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
        Instances For
          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) :

          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) :

          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) :

          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) :

          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] (h : Function.Surjective (algebraMap 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] :

          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} [CommSemiring R] [Semiring S] [Algebra R S] (h : Function.Surjective (algebraMap 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] (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} [CommSemiring R] [Semiring S] [Algebra R S] (h : Function.Surjective (algebraMap 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] (l : M →ₗ[R] N) (x : M) :
              def LinearEquiv.extendScalarsOfSurjective {R : Type u_1} {S : Type u_2} [CommSemiring R] [Semiring S] [Algebra R S] (h : Function.Surjective (algebraMap 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] (f : M ≃ₗ[R] N) :

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

              Equations
              Instances For
                @[simp]
                theorem LinearEquiv.extendScalarsOfSurjective_apply {R : Type u_1} {S : Type u_4} [CommSemiring R] [Semiring S] [Algebra R S] (h : Function.Surjective (algebraMap 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] (f : M ≃ₗ[R] N) (x : M) :
                @[simp]