LeanAide documentation

LeanAide GPT-4 documentation

Module: Mathlib.Topology.Algebra.Module.CharacterSpace

`WeakDual.CharacterSpace.union_zero_isClosed` theorem WeakDual.CharacterSpace.union_zero_isClosed : ∀ (𝕜 : Type u_1) (A : Type u_2) [inst : CommSemiring 𝕜] [inst_1 : TopologicalSpace 𝕜] [inst_2 : ContinuousAdd 𝕜] [inst_3 : ContinuousConstSMul 𝕜 𝕜] [inst_4 : NonUnitalNonAssocSemiring A] [inst_5 : TopologicalSpace A] [inst_6 : Module 𝕜 A] [inst_7 : T2Space 𝕜] [inst_8 : ContinuousMul 𝕜], IsClosed (WeakDual.characterSpace 𝕜 A ∪ {0}) This theorem states that for any given type 𝕜 and A, where 𝕜 is a commutative semiring with a specified topological space structure, and it supports continuous addition, continuous scalar multiplication, and continuous multiplication, and A is a non-unital non-associative semiring with a topological space structure and is also a 𝕜-module, and 𝕜 is a Hausdorff space (T2 space), then the union of the character space of 𝕜 and A (denoted as `characterSpace 𝕜 A`) and the singleton set containing just the zero element is always a closed set in the weak dual of 𝕜 and A (denoted as `WeakDual 𝕜 A`). More concisely: The union of the character space of a commutative Hausdorff semiring 𝕜 with a topology supporting continuous operations, and a non-unital non-associative 𝕜-module A, and the singleton set containing the zero element is a closed set in the weak dual of 𝕜 and A.
`WeakDual.CharacterSpace.isClosed` theorem WeakDual.CharacterSpace.isClosed : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : CommRing 𝕜] [inst_1 : NoZeroDivisors 𝕜] [inst_2 : TopologicalSpace 𝕜] [inst_3 : ContinuousAdd 𝕜] [inst_4 : ContinuousConstSMul 𝕜 𝕜] [inst_5 : TopologicalSpace A] [inst_6 : Semiring A] [inst_7 : Algebra 𝕜 A] [inst_8 : Nontrivial 𝕜] [inst_9 : T2Space 𝕜] [inst_10 : ContinuousMul 𝕜], IsClosed (WeakDual.characterSpace 𝕜 A) This theorem states that, given a number of conditions on types `𝕜` and `A`, the character space forms a closed set in the weak dual of `𝕜` and `A`. The conditions include: `𝕜` is a commutative ring with no zero divisors, both `𝕜` and `A` are topological spaces, addition and scalar multiplication on `𝕜` are continuous, `𝕜` acts as a ring of scalars over `A` in a sense that `A` is a `𝕜`-algebra, `𝕜` is nontrivial, `𝕜` is a Hausdorff space, and multiplication on `𝕜` is continuous. More concisely: Given a commutative ring with no zero divisors 𝕜 that is a Hausdorff space and acts as a ring of scalars over a topological space A, the character space of 𝕜 on A is a closed subset of the weak dual of 𝕜 and A.