Formalization of Naganori Yamaguchi's Extension of solvable coverings across horizontal divisors over the integers, using the numbering of arXiv v1. Includes the geometric, group-theoretic and representation-theoretic ar…
Extension of solvable coverings
Library documentation
Extension of solvable coverings
Formalization of Naganori Yamaguchi's Extension of solvable coverings across horizontal divisors over the integers, using the numbering of arXiv v1. Includes the geometric, group-theoretic and representation-theoretic arguments.
These are the geometric definitions used in Yamaguchi, arXiv:2610.02948v1: reduced prime components of an effective Cartier divisor, their generic points, horizontality over Spec ℤ, and geometric integrality after finite…
定理 2.5 の幾何学的な段階。開正規部分群に対応する有限 étale 被覆とその引き戻しは EFG の OpenNormalPullbackModel から実際に構成する。補題 2.1 と 2.4 によって 引き戻し全体が連結であることを示し、選んだ連結成分と境界補集合を同一視する。 その補集合に補題 2.1 を適用し、任意の有限離散可換群への連続準同型が局所的な核を 消すことを証明する。基本群の射の合成に伴う共役は、単位元に送られる…
The branch prime selected by the normal-crossings construction lies over the original component generic point. Its geometric point on every further prime localization has the same algebraically closed field and the same…
A prescribed normalization point is transported to the discrete valuation stalk at the component's generic point. The connected component through that point supplies a genuine finite Galois extension of the local fractio…
A cover which extends over the ambient scheme has trivial geometric-point inertia at every boundary component. This proves one inclusion in the kernel formula of Lemma 1.1 without requiring ambient normality or integrali…
A height-one prime containing the Cartier ideal represents a generic point of an actual component of the boundary. The previously constructed étale normalization over that component's DVR therefore remains étale after pa…
ここでは実際の有限 étale 被覆を相対正規化し、その上の幾何点を固定する被覆自己同型の 部分群を定義する。位相的な点を固定する分解群とは異なり、幾何点からの射の等式を 要求する。自己同型の延長と群公理は正規化の普遍性から証明する。 台のスキーム全体の整性・正規性は仮定しない。 原稿の惰性群は、境界成分一般点の strict henselization の分数体の基本群の像である。 BoundaryStrictInertia が共通の…
The original boundary-unramified condition makes the normalization of every pointed Galois fraction-stalk component étale over the DVR stalk. All point and action comparisons are supplied by the actual cover construction…
A normalized geometric point of a component over the fraction stalk maps to the original cover's normalization. Equivariance and injectivity of the canonical component quotient transfer the original boundary condition to…
The normalized local Galois components cover the normalization of the whole fraction-field pullback. The actual Cartier-complement pullback and normalization-localization isomorphisms then identify this with the base cha…
The principal complement square identifies the actual pulled-back finite cover. Normalization commutes with the stalk base change, and normalized component inclusions are open immersions. These comparisons transport the…
Choose an actual local Cartier equation. Every connected Galois component of the pulled-back cover has etale normalization by purity: height-one etaleness comes from the original boundary components, and regularity is tr…
A finite Galois quotient killing the transported strict inertia generators has trivial action on every strict generic fiber. The actual strict-local normalization criterion supplies etaleness at each component stalk. Pur…
At a boundary component use its canonical residue-field geometric point and the actual geometric etale stalk. The shared point construction produces a point of the original normalization over that very geometric point, f…
For each boundary component we use its actual strict-Henselian generic morphism and the canonical geometric point of its fraction field. All isomorphisms from the resulting geometric fiber functor to the specified common…
The shared component generic point and the manuscript component point agree by the proved generic-point equation. Transporting the actual local-ring results along that equation gives the domain and DVR structures used he…
Purity supplies finite etaleness over every boundary stalk. Affine spreading then makes the actual relative normalization finite etale globally. Its restriction is the original cover, so the finite-cover kernel criterion…
Canonical aggregate for Yamaguchi26SolvableCoverings.GroupTheory.
連続全射 f : G → Q に対し、Q の任意の開正規部分群 H の逆像上で アーベル化の写像が単射ならば、ker f は位相的完全である。 証明では有限商 q : G → S ごとに N = q(ker f) を作り、S/N への写像を Q に降ろす。その核を H とすると、局所アーベル化の単射性から N = [N,N] が従う。最後に閉集合への所属を有限商で検出して核の完全性を得る。 ここにはスキームに関する仮定や結論を新しい f…
I 進位相を持つ可換環 A が I 進分離的であるとする。 交換子部分群が稠密な位相群 G から GLₙ(A) への連続表現が I を法として 自明なら、表現自体が自明である。 証明は合同核の pro-p 性を仮定せず、行列の差を直接計算する。 I^r を法として単位行列となる二つの行列は、r ≥ 1 のとき I^(r+1) を法として 可換である。これは二つの差の積の成分が I^(2r) ⊆ I^(r+1) に入るためである。 したが…
Canonical aggregate for Yamaguchi26SolvableCoverings.Representations.
Source: Yamaguchi, arXiv:2610.02948v1, Lemma 1.1. X は連結な局所 Noether スキーム、D は X 上の有効 Cartier 因子、 U = X ∖ Supp(D) とする。D の台の各点で X が正則であることを仮定する。 この補題では D の水平性は仮定しない。X 全体の正則性・整性・正規性も 追加していない。 結論は、U が連結で、包含 U ⟶ X による étale 基本群…
Source: Yamaguchi, arXiv:2610.02948v1, Lemma 1.2. X は連結な局所 Noether スキーム、D は水平な有効 Cartier 因子、 U = X ∖ Supp(D)、E は D の素成分、p は素数とする。 水平とは各素成分が Spec ℤ を支配することである。 次の二条件を仮定する。 X は D の台の全ての点で正則である。 E 上に、剰余標数が p で、D 全体が normal…
For a horizontal effective Cartier divisor on a connected locally Noetherian scheme regular along its support, assume that every component contains a normal crossings point in every prime residue characteristic. The comp…
The etale fundamental group of Spec ℤ is trivial for every geometric base point. The proof uses Minkowski's discriminant bound to show that every connected finite etale cover of Spec ℤ is trivial, then tests automorphism…
Source: Yamaguchi, arXiv:2610.02948v1, Lemma 2.1. 対応する Lean 宣言は abelianinvariance21。 X を連結な局所 Noether スキーム、D を水平な有効 Cartier 因子とし、 U = X \ Supp(D) と置く。次の三条件を仮定する。 X は D の台の各点で正則である。 D の各素成分は、剰余標数が 2 で、D 全体が normal crossin…
For a horizontal effective Cartier divisor D on a connected locally Noetherian scheme X, condition (†) consists of regularity along the support, a normal crossings point of residue characteristic two on every component,…
Source: Yamaguchi, arXiv:2610.02948v1, Remark 2.3. 対応する Lean 宣言は smoothboundary23。一つの remark に含まれる一般論と 境界条件への適用を、一つの宣言の二つの結論として記述する。 第一の主張では、スキーム E の構造射 E ⟶ Spec ℤ が滑らか・有限型・全射であり、 E の ℚ 上の一般ファイバーが幾何的連結であると仮定する。 結論は、任意の有限…
Pulling a horizontal effective Cartier divisor satisfying condition (†) back along a connected finite etale cover preserves horizontality and condition (†). Finite flat maps take the generic point of a component to a gen…
Under condition (†), the complement of the horizontal divisor is connected and the kernel of the inclusion-induced fundamental-group homomorphism is topologically perfect. The same homomorphism induces an isomorphism on…
Under condition (†), a continuous representation of the complement's fundamental group over a complete Noetherian local ring with finite residue field factors through the ambient fundamental group if and only if its resi…