Homomorphisms of R
-algebras #
This file defines bundled homomorphisms of R
-algebras.
Main definitions #
AlgHom R A B
: the type ofR
-algebra morphisms fromA
toB
.Algebra.ofId R A : R →ₐ[R] A
: the canonical map fromR
toA
, as anAlgHom
.
Notations #
A →ₐ[R] B
:R
-algebra homomorphism fromA
toB
.
Defining the homomorphism in the category R-Alg.
Instances For
Defining the homomorphism in the category R-Alg.
Equations
- «term_→ₐ_» = Lean.ParserDescr.trailingNode `«term_→ₐ_» 25 26 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " →ₐ ") (Lean.ParserDescr.cat `term 25))
Instances For
Defining the homomorphism in the category R-Alg.
Equations
- One or more equations did not get rendered due to their size.
Instances For
AlgHomClass F R A B
asserts F
is a type of bundled algebra homomorphisms
from A
to B
.
Instances
Equations
- ⋯ = ⋯
Turn an element of a type F
satisfying AlgHomClass F α β
into an actual
AlgHom
. This is declared as the default coercion from F
to α →+* β
.
Equations
- ↑f = { toFun := ⇑f, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }
Instances For
Equations
- ⋯ = ⋯
See Note [custom simps projection]
Equations
- AlgHom.Simps.apply f = ⇑f
Instances For
If a RingHom
is R
-linear, then it is an AlgHom
.
Equations
- AlgHom.mk' f h = { toFun := ⇑f, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }
Instances For
Composition of algebra homeomorphisms.
Equations
- φ₁.comp φ₂ = { toRingHom := φ₁.comp ↑φ₂, commutes' := ⋯ }
Instances For
Promote a LinearMap
to an AlgHom
by supplying proofs about the behavior on 1
and *
.
Equations
- AlgHom.ofLinearMap f map_one map_mul = { toFun := ⇑f, map_one' := map_one, map_mul' := map_mul, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }
Instances For
AlgebraMap
as an AlgHom
.
Equations
- Algebra.ofId R A = { toRingHom := algebraMap R A, commutes' := ⋯ }
Instances For
This is a special case of a more general instance that we define in a later file.
Equations
- ⋯ = ⋯
Equations
Each element of the monoid defines an algebra homomorphism.
This is a stronger version of MulSemiringAction.toRingHom
and
DistribMulAction.toLinearMap
.
Equations
- MulSemiringAction.toAlgHom R A m = { toFun := fun (a : A) => m • a, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }