Dummit and Foote의 추상대수 교과서에서 버그를 찾다
Finding a bug in Dummit and Foote's Abstract Algebra
Recurse Center에서의 두 번째 주에, 저자는 Dummit and Foote의 'Abstract Algebra' 교과서를 Rocq로 형식화하려고 시도했습니다. 첫 번째 증명 연습 문제에서 명제가 실제로는 거짓임을 발견했습니다. 공집합 도메인과 비어 있지 않은 공역을 가진 함수는 단사적이지만 왼쪽 역함수를 가질 수 없다는 반례를 제시합니다. 이는 종이로 연습할 때는 놓치기 쉬운 경계 사례로, 형식적 증명 도구를 사용함으로써 드러났습니다. 저자는 이 오류가 이미 교과서의 정오표에 등재되어 있음을 확인했습니다.
종이로 이 연습 문제를 풀었다면 이 경계 사례를 생각하지 못했을 것입니다. Rocq를 사용하고 있었기 때문에, 명제를 증명하려고 계속 벽에 부딪혔습니다.
HN 토론
36- generationP
이건 Dummit과 Foote에만 있는 게 아니라, 놓치기 너무 쉬운 거야. 이 결과를 서술하는 곳의 절반쯤에는 있을 거라고 짐작해. 몇 달 전에 내 강의 노트에서 고쳤지.
- Paracompact
상호작용식 증명 보조 도구가 수학적 사고를 단순히 느리게 만드는 게 아니라 개선하는 데 사용되는 걸 볼 때마다 마음이 따뜻해져요. 수년간这种东西을 사용해 본 결과, 프로토타이핑을 위한 증명 보조 도구의 고속 사용에 충분한 관심이 기울여지지 않고 있다고 생각합니다. 새로운 개념을 더듬는 데 쓰이는 휴지 조각을 완전히 대체할 수 있습니다.
- troethe
제안된 수정(즉, 'A가 inhabited이거나 B가 uninhabited여야 한다'는 요구)이 작동하긴 하지만, 이 특정한 경계 사례를 해결하기 위해 덧붙인 것처럼 보입니다. 더 우아한 해결책은 왼쪽 역함수의 정의를 함수 `g: B -> A`에서 함수 `g: f(A) -> A`로 완화하는 것이라고 생각합니다. 여기서 `f(A)`는 실제로 `f`에 의해 매핑되는 `B`의 부분집합, 즉 책의 함수 정의에 따르면 `f`에서 '오른쪽' 요소들의 집합입니다. 이것은 `f(A) = f({}) = {}`이고 (정확히 하나의) 함수 `g: {} -> {}`가 존재하므로, 이는 또한 자명하게 `f`의 왼쪽 역함수이기 때문에 경계 사례도 해결합니다. 여기서 진짜 문제는 `g: B -> A`라는 서술이 `g`가 `f`에 의해 생성될 수조차 없는 B의 요소들을 A로 다시 매핑하도록 불필요하게 요구했다는 점이며, 따라서 그러한 요소들은 왼쪽 역함수에 대해 무관해야 합니다.
- jonlong
여기에 덧붙이고 싶은 것은 왼쪽 소거( left-cancellation)의 속성이 정확히 단사성과 동등하다는 것입니다. 즉, `f : A -> B`가 단사 함수일 필요충분조건은 임의의 `g, h : C -> A`에 대해 `f o g = f o h`이면 `g = h`라는 것입니다. 만약 `A = {}`이면 `f`는 단사이고 왼쪽 소거 가능하며, 둘 다 공허하게 성립합니다. 이제 미묘한 점은 왼쪽 소거 가능성이 왼쪽 역함수를 갖는 것과 동등하지 않다는 것입니다. 정확히 지적된 이유 때문입니다. 이 관찰의 가치는 왼쪽 소거 가능성이 임의의 범주에서 작동하는 단사성의 유용한 일반화이며, 왼쪽 소거 가능한 사상은 단사 사상(monomorphism)이라고 불린다는 것입니다. 이미 단사 사상에 대해 알고 있다면 D&F의 연습 문제에 뭔가 '이상한' 점이 있다는 것을 알아차리기가 더 쉽습니다!
- hyperhello
두 입력이 같은 출력으로 매핑되지 않는다는 이유만으로 {}->를 단사라고 부르는 것은 공정하지 않다고 생각합니다. 그것은 공허합니다.