Documentation

Mathlib.Algebra.Algebra.Pi

The R-algebra structure on families of R-algebras #

The R-algebra structure on ∀ i : I, A i when each A i is an R-algebra.

Main definitions #

instance Pi.algebra (I : Type u) {R : Type u_1} (f : IType v) {r : CommSemiring R} [s : (i : I) → Semiring (f i)] [(i : I) → Algebra R (f i)] :
Algebra R ((i : I) → f i)
Equations
theorem Pi.algebraMap_def (I : Type u) {R : Type u_1} (f : IType v) :
∀ {x : CommSemiring R} [_s : (i : I) → Semiring (f i)] [inst : (i : I) → Algebra R (f i)] (a : R), (algebraMap R ((i : I) → f i)) a = fun (i : I) => (algebraMap R (f i)) a
@[simp]
theorem Pi.algebraMap_apply (I : Type u) {R : Type u_1} (f : IType v) :
∀ {x : CommSemiring R} [_s : (i : I) → Semiring (f i)] [inst : (i : I) → Algebra R (f i)] (a : R) (i : I), (algebraMap R ((i : I) → f i)) a i = (algebraMap R (f i)) a
@[simp]
theorem Pi.evalAlgHom_apply {I : Type u} (R : Type u_1) (f : IType v) :
∀ {x : CommSemiring R} [inst : (i : I) → Semiring (f i)] [inst_1 : (i : I) → Algebra R (f i)] (i : I) (f_1 : (i : I) → f i), (Pi.evalAlgHom R f i) f_1 = f_1 i
def Pi.evalAlgHom {I : Type u} (R : Type u_1) (f : IType v) :
{x : CommSemiring R} → [inst : (i : I) → Semiring (f i)] → [inst_1 : (i : I) → Algebra R (f i)] → (i : I) → ((i : I) → f i) →ₐ[R] f i

Function.eval as an AlgHom. The name matches Pi.evalRingHom, Pi.evalMonoidHom, etc.

Equations
  • Pi.evalAlgHom R f i = let __src := Pi.evalRingHom f i; { toFun := fun (f : (i : I) → f i) => f i, map_one' := , map_mul' := , map_zero' := , map_add' := , commutes' := }
Instances For
    @[simp]
    theorem Pi.constAlgHom_apply (R : Type u_1) (A : Type u_2) (B : Type u_3) [CommSemiring R] [Semiring B] [Algebra R B] (a : B) :
    ∀ (a_1 : A), (Pi.constAlgHom R A B) a a_1 = Function.const A a a_1
    def Pi.constAlgHom (R : Type u_1) (A : Type u_2) (B : Type u_3) [CommSemiring R] [Semiring B] [Algebra R B] :
    B →ₐ[R] AB

    Function.const as an AlgHom. The name matches Pi.constRingHom, Pi.constMonoidHom, etc.

    Equations
    Instances For
      @[simp]
      theorem Pi.constRingHom_eq_algebraMap (R : Type u_1) (A : Type u_2) [CommSemiring R] :
      Pi.constRingHom A R = algebraMap R (AR)

      When R is commutative and permits an algebraMap, Pi.constRingHom is equal to that map.

      @[simp]
      theorem Pi.constAlgHom_eq_algebra_ofId (R : Type u_1) (A : Type u_2) [CommSemiring R] :
      Pi.constAlgHom R A R = Algebra.ofId R (AR)
      instance Function.algebra {R : Type u_1} (I : Type u_2) (A : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] :
      Algebra R (IA)

      A special case of Pi.algebra for non-dependent types. Lean struggles to elaborate definitions elsewhere in the library without this,

      Equations
      @[simp]
      theorem AlgHom.compLeft_apply {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) (I : Type u_2) (h : IA) :
      ∀ (a : I), (f.compLeft I) h a = (f h) a
      def AlgHom.compLeft {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) (I : Type u_2) :
      (IA) →ₐ[R] IB

      R-algebra homomorphism between the function spaces I → A and I → B, induced by an R-algebra homomorphism f between A and B.

      Equations
      • f.compLeft I = let __src := f.compLeft I; { toFun := fun (h : IA) => f h, map_one' := , map_mul' := , map_zero' := , map_add' := , commutes' := }
      Instances For
        @[simp]
        theorem AlgEquiv.piCongrRight_apply {R : Type u_1} {ι : Type u_2} {A₁ : ιType u_3} {A₂ : ιType u_4} [CommSemiring R] [(i : ι) → Semiring (A₁ i)] [(i : ι) → Semiring (A₂ i)] [(i : ι) → Algebra R (A₁ i)] [(i : ι) → Algebra R (A₂ i)] (e : (i : ι) → A₁ i ≃ₐ[R] A₂ i) (x : (i : ι) → A₁ i) (j : ι) :
        (AlgEquiv.piCongrRight e) x j = (e j) (x j)
        def AlgEquiv.piCongrRight {R : Type u_1} {ι : Type u_2} {A₁ : ιType u_3} {A₂ : ιType u_4} [CommSemiring R] [(i : ι) → Semiring (A₁ i)] [(i : ι) → Semiring (A₂ i)] [(i : ι) → Algebra R (A₁ i)] [(i : ι) → Algebra R (A₂ i)] (e : (i : ι) → A₁ i ≃ₐ[R] A₂ i) :
        ((i : ι) → A₁ i) ≃ₐ[R] (i : ι) → A₂ i

        A family of algebra equivalences ∀ i, (A₁ i ≃ₐ A₂ i) generates a multiplicative equivalence between ∀ i, A₁ i and ∀ i, A₂ i.

        This is the AlgEquiv version of Equiv.piCongrRight, and the dependent version of AlgEquiv.arrowCongr.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[simp]
          theorem AlgEquiv.piCongrRight_refl {R : Type u_1} {ι : Type u_2} {A : ιType u_3} [CommSemiring R] [(i : ι) → Semiring (A i)] [(i : ι) → Algebra R (A i)] :
          (AlgEquiv.piCongrRight fun (i : ι) => AlgEquiv.refl) = AlgEquiv.refl
          @[simp]
          theorem AlgEquiv.piCongrRight_symm {R : Type u_1} {ι : Type u_2} {A₁ : ιType u_3} {A₂ : ιType u_4} [CommSemiring R] [(i : ι) → Semiring (A₁ i)] [(i : ι) → Semiring (A₂ i)] [(i : ι) → Algebra R (A₁ i)] [(i : ι) → Algebra R (A₂ i)] (e : (i : ι) → A₁ i ≃ₐ[R] A₂ i) :
          (AlgEquiv.piCongrRight e).symm = AlgEquiv.piCongrRight fun (i : ι) => (e i).symm
          @[simp]
          theorem AlgEquiv.piCongrRight_trans {R : Type u_1} {ι : Type u_2} {A₁ : ιType u_3} {A₂ : ιType u_4} {A₃ : ιType u_5} [CommSemiring R] [(i : ι) → Semiring (A₁ i)] [(i : ι) → Semiring (A₂ i)] [(i : ι) → Semiring (A₃ i)] [(i : ι) → Algebra R (A₁ i)] [(i : ι) → Algebra R (A₂ i)] [(i : ι) → Algebra R (A₃ i)] (e₁ : (i : ι) → A₁ i ≃ₐ[R] A₂ i) (e₂ : (i : ι) → A₂ i ≃ₐ[R] A₃ i) :
          (AlgEquiv.piCongrRight e₁).trans (AlgEquiv.piCongrRight e₂) = AlgEquiv.piCongrRight fun (i : ι) => (e₁ i).trans (e₂ i)