讨论室: 学术

关于此版块

不可编辑

这个页面是讨论数学问题的地方. 如果要讨论关于香蕉空间网站的问题, 请前往讨论室: 香蕉空间.

正则序列模极小素理想的高度

1
Fyx1123581347 (讨论贡献)

是 Noether 局部环, 是极大理想中正则序列. 设 任一极小素理想, 是否有 .

刚看了点代数拓扑和微分几何, 想问问李群和基本群能联系起来吗

2
Username (讨论贡献)

如题

Master (讨论贡献)

如果你想问的是 “基本群能否以自然的方式成为不离散的李群”, 答案是否定的.

由Yycdxp做出的摘要

把胖康托集 打到康托集 , 即可

HoshinoKoji (讨论贡献)

不严格递增, 为 Riemann 可积函数, 那么 是否一定 Riemann 可积?

注: 这道习题在 Lebesgue 可积性准则之前, 我手上只有 Darboux 的定义和一两个等价条件.

Yycdxp (讨论贡献)

这学期刚上实分析课, 对相关经典知识不是很熟悉请见谅.

我们知道 “胖” 康托集 (Wiki) , 它是一个闭集, 有着非零的测度. 因此, 它的示性函数不黎曼可积. 而康托集则有零测度, 示性函数黎曼可积. 考虑构造将胖康托集打到康托集的递增函数.

是胖康托集的构造中第 步后剩余的 个闭区间, 是康托集构造中的这 个区间. 定义 为如下的分段线性的连续递增函数: 将 中的区间依次线性打到 中的区间, 再将剩余部分线性连接. 容易发现在 上, , 且这部分函数值均不落在 中; 剩余部分的 .

因此这些 一致收敛到 , 它也是连续递增函数. 且由上述讨论可知, 若 , 则有 . 这即说明 ; 另一方面, 若记 为所有区间端点 ( 的稠密子集) , 则由构造 . 因此 , 根据连续性即得到 .

考虑 是 Cantor 集的示性函数, 则 黎曼可积, 且 不是黎曼可积函数.

如有错误请指出, 谢谢

Yycdxp (讨论贡献)

Update: 简要证明一下胖康托集的示性函数 的不可积性.

设第 步删除的单个小区间长度为 , 其中 ( 即为常规 Cantor 集) . 则我们有 的长度和: 它有一个与 无关的下界 .

对任意 , 取 充分大使得 . 取 的间距为 的等距划分. 由于胖康托集 的补集是稠密集 (因为 无处稠密) , 我们知道任何一个开区间上 的下界都是 . 因此达布下和满足

考虑用 估计 的达布上和. 对于每个划分的开区间 , 若有 , 即 , 由于第 步后扣除的开区间长度均 , 可知 落在第 步及以前扣除的开区间中, 也即 , 因此 .

因而我们得到又因为 , 显然上式有 成立. 因此我们得到

从而我们知道, 对任意 , 总存在划分 使得 , 其中 是固定的常数. 从而 不是黎曼可积的.

HoshinoKoji (讨论贡献)

非常感谢!

什么样的形式系统可以从内部避免悖论?

5
大耳白兔 (讨论贡献)

大家应该知道哥德尔的第一第二不完全性定理, 有的形式系统无法从内部推理避免悖论, 但是可以从外部推理避免悖论. 是否存在一些形式系统, 无法用任何推理避免悖论?

大耳白兔 (讨论贡献)

避免悖论是否存在统一的理论?

大耳白兔 (讨论贡献)

避免悖论是否存在统一的理论, 或一般性的算法?

Trebor (讨论贡献)

还是先读一些数理逻辑的基础书, 思而不学则殆.

Ice1000 (讨论贡献)

以悖论命题作为公理的形式系统就无法用任何推理避免悖论

n 为奇数时, 证明 AB’+A’B 为奇异阵

5
江谨 (讨论贡献)

设 A, B 为 n 阶方阵, 满足 . 证明: 若 是奇数, 则 为奇异阵.

Master (讨论贡献)

’ 表示伴随矩阵吗? 如果是的话只需注意到矩阵秩小于 则其伴随矩阵为 .

江谨 (讨论贡献)

‘表示转置

秋逸笛 (讨论贡献)

. 如果 可逆那么 .

.

因为 是奇数, 所以 . 同理 ; 故 (这里利用西尔维斯特秩不等式), 矛盾.

江谨 (讨论贡献)

看懂了, 感谢

请问在 f 一阶可导的情况下怎么证明.

2
江谨 (讨论贡献)

在 [a,b] 上可导, , . 证明

秋逸笛 (讨论贡献)

https://b23.tv/8zEt8F6

是否可以用某种全本质满函子构造范畴的局部化?

2
从周 (讨论贡献)

