Commit 2023-07-18 21:46 15ef30fa

View on Github →

feat: define NonUnitalStarSubalgebras and develop basic API (#5537) This continues the non-unital-ization of mathlib This PR also redefines StarSubalgebra.centralizer so that it no longer requires the set s provided to be closed under star, and instead the carrier is just the Set.centralizer (s ∪ star s). Consequently, this changes some things in von Neumann algebras, where we now need to see that Set.centralizer (↑S ∪ star ↑S) = Set.centralizer ↑S, where S is a StarSubalgebra. Therefore we add the simp lemma StarMemClass.star_coe_eq.

depends on: #5151
depends on: #5512

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Star/Basic.lean

Created Mathlib/Algebra/Star/Center.lean

added theorem Set.star_mem_center

added theorem Set.star_mem_centralizer'

added theorem Set.star_mem_centralizer

Created Mathlib/Algebra/Star/NonUnitalSubalgebra.lean

added def NonUnitalStarAlgHom.codRestrict

added theorem NonUnitalStarAlgHom.coe_codRestrict

added theorem NonUnitalStarAlgHom.coe_range

added def NonUnitalStarAlgHom.equalizer

added theorem NonUnitalStarAlgHom.injective_codRestrict

added theorem NonUnitalStarAlgHom.mem_equalizer

added theorem NonUnitalStarAlgHom.mem_range

added theorem NonUnitalStarAlgHom.mem_range_self

added def NonUnitalStarAlgHom.rangeRestrict

added theorem NonUnitalStarAlgHom.range_comp

added theorem NonUnitalStarAlgHom.range_comp_le_range

added theorem NonUnitalStarAlgHom.subtype_comp_codRestrict

added def NonUnitalStarAlgebra.adjoin

added theorem NonUnitalStarAlgebra.adjoin_eq_starClosure_adjoin

added theorem NonUnitalStarAlgebra.adjoin_le

added theorem NonUnitalStarAlgebra.adjoin_le_iff

added theorem NonUnitalStarAlgebra.adjoin_toNonUnitalSubalgebra

added theorem NonUnitalStarAlgebra.coe_bot

added theorem NonUnitalStarAlgebra.coe_iInf

added theorem NonUnitalStarAlgebra.coe_inf

added theorem NonUnitalStarAlgebra.coe_sInf

added theorem NonUnitalStarAlgebra.coe_top

added theorem NonUnitalStarAlgebra.comap_top

added theorem NonUnitalStarAlgebra.eq_top_iff

added theorem NonUnitalStarAlgebra.iInf_toNonUnitalSubalgebra

added theorem NonUnitalStarAlgebra.inf_toNonUnitalSubalgebra

added theorem NonUnitalStarAlgebra.map_bot

added theorem NonUnitalStarAlgebra.map_sup

added theorem NonUnitalStarAlgebra.map_top

added theorem NonUnitalStarAlgebra.mem_bot

added theorem NonUnitalStarAlgebra.mem_iInf

added theorem NonUnitalStarAlgebra.mem_inf

added theorem NonUnitalStarAlgebra.mem_sInf

added theorem NonUnitalStarAlgebra.mem_sup_left

added theorem NonUnitalStarAlgebra.mem_sup_right

added theorem NonUnitalStarAlgebra.mem_top

added theorem NonUnitalStarAlgebra.mul_mem_sup

added theorem NonUnitalStarAlgebra.range_id

added theorem NonUnitalStarAlgebra.range_top_iff_surjective

added theorem NonUnitalStarAlgebra.sInf_toNonUnitalSubalgebra

added theorem NonUnitalStarAlgebra.self_mem_adjoin_singleton

added theorem NonUnitalStarAlgebra.star_self_mem_adjoin_singleton

added theorem NonUnitalStarAlgebra.star_subset_adjoin

added theorem NonUnitalStarAlgebra.subset_adjoin

added theorem NonUnitalStarAlgebra.toNonUnitalSubalgebra_bot

added theorem NonUnitalStarAlgebra.toNonUnitalSubalgebra_eq_top

added def NonUnitalStarAlgebra.toTop

added theorem NonUnitalStarAlgebra.top_toNonUnitalSubalgebra

added def NonUnitalStarSubalgebra.center

added theorem NonUnitalStarSubalgebra.center_eq_top

added theorem NonUnitalStarSubalgebra.center_toNonUnitalSubalgebra

added def NonUnitalStarSubalgebra.centralizer

added theorem NonUnitalStarSubalgebra.centralizer_le

added theorem NonUnitalStarSubalgebra.centralizer_univ

added theorem NonUnitalStarSubalgebra.coe_center

added theorem NonUnitalStarSubalgebra.coe_centralizer

added theorem NonUnitalStarSubalgebra.coe_comap

added theorem NonUnitalStarSubalgebra.coe_copy

added theorem NonUnitalStarSubalgebra.coe_iSup_of_directed

added theorem NonUnitalStarSubalgebra.coe_map

added theorem NonUnitalStarSubalgebra.coe_prod

added theorem NonUnitalStarSubalgebra.coe_smul

added theorem NonUnitalStarSubalgebra.coe_toNonUnitalSubalgebra

added theorem NonUnitalStarSubalgebra.coe_toNonUnitalSubring

added def NonUnitalStarSubalgebra.comap

added theorem NonUnitalStarSubalgebra.copy_eq

added theorem NonUnitalStarSubalgebra.ext

added theorem NonUnitalStarSubalgebra.gc_map_comap

added theorem NonUnitalStarSubalgebra.iSupLift_comp_inclusion

added theorem NonUnitalStarSubalgebra.iSupLift_inclusion

added theorem NonUnitalStarSubalgebra.iSupLift_mk

added theorem NonUnitalStarSubalgebra.iSupLift_of_mem

added def NonUnitalStarSubalgebra.inclusion

added theorem NonUnitalStarSubalgebra.inclusion_inclusion

added theorem NonUnitalStarSubalgebra.inclusion_injective

added theorem NonUnitalStarSubalgebra.inclusion_mk

added theorem NonUnitalStarSubalgebra.inclusion_right

added theorem NonUnitalStarSubalgebra.inclusion_self

added def NonUnitalStarSubalgebra.map

added theorem NonUnitalStarSubalgebra.map_id

added theorem NonUnitalStarSubalgebra.map_injective

added theorem NonUnitalStarSubalgebra.map_le

added theorem NonUnitalStarSubalgebra.map_map

added theorem NonUnitalStarSubalgebra.map_mono

added theorem NonUnitalStarSubalgebra.map_toNonUnitalSubalgebra

added theorem NonUnitalStarSubalgebra.mem_carrier

added theorem NonUnitalStarSubalgebra.mem_center_iff

added theorem NonUnitalStarSubalgebra.mem_centralizer_iff

added theorem NonUnitalStarSubalgebra.mem_comap

added theorem NonUnitalStarSubalgebra.mem_map

added theorem NonUnitalStarSubalgebra.mem_prod

added theorem NonUnitalStarSubalgebra.mem_toNonUnitalSubalgebra

added theorem NonUnitalStarSubalgebra.mem_toNonUnitalSubring

added def NonUnitalStarSubalgebra.prod

added theorem NonUnitalStarSubalgebra.prod_inf_prod

added theorem NonUnitalStarSubalgebra.prod_mono

added theorem NonUnitalStarSubalgebra.prod_toNonUnitalSubalgebra

added theorem NonUnitalStarSubalgebra.prod_top

added theorem NonUnitalStarSubalgebra.range_val

added def NonUnitalStarSubalgebra.toNonUnitalSubalgebra'

added theorem NonUnitalStarSubalgebra.toNonUnitalSubalgebra_inj

added theorem NonUnitalStarSubalgebra.toNonUnitalSubalgebra_injective

added theorem NonUnitalStarSubalgebra.toNonUnitalSubalgebra_le_iff

added theorem NonUnitalStarSubalgebra.toNonUnitalSubalgebra_subtype

added theorem NonUnitalStarSubalgebra.toNonUnitalSubalgebra_toNonUnitalStarSubalgebra

added def NonUnitalStarSubalgebra.toNonUnitalSubring

added theorem NonUnitalStarSubalgebra.toNonUnitalSubring_inj

added theorem NonUnitalStarSubalgebra.toNonUnitalSubring_injective

added theorem NonUnitalStarSubalgebra.toSubring_subtype

added theorem NonUnitalStarSubalgebra.val_inclusion

added structure NonUnitalStarSubalgebra

added theorem NonUnitalStarSubalgebraClass.coeSubtype

added def NonUnitalStarSubalgebraClass.subtype

added theorem NonUnitalSubalgebra.coe_star

added theorem NonUnitalSubalgebra.coe_toNonUnitalStarSubalgebra

added theorem NonUnitalSubalgebra.mem_star_iff

added theorem NonUnitalSubalgebra.mem_toNonUnitalStarSubalgebra

added def NonUnitalSubalgebra.starClosure

added theorem NonUnitalSubalgebra.starClosure_eq_adjoin

added theorem NonUnitalSubalgebra.starClosure_le

added theorem NonUnitalSubalgebra.starClosure_le_iff

added theorem NonUnitalSubalgebra.starClosure_mono

added theorem NonUnitalSubalgebra.starClosure_toNonunitalSubalgebra

added theorem NonUnitalSubalgebra.star_adjoin_comm

added theorem NonUnitalSubalgebra.star_mem_star_iff

added theorem NonUnitalSubalgebra.star_mono

added def NonUnitalSubalgebra.toNonUnitalStarSubalgebra

added theorem NonUnitalSubalgebra.toNonUnitalStarSubalgebra_toNonUnitalSubalgebra

added theorem StarAlgEquiv.ofInjective'_apply

added def StarAlgEquiv.ofLeftInverse'

added theorem StarAlgEquiv.ofLeftInverse'_apply

added theorem StarAlgEquiv.ofLeftInverse'_symm_apply

Modified Mathlib/Algebra/Star/Pointwise.lean

added theorem StarMemClass.star_coe_eq

Modified Mathlib/Algebra/Star/Subalgebra.lean

deleted theorem Set.star_mem_centralizer

modified def StarSubalgebra.centralizer

modified theorem StarSubalgebra.centralizer_le

modified theorem StarSubalgebra.coe_centralizer

added theorem StarSubalgebra.coe_mk

modified theorem StarSubalgebra.mem_centralizer_iff

Modified Mathlib/Analysis/VonNeumannAlgebra/Basic.lean

added theorem VonNeumannAlgebra.coe_mk

added theorem VonNeumannAlgebra.coe_toStarSubalgebra

modified def VonNeumannAlgebra.commutant