1
Introduction
2
The Quotient Isomorphism
▶
2.1
Degree Bound via Cayley–Hamilton
2.2
The Isomorphism via Orzech’s Property
3
The Étale Case (Lemma 3.2)
▶
3.1
Generator Descends to Residue Field
3.2
Rank Equality across Residue Fields
3.3
Minimal Polynomial Descends to Residue Field
3.4
Unit Derivative Condition
3.5
Existence of Generator (Nakayama Argument)
4
Converse: Monogenic with Unit Derivative Implies Étale
5
The Partially Étale Case (Lemma 3.1)
▶
5.1
Sub-lemmas
5.2
Nakayama Helpers
5.3
Principal Adjustment Lemma
5.4
Main Theorem: Lemma 3.1
6
Plan for Mathlib PRs
▶
6.1
PR 1: Quotient Isomorphism without Integrally Closed
▶
Declarations
File placement
Namespace and naming
Required imports (for the declarations)
Proof adjustments for Mathlib style
Potential issues
6.2
PR 2: Residue Field Properties for Étale Local Extensions
▶
Declarations
File placement
Namespace
Required imports
Proof structure
Potential issues
6.3
PR 3: Finite Étale Local Extensions are Monogenic
▶
Declarations
File placement
Namespace
Required imports
Proof structure
Potential issues
6.4
PR 4: Converse — Standard Étale from Unit Derivative
▶
Declarations
File placement
Namespace
Required imports
Proof structure
Potential issues
6.5
PR 5: Nakayama Helpers and Partially Étale Case (Lemma 3.1)
▶
Sub-PR 5a: Height-One Primes in UFDs are Principal
Sub-PR 5b: Taylor Expansion for Polynomial Evaluation
Sub-PR 5c: Maximal Ideal Decomposition and Quotient Lifting
Sub-PR 5d: Main Theorem (Lemma 3.1)
6.6
Dependency Graph Summary
Dependency graph
Monogenic Extensions of Local Rings
Bianca Viray, Bryan Boehnke, Grant Yang, George Peykanu, Tianshuo Wang
1
Introduction
2
The Quotient Isomorphism
2.1
Degree Bound via Cayley–Hamilton
2.2
The Isomorphism via Orzech’s Property
3
The Étale Case (Lemma 3.2)
3.1
Generator Descends to Residue Field
3.2
Rank Equality across Residue Fields
3.3
Minimal Polynomial Descends to Residue Field
3.4
Unit Derivative Condition
3.5
Existence of Generator (Nakayama Argument)
4
Converse: Monogenic with Unit Derivative Implies Étale
5
The Partially Étale Case (Lemma 3.1)
5.1
Sub-lemmas
5.2
Nakayama Helpers
5.3
Principal Adjustment Lemma
5.4
Main Theorem: Lemma 3.1
6
Plan for Mathlib PRs
6.1
PR 1: Quotient Isomorphism without Integrally Closed
Declarations
File placement
Namespace and naming
Required imports (for the declarations)
Proof adjustments for Mathlib style
Potential issues
6.2
PR 2: Residue Field Properties for Étale Local Extensions
Declarations
File placement
Namespace
Required imports
Proof structure
Potential issues
6.3
PR 3: Finite Étale Local Extensions are Monogenic
Declarations
File placement
Namespace
Required imports
Proof structure
Potential issues
6.4
PR 4: Converse — Standard Étale from Unit Derivative
Declarations
File placement
Namespace
Required imports
Proof structure
Potential issues
6.5
PR 5: Nakayama Helpers and Partially Étale Case (Lemma 3.1)
Sub-PR 5a: Height-One Primes in UFDs are Principal
Sub-PR 5b: Taylor Expansion for Polynomial Evaluation
Sub-PR 5c: Maximal Ideal Decomposition and Quotient Lifting
Sub-PR 5d: Main Theorem (Lemma 3.1)
6.6
Dependency Graph Summary