起因是我正在看 Sophie Morel 的同调代数讲义 (http://morel.perso.math.cnrs.fr/notes540.pdf). 其中的 Proposition V.2.1.6,p156 提到:

是一个全本质满 (full and essentially surjective) 函子, 是由 中的态射组成的集合. 若存在 中的态射组成的集合 , 使得 . 设 的局部化, 则 的局部化.

讲义中已经证明了局部化满足的三条性质中的两条, 即 中的态射映到 中的同构态射; 并且对于另一个范畴 和函子 , 存在双射 .

但是没有证明 满足局部化的泛性质.

我的想法是, 设 的局部化. 利用局部化的泛性质得到一个函子 , 使得有函子的自然同构 , 然后再证明 是范畴等价. 但是我想不出怎么说明 是范畴等价.

我感觉 是一个很关键的非平凡的条件, 但我不知道怎么用上它.

烦请各位前辈不吝赐教.

从周 (讨论贡献)

情况有变, 这个命题是错的, 只需令 都是只有一个对象的 groupoid 即可.

Leynpid (讨论贡献)

Let where are Banach spaces. Let be the projections and be the inclusion maps. Under what conditions does a continuous linear map have a continuous inverse?

If or , we know that is invertible iff , i.e. . But for general Banach spaces, what do we require about the maps ? Do we have a similar result?

如何在计算机科学中应用类型论和范畴论?

14
由Ice1000做出的摘要

已经回答

Master (讨论贡献)

如题, 我好奇计算机学家为何要考虑类型论和范畴论, 它反映了计算机科学中何种对象的数学结构?

Ice1000 (讨论贡献)

这是个很好的问题. 首先, 计算机科学 (广义) 很难应用类型论和范畴论, 实际上是类型论的研究中有大量对范畴论的应用, 而类型论本身是编程语言理论的基础理论. 在我看来 (前面部分应该是成立的, 从现在开始是我的个人想法) , 类型论之于对编程语言学家来说有点类似集合论之于数学家: 大家都接受过相关的基础教育, 理解这些理论的重要性, 但该不了解领域的前沿研究. 数学家中也有专门研究集合论的人, 同样, 编程语言学家中也有研究类型论的人, 只是后者的比例相对高一些.

因此, 根据我的个人观点, 这个问题的题设不成立, 计算机科学家基本不考虑类型论和范畴论. 下面我说说我为什么关心类型论和范畴论.

Ice1000 (讨论贡献)

编程语言是非常常用的计算机工具, 这个是计算机科学家比较关心的, 并且编程语言对于程序员的思维影响非常深刻, 比如常年使用 Java 的人会认为子类型多态是天经地义的, 而长时间使用 Rust 的人脑子里会对程序进行线性逻辑式的建模, 长时间使用 typescript 的话会内化结构化类型的思想, 等等. 拥有这些不同的思想对程序员来说, 并不影响她们完成编程任务, 因此大部分程序员都对这些想法停留在「知道有这些概念, 但不深究, 也不感兴趣」的程度. 在我看来, 有这么多编程语言的原因, 就是不同的人对理想的编程方式有不同的看法, 而这些想法往往是互斥的. 如果你希望程序能随时中断执行、跨函数跳转, 这当然听起来没有问题, 但也有的人希望程序在每个函数结尾自动清理局部内存, 这两者就冲突了——跳出当前函数就没有办法进行内存清理了. 因此会有人互相看不惯, 就会不断地产生新的语言.

我最早写程序的时候, 就感受到了这一点, 因此想要探索这些思想的本质、想要自己设计出完美的编程语言 (实际上是不存在的) , 所以就接触到了编程语言理论的研究: 这个理论将编程语言抽象成各种语言特性的组合, 并重点研究具体的语言特性、语言特性之间的交互, 因此熟悉编程语言理论的人能准确判断「将什么样的语言特性组合起来是能工作的」, 并且设计出好用的编程语言. 我觉得这很酷, 但随后就接触到了类型论: 它不研究具体的语言特性了, 而是直接发明了更底层的代数结构, 并认为编程语言就是这个代数结构在计算机中的模拟. 这样的代数结构有很多, 比如广义代数理论、概括范畴偏等关系等. 这样的建模方式有很多局限性, 但它却给理解编程语言的方式带来了全新的直觉, 比如将计算视为一种单子、将类型视为一个范畴里的对象等等. 这就是类型论研究者关心范畴论的地方.

除此之外, 现代的编程语言研究除了大规模的工程问题 (提升计算性能、支持更多架构等) 和怎么设计好用的语言特性 (全凭审美和感觉) 这两个发表论文比较看脸的方向之外, 就是类型论了, 我觉得后者对 career 来说比较靠谱. 我个人也对编程工具比较感兴趣, 但学术界并不 appreciate 这些, 所以就是 sidekick.

Master (讨论贡献)

计算视为单子具体指什么呢?

Ice1000 (讨论贡献)

令 Computed : Set → Set 作为一种标记计算的函数, 输入一个表达式的集合, 过滤掉里面那些会因为计算而变成其它东西的表达式, 比如 1 + 1 就会被删掉, 因为它运行后就是 2 了. 这里 Computed 就是一个 Monad. 不知道这么说能不能表达出它里面微妙的意思, 但大概就是过滤两遍和只过滤一遍效果是一样的, 而且 “把一个没化简的东西拿去化简” 本身是一个可重复而不可逆的过程, 这对应了单子的那两个自然变换

编辑: 经过后面的讨论, 这个说法是有问题的.

Trebor (讨论贡献)

计算并不是值到值的映射 (如果是, 这称作纯计算) . 一次计算可能会产生异常, 生成随机数, 读取磁盘文件等. 单子这个数学结构可以刻画绝大部分计算的概念.

单子是一个自函子 上配备一些结构. 是所有类型的范畴, 态射是函数. 表示一次计算, 产生类型 的值. 单子配备了自然变换 , 表示不做任何计算直接返回输入.

表示两个输入值, 经过一些计算, 产生新的值的函数. 单子配备了一个运算将这两次计算连起来得到 , 满足自然性. 我们要求它们满足单位律和结合律.

编程语言里面可以直接提供一个单子 (类似公理, 看不到这个单子内部的定义) 与一些计算 , 让程序员使用. 程序员也可以自己定义单子, 如 表示可能失败的运算, 并上的这个点表示失败; 表示带有一个状态的计算, 输入一个起始状态, 输出计算结果与结束状态, 等.

Haskell 与 F 等语言都用单子组织程序. 不过它们的教材普遍呈现去范畴化的趋势, 因为程序员大部分情况下不喜欢 fancy 的语言, 要把定义解包成不用范畴的话说.

Ice1000 (讨论贡献)

我说的就是纯计算, 类似 Andrew Pitts 写的那个 categorical logic 里的 computation type, 单子表示 effect 是另一种应用了. 这种应用一般不验证单子的交换条件所以我没写

Trebor (讨论贡献)

过滤两遍和只过滤一遍效果是一样的

这很强烈地暗示应该有一个自然同构, 而不是自然变换, 你确定这是你想说的吗?

Computation type 实际上是一样的思想, 注意我没有说 “副作用”, 消耗时间也可以看作是计算的一种表现.

Ice1000 (讨论贡献)

你说的有道理, 很显然这里不是自然同构的关系, 我觉得那个表示计算的 Monad 确实是用来标记的, 但过滤表达式这个想法是我为了具体化这个过程临时想的. 这样一看确实有问题.

Master (讨论贡献)

“编程语言里面可以直接提供一个单子” 这句话怎么理解呢?

Trebor (讨论贡献)

你是想问编程语言的设计者如何实现这个功能, 还是编程语言的使用者如何使用这个功能

Master (讨论贡献)

大概是都想问.

Trebor (讨论贡献)

使用者的视角, 这就是一个提前定义好现成的单子, 和其他单子使用上没有区别. 实现上那就是正常的魔法, 一般都没什么特别非平凡的

Ice1000 (讨论贡献)

我觉得其实就是指提供一个满足单子律的语言特性. 也可能不满足, 只是像一个单子. 比如修改变量的能力其实就属于一种单子

关于数学分析讲义中证明用 Dedekind 分割构造的实数满足 “对于任意的 X,Y∈R, 存在唯一的 Z∈R, 使得 X+Z=Y” 的疑问

4
Afheah (讨论贡献)

大家好, 我是数学系的新生, 所以可能问的问题有点傻, 还请大家耐心帮助我, 非常感谢!

在香蕉空间的数学分析讲义中, (https://www.bananaspace.org/wiki/讲义: 数学分析/实数的构造:_Dedekind_分割) , 我对其中加法构造的 “(F4) 对任意的 Dedekind 分割 X 和 Y, 存在唯一的 Z∈R, 使得 X+Z=Y” 定理的证明存在疑惑. 在证明 Y⊂X+Z 时, 我们有 y<y , x<x’. 为什么可以由技术性引理得到 x′−x<y −y 呢?

也就是说, x′−x>0,y −y>0, 为什么可以得到总存在一对 x 和 x‘, 保证他们的差小于 y −y 呢?

谢谢大家. ​

BCJ (讨论贡献)

引理说明对任意正整数 , 可以找到 使得 . 由于 是正有理数, 存在正整数 , 使得 .

此帖子已被 “Afheah” 隐藏