Documentation Verification Report

CharacterSpace

📁 Source: Mathlib/Topology/Algebra/Module/CharacterSpace.lean

Statistics

Metric	Count
Definitions `instFunLike`, `toAlgHom`, `toCLM`, `toNonUnitalAlgHom`, `characterSpace`, `gelfandTransform`	6
Theorems `apply_mem_spectrum`, `coe_coe`, `coe_toCLM`, `coe_toNonUnitalAlgHom`, `eq_set_map_one_map_mul`, `ext`, `ext_iff`, `ext_ker`, `instAlgHomClass`, `instContinuousLinearMapClass`, `instIsEmpty`, `instNonUnitalAlgHomClass`, `isClosed`, `toAlgHom_apply`, `union_zero`, `union_zero_isClosed`, `gelfandTransform_apply_apply`, `ker_isMaximal`	18
Total	24

WeakDual

Definitions

Name	Category	Theorems
`characterSpace` 📖	CompOp	40 math math: `Ideal.toCharacterSpace_apply_eq_zero_of_mem`, `CharacterSpace.instIsEmpty`, `StarAlgebra.elemental.characterSpaceToSpectrum_coe`, `CharacterSpace.apply_mem_spectrum`, `CharacterSpace.ext_iff`, `CharacterSpace.union_zero_isClosed`, `gelfandStarTransform_naturality`, `gelfandStarTransform_apply_apply`, `gelfandTransform_bijective`, `spectrum.gelfandTransform_eq`, `CharacterSpace.instNonUnitalAlgHomClass`, `CharacterSpace.continuousMapEval_bijective`, `gelfandStarTransform_symm_apply`, `CharacterSpace.homeoEval_naturality`, `StarAlgebra.elemental.bijective_characterSpaceToSpectrum`, `gelfandTransform_map_star`, `CharacterSpace.coe_coe`, `CharacterSpace.coe_toNonUnitalAlgHom`, `CharacterSpace.coe_toCLM`, `CharacterSpace.union_zero`, `CharacterSpace.compContinuousMap_apply`, `instNonemptyElemWeakDualComplexCharacterSpaceOfNontrivial`, `CharacterSpace.eq_set_map_one_map_mul`, `ker_isMaximal`, `CharacterSpace.norm_le_norm_one`, `CharacterSpace.mem_spectrum_iff_exists`, `gelfandTransform_apply_apply`, `CharacterSpace.continuousMapEval_apply_apply`, `CharacterSpace.equivAlgHom_coe`, `CharacterSpace.instAlgHomClass`, `gelfandTransform_isometry`, `CharacterSpace.compContinuousMap_comp`, `CharacterSpace.equivAlgHom_symm_coe`, `StarAlgebra.elemental.continuous_characterSpaceToSpectrum`, `CharacterSpace.exists_apply_eq_zero`, `CharacterSpace.compContinuousMap_id`, `CharacterSpace.isClosed`, `CharacterSpace.instCompactSpaceElemCharacterSpaceOfProperSpace`, `CharacterSpace.instStarHomClass`, `CharacterSpace.instContinuousLinearMapClass`
`gelfandTransform` 📖	CompOp	6 math math: `gelfandTransform_bijective`, `spectrum.gelfandTransform_eq`, `gelfandStarTransform_symm_apply`, `gelfandTransform_map_star`, `gelfandTransform_apply_apply`, `gelfandTransform_isometry`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`gelfandTransform_apply_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `Set.Elem` `WeakDual` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `characterSpace` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `instTopologicalSpaceWeakDual` `ContinuousMap.instFunLike` `AlgHom` `IsTopologicalSemiring.toContinuousAdd` `CommSemiring.toSemiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `SMulCommClass.continuousConstSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Algebra.toSMul` `Algebra.id` `Algebra.to_smulCommClass` `IsTopologicalSemiring.toContinuousMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `ContinuousMap.instSemiringOfIsTopologicalSemiring` `ContinuousMap.algebra` `AlgHom.funLike` `gelfandTransform` `CharacterSpace.instFunLike`	—	`IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `SMulCommClass.continuousConstSMul` `Algebra.to_smulCommClass` `IsTopologicalSemiring.toContinuousMul`
`ker_isMaximal` 📖	mathematical	—	`Ideal.IsMaximal` `Ring.toSemiring` `RingHom.ker` `Set.Elem` `WeakDual` `Semifield.toCommSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Algebra.toModule` `characterSpace` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Field.toCommRing` `CharacterSpace.instFunLike` `AlgHomClass.toRingHomClass` `Algebra.id` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CharacterSpace.instAlgHomClass` `IsDomain.to_noZeroDivisors` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `instIsDomain`	—	`RingHom.ker_isMaximal_of_surjective` `AlgHomClass.toRingHomClass` `CharacterSpace.instAlgHomClass` `IsDomain.to_noZeroDivisors` `instIsDomain` `AlgHomClass.commutes`

WeakDual.CharacterSpace

Definitions

Name	Category	Theorems
`instFunLike` 📖	CompOp	19 math math: `Ideal.toCharacterSpace_apply_eq_zero_of_mem`, `StarAlgebra.elemental.characterSpaceToSpectrum_coe`, `apply_mem_spectrum`, `ext_iff`, `gelfandStarTransform_apply_apply`, `instNonUnitalAlgHomClass`, `coe_coe`, `coe_toNonUnitalAlgHom`, `coe_toCLM`, `WeakDual.ker_isMaximal`, `mem_spectrum_iff_exists`, `WeakDual.gelfandTransform_apply_apply`, `continuousMapEval_apply_apply`, `equivAlgHom_coe`, `instAlgHomClass`, `equivAlgHom_symm_coe`, `exists_apply_eq_zero`, `instStarHomClass`, `instContinuousLinearMapClass`
`toAlgHom` 📖	CompOp	1 math math: `toAlgHom_apply`
`toCLM` 📖	CompOp	1 math math: `coe_toCLM`
`toNonUnitalAlgHom` 📖	CompOp	2 math math: `coe_toNonUnitalAlgHom`, `toAlgHom_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_mem_spectrum` 📖	mathematical	—	`Set` `Set.instMembership` `spectrum` `CommRing.toCommSemiring` `DFunLike.coe` `Set.Elem` `WeakDual` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Algebra.toModule` `Ring.toSemiring` `WeakDual.characterSpace` `instFunLike`	—	`AlgHom.apply_mem_spectrum` `instAlgHomClass`
`coe_coe` 📖	mathematical	—	`DFunLike.coe` `WeakDual` `NonUnitalNonAssocSemiring.toAddCommMonoid` `instFunLikeWeakDual` `Set` `Set.instMembership` `WeakDual.characterSpace` `Set.Elem` `instFunLike`	—	—
`coe_toCLM` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `ContinuousLinearMap.funLike` `toCLM` `Set.Elem` `WeakDual` `WeakDual.characterSpace` `instFunLike`	—	—
`coe_toNonUnitalAlgHom` 📖	mathematical	—	`DFunLike.coe` `NonUnitalAlgHom` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `MonoidHom.id` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Module.toDistribMulAction` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `NonUnitalAlgHom.instFunLike_1` `toNonUnitalAlgHom` `Set.Elem` `WeakDual` `WeakDual.characterSpace` `instFunLike`	—	—
`eq_set_map_one_map_mul` 📖	mathematical	—	`WeakDual.characterSpace` `CommRing.toCommSemiring` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `setOf` `WeakDual` `NonUnitalNonAssocSemiring.toAddCommMonoid` `DFunLike.coe` `instFunLikeWeakDual` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`Set.ext` `CanLift.prf` `Subtype.canLift` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `instAlgHomClass` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `instNonUnitalAlgHomClass` `zero_ne_one` `NeZero.one`
`ext` 📖	—	`DFunLike.coe` `Set.Elem` `WeakDual` `NonUnitalNonAssocSemiring.toAddCommMonoid` `WeakDual.characterSpace` `instFunLike`	—	—	`DFunLike.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `Set.Elem` `WeakDual` `NonUnitalNonAssocSemiring.toAddCommMonoid` `WeakDual.characterSpace` `instFunLike`	—	`ext`
`ext_ker` 📖	—	`RingHom.ker` `Set.Elem` `WeakDual` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Algebra.toModule` `Ring.toSemiring` `WeakDual.characterSpace` `CommSemiring.toSemiring` `instFunLike` `AlgHomClass.toRingHomClass` `Algebra.id` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instAlgHomClass`	—	—	`AlgHomClass.toRingHomClass` `instAlgHomClass` `ext` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `instNonUnitalAlgHomClass` `AlgHomClass.commutes` `sub_self` `sub_eq_zero` `RingHom.mem_ker`
`instAlgHomClass` 📖	mathematical	—	`AlgHomClass` `Set.Elem` `WeakDual` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `WeakDual.characterSpace` `CommSemiring.toSemiring` `Algebra.id` `instFunLike`	—	`instNonUnitalAlgHomClass` `NonUnitalAlgSemiHomClass.toMulHomClass` `mul_sub` `sub_eq_zero` `mul_one` `map_mul` `one_mul` `mul_eq_zero` `MulZeroClass.mul_zero` `Subtype.prop` `ContinuousLinearMap.ext` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `Algebra.algebraMap_eq_smul_one` `Algebra.algebraMap_self` `RingHom.id_apply` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `instContinuousLinearMapClass` `smul_eq_mul`
`instContinuousLinearMapClass` 📖	mathematical	—	`ContinuousLinearMapClass` `Set.Elem` `WeakDual` `NonUnitalNonAssocSemiring.toAddCommMonoid` `WeakDual.characterSpace` `CommSemiring.toSemiring` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `instFunLike`	—	`ContinuousLinearMap.map_add` `ContinuousLinearMap.map_smul` `ContinuousLinearMap.cont`
`instIsEmpty` 📖	mathematical	—	`IsEmpty` `Set.Elem` `WeakDual` `NonUnitalNonAssocSemiring.toAddCommMonoid` `WeakDual.characterSpace`	—	`Subtype.prop` `ContinuousLinearMap.ext` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass`
`instNonUnitalAlgHomClass` 📖	mathematical	—	`NonUnitalAlgHomClass` `Set.Elem` `WeakDual` `NonUnitalNonAssocSemiring.toAddCommMonoid` `WeakDual.characterSpace` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Module.toDistribMulAction` `Semiring.toModule` `instFunLike`	—	`instContinuousLinearMapClass` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `SemilinearMapClass.toAddHomClass` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `Subtype.prop`
`isClosed` 📖	mathematical	—	`IsClosed` `WeakDual` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `instTopologicalSpaceWeakDual` `WeakDual.characterSpace`	—	`eq_set_map_one_map_mul` `Set.setOf_and` `IsClosed.inter` `isClosed_eq` `WeakDual.eval_continuous` `continuous_const` `union_zero` `union_zero_isClosed`
`toAlgHom_apply` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `AlgHom.funLike` `toAlgHom` `MulActionHom.toFun` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MonoidHom.instFunLike` `MonoidHom.id` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Module.toDistribMulAction` `Algebra.toModule` `Semiring.toModule` `DistribMulActionHom.toMulActionHom` `NonUnitalAlgHom.toDistribMulActionHom` `toNonUnitalAlgHom`	—	—
`union_zero` 📖	mathematical	—	`Set` `WeakDual` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Set.instUnion` `WeakDual.characterSpace` `Set.instSingletonSet` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoidWeakDual` `setOf`	—	`le_antisymm` `MulZeroClass.zero_mul` `em`
`union_zero_isClosed` 📖	mathematical	—	`IsClosed` `WeakDual` `NonUnitalNonAssocSemiring.toAddCommMonoid` `instTopologicalSpaceWeakDual` `Set` `Set.instUnion` `WeakDual.characterSpace` `Set.instSingletonSet` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoidWeakDual`	—	`union_zero` `Set.setOf_forall` `isClosed_iInter` `isClosed_eq` `WeakDual.eval_continuous` `Continuous.mul`

---

← Back to Index