Documentation

Mathlib.RingTheory.AlgebraTower

Towers of algebras #

We set up the basic theory of algebra towers. An algebra tower A/S/R is expressed by having instances of Algebra A S, Algebra R S, Algebra R A and IsScalarTower R S A, the later asserting the compatibility condition (r • s) • a = r • (s • a).

In FieldTheory/Tower.lean we use this to prove the tower law for finite extensions, that if R and S are both fields, then [A:R] = [A:S] [S:A].

In this file we prepare the main lemma: if {bi | i ∈ I} is an R-basis of S and {cj | j ∈ J} is an S-basis of A, then {bi cj | i ∈ I, j ∈ J} is an R-basis of A. This statement does not require the base rings to be a field, so we also generalize the lemma to rings in this file.

def IsScalarTower.Invertible.algebraTower (R : Type u) (S : Type v) (A : Type w) [CommSemiring R] [CommSemiring S] [Semiring A] [Algebra R S] [Algebra S A] [Algebra R A] [IsScalarTower R S A] (r : R) [Invertible (↑(algebraMap R S) r)] :
Invertible (↑(algebraMap R A) r)

Suppose that R → S → A is a tower of algebras. If an element r : R is invertible in S, then it is invertible in A.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    def IsScalarTower.invertibleAlgebraCoeNat (R : Type u) (A : Type w) [CommSemiring R] [Semiring A] [Algebra R A] (n : ) [inv : Invertible n] :

    A natural number that is invertible when coerced to R is also invertible when coerced to any R-algebra.

    Equations
    Instances For
      @[simp]
      theorem Basis.algebraMapCoeffs_repr_apply_support_val {R : Type u} (A : Type w) {ι : Type u_1} {M : Type u_2} [CommSemiring R] [Semiring A] [AddCommMonoid M] [Algebra R A] [Module A M] [Module R M] [IsScalarTower R A M] (b : Basis ι R M) (h : Function.Bijective ↑(algebraMap R A)) :
      ∀ (a : M), ((Basis.algebraMapCoeffs A b h).repr a).support.val = Multiset.filter (fun x => ¬↑(RingEquiv.symm (RingEquiv.symm (RingEquiv.ofBijective (algebraMap R A) h))) (↑(↑(LinearEquiv.restrictScalars A b.repr) a) x) = 0) (↑(LinearEquiv.restrictScalars A b.repr) a).support.val
      @[simp]
      theorem Basis.algebraMapCoeffs_repr_apply_toFun {R : Type u} (A : Type w) {ι : Type u_1} {M : Type u_2} [CommSemiring R] [Semiring A] [AddCommMonoid M] [Algebra R A] [Module A M] [Module R M] [IsScalarTower R A M] (b : Basis ι R M) (h : Function.Bijective ↑(algebraMap R A)) :
      ∀ (a : M) (a_1 : ι), ↑((Basis.algebraMapCoeffs A b h).repr a) a_1 = ↑(algebraMap R A) (↑(↑(LinearEquiv.restrictScalars A b.repr) a) a_1)
      noncomputable def Basis.algebraMapCoeffs {R : Type u} (A : Type w) {ι : Type u_1} {M : Type u_2} [CommSemiring R] [Semiring A] [AddCommMonoid M] [Algebra R A] [Module A M] [Module R M] [IsScalarTower R A M] (b : Basis ι R M) (h : Function.Bijective ↑(algebraMap R A)) :
      Basis ι A M

      If R and A have a bijective algebraMap R A and act identically on M, then a basis for M as R-module is also a basis for M as R'-module.

      Equations
      Instances For
        theorem Basis.algebraMapCoeffs_apply {R : Type u} (A : Type w) {ι : Type u_1} {M : Type u_2} [CommSemiring R] [Semiring A] [AddCommMonoid M] [Algebra R A] [Module A M] [Module R M] [IsScalarTower R A M] (b : Basis ι R M) (h : Function.Bijective ↑(algebraMap R A)) (i : ι) :
        ↑(Basis.algebraMapCoeffs A b h) i = b i
        @[simp]
        theorem Basis.coe_algebraMapCoeffs {R : Type u} (A : Type w) {ι : Type u_1} {M : Type u_2} [CommSemiring R] [Semiring A] [AddCommMonoid M] [Algebra R A] [Module A M] [Module R M] [IsScalarTower R A M] (b : Basis ι R M) (h : Function.Bijective ↑(algebraMap R A)) :
        ↑(Basis.algebraMapCoeffs A b h) = b
        theorem linearIndependent_smul {R : Type u} {S : Type v} {A : Type w} [CommSemiring R] [Semiring S] [AddCommMonoid A] [Algebra R S] [Module S A] [Module R A] [IsScalarTower R S A] {ι : Type v₁} {b : ιS} {ι' : Type w₁} {c : ι'A} (hb : LinearIndependent R b) (hc : LinearIndependent S c) :
        LinearIndependent R fun p => b p.fst c p.snd
        noncomputable def Basis.smul {R : Type u} {S : Type v} {A : Type w} [CommSemiring R] [Semiring S] [AddCommMonoid A] [Algebra R S] [Module S A] [Module R A] [IsScalarTower R S A] {ι : Type v₁} {ι' : Type w₁} (b : Basis ι R S) (c : Basis ι' S A) :
        Basis (ι × ι') R A

        Basis.SMul (b : Basis ι R S) (c : Basis ι S A) is the R-basis on A where the (i, j)th basis vector is b i • c j.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[simp]
          theorem Basis.smul_repr {R : Type u} {S : Type v} {A : Type w} [CommSemiring R] [Semiring S] [AddCommMonoid A] [Algebra R S] [Module S A] [Module R A] [IsScalarTower R S A] {ι : Type v₁} {ι' : Type w₁} (b : Basis ι R S) (c : Basis ι' S A) (x : A) (ij : ι × ι') :
          ↑((Basis.smul b c).repr x) ij = ↑(b.repr (↑(c.repr x) ij.snd)) ij.fst
          theorem Basis.smul_repr_mk {R : Type u} {S : Type v} {A : Type w} [CommSemiring R] [Semiring S] [AddCommMonoid A] [Algebra R S] [Module S A] [Module R A] [IsScalarTower R S A] {ι : Type v₁} {ι' : Type w₁} (b : Basis ι R S) (c : Basis ι' S A) (x : A) (i : ι) (j : ι') :
          ↑((Basis.smul b c).repr x) (i, j) = ↑(b.repr (↑(c.repr x) j)) i
          @[simp]
          theorem Basis.smul_apply {R : Type u} {S : Type v} {A : Type w} [CommSemiring R] [Semiring S] [AddCommMonoid A] [Algebra R S] [Module S A] [Module R A] [IsScalarTower R S A] {ι : Type v₁} {ι' : Type w₁} (b : Basis ι R S) (c : Basis ι' S A) (ij : ι × ι') :
          ↑(Basis.smul b c) ij = b ij.fst c ij.snd
          theorem Basis.algebraMap_injective {R : Type u} {S : Type v} [CommRing R] [Ring S] [Algebra R S] {ι : Type u_1} [NoZeroDivisors R] [Nontrivial S] (b : Basis ι R S) :
          def AlgHom.restrictDomain {A : Type w} (B : Type u₁) {C : Type u_1} {D : Type u_2} [CommSemiring A] [CommSemiring C] [CommSemiring D] [Algebra A C] [Algebra A D] (f : C →ₐ[A] D) [CommSemiring B] [Algebra A B] [Algebra B C] [IsScalarTower A B C] :

          Restrict the domain of an AlgHom.

          Equations
          Instances For
            def AlgHom.extendScalars {A : Type w} (B : Type u₁) {C : Type u_1} {D : Type u_2} [CommSemiring A] [CommSemiring C] [CommSemiring D] [Algebra A C] [Algebra A D] (f : C →ₐ[A] D) [CommSemiring B] [Algebra A B] [Algebra B C] [IsScalarTower A B C] :

            Extend the scalars of an AlgHom.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              def algHomEquivSigma {A : Type w} {B : Type u₁} {C : Type u_1} {D : Type u_2} [CommSemiring A] [CommSemiring C] [CommSemiring D] [Algebra A C] [Algebra A D] [CommSemiring B] [Algebra A B] [Algebra B C] [IsScalarTower A B C] :
              (C →ₐ[A] D) (f : B →ₐ[A] D) × (C →ₐ[B] D)

              AlgHoms from the top of a tower are equivalent to a pair of AlgHoms.

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