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 : I → Type v)
{r : CommSemiring R}
[s : (i : I) → Semiring (f i)]
[(i : I) → Algebra R (f i)]
:
Algebra R ((i : I) → f i)
theorem
Pi.algebraMap_def
(I : Type u)
{R : Type u_1}
(f : I → Type 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 => ↑(algebraMap R (f i)) a
@[simp]
theorem
Pi.algebraMap_apply
(I : Type u)
{R : Type u_1}
(f : I → Type 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 : I → Type v)
:
∀ {x : CommSemiring R} [inst : (i : I) → Semiring (f i)] [inst_1 : (i : I) → Algebra R (f i)] (i : I)
(f : (i : I) → f i), ↑(Pi.evalAlgHom R f i) f = f i
def
Pi.evalAlgHom
{I : Type u}
(R : Type u_1)
(f : I → Type 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.
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 : A), ↑(Pi.constAlgHom R A B) a a = Function.const A a a
def
Pi.constAlgHom
(R : Type u_1)
(A : Type u_2)
(B : Type u_3)
[CommSemiring R]
[Semiring B]
[Algebra R B]
:
Function.const
as an AlgHom
. The name matches Pi.constRingHom
, Pi.constMonoidHom
,
etc.
Instances For
@[simp]
theorem
Pi.constRingHom_eq_algebraMap
(R : Type u_1)
(A : Type u_2)
[CommSemiring R]
:
Pi.constRingHom A R = algebraMap R (A → R)
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 (A → R)
instance
Function.algebra
{R : Type u_1}
(I : Type u_2)
(A : Type u_3)
[CommSemiring R]
[Semiring A]
[Algebra R A]
:
Algebra R (I → A)
A special case of Pi.algebra
for non-dependent types. Lean struggles to elaborate
definitions elsewhere in the library without this,
@[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)
:
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
.
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.symm (AlgEquiv.piCongrRight e) = AlgEquiv.piCongrRight fun i => AlgEquiv.symm (e i)
@[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.trans (AlgEquiv.piCongrRight e₁) (AlgEquiv.piCongrRight e₂) = AlgEquiv.piCongrRight fun i => AlgEquiv.trans (e₁ i) (e₂ i)