Structures · Algebra
AlgHomClass
AlgHomClass F R A B asserts F is a type of bundled algebra homomorphisms
from A to B.
- Defined in
- Mathlib.Algebra.Algebra.Hom
- Shape
- 4 explicit arguments · adds commutes
Extends1
Extended by0
Nothing extends this class yet.
Concrete types that are instances5
- AlgHom
- GradedAlgHom
- StarAlgHom
- ContinuousAlgHom
- Set.Elem
How is a type an instance?
Loading the hierarchy index…
Assumed by68
- Polynomial.aeval_algHom_apply
- IsIntegral.map
- AlgHomClass.commutes
- AlgHomClass.toAlgHom
- StarAlgHomClass.toStarAlgHom
- DirectLimit.Algebra.of
- AlgHom.apply_mem_spectrum
- AlgHom.spectrum_apply_subset
- StarAlgHom.equalizer
- DirectLimit.Algebra.lift
- Derivation.liftOfRightInverse
- GradedAlgHom.ofClass
- StarAlgHomClass.map_cfc
- AlgHomClass.unitization_injective
- Derivation.liftOfRightInverse_apply
- Unitization.algHom_ext''
- AlgHom.coe_coe
- StarAlgHom.adjoin_le_equalizer
- Derivation.liftOfSurjective
- Ideal.LiesOver.of_eq_comap
- AlgHomClass.toRingHom_toAlgHom
- AlgHomClass.unitization_injective'
- DirectLimit.Algebra.hom_ext
- IsSelfAdjoint.map_spectrum_real
- Unitization.algHom_ext
- StarAlgHomClass.ext_topologicalClosure
- StarAlgebra.elemental.starAlgHomClass_ext
- DirectLimit.map₀_algebraMap
- AlgHom.mem_resolventSet_apply
- StarAlgHom.ext_adjoin
- ContinuousMap.AlgHom.closure_ker_inter
- AlgHom.eqOn_sup
- StarAlgHom.coe_coe
- GradedAlgHom.coe_ofClass
- Ideal.comap_liesOver
- GradedAlgHom.toGradedRingHom_ofClass
- DirectLimit.Algebra.of_f
- DirectLimit.Algebra.lift_comp_of
- Derivation.liftOfSurjective.congr_simp
- AlgHom.ext_on_codisjoint
- AlgHomClass.toLinearMap_toAlgHom
- DirectLimit.Algebra.hom_ext_iff
- DirectLimit.Algebra.lift_of
- DirectLimit.instAlgebra
- WeakDual.Complex.instStarHomClass
- StarAlgHom.mem_equalizer
- DirectLimit.Algebra.of_apply
- AlgHomClass.linearMapClass
- DirectLimit.algebraMap_def
- AlgHom.norm_apply_le_self_mul_norm_one