Module

Theorem2Dot4FiniteEtaleStability.lean

Nyll.Yamaguchi26SolvableCoverings.Theorem2Dot4FiniteEtaleStability

1 declaration indexed from sourceView source ↗

Module documentation

Lemma 2.4: stability under finite etale covers

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 generic point, and finiteness makes the map of components surjective. This supplies a point in residue characteristic two upstairs. Regularity and normal crossings are preserved by etale base change. The generic-fiber condition follows by composing finite etale covers.

Source: Yamaguchi, arXiv:2610.02948v1, Lemma 2.4.

Imports6

Imported by2

theorem

finite_etale_stability_2_4

L40 ↗

Yamaguchi26SolvableCoverings.finite_etale_stability_2_4

Documentation

補題 2.4：連結有限 étale 被覆への引き戻しは、水平性と定義 2.2 の境界条件 (†) を保つ。

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open AlgebraicGeometry CategoryTheory
open AlgebraicGeometry.FiniteEtale
namespace Yamaguchi26SolvableCoverings
variable {X : Scheme.{0}} [ConnectedSpace X] [IsLocallyNoetherian X]
omit [ConnectedSpace X] [IsLocallyNoetherian X] in

Lean source · statement

theorem finite_etale_stability_2_4
    (D : X.EffectiveCartierDivisor) (hhor : IsHorizontal D)
    (hD : BoundaryCondition D) (Y : FiniteEtale X) (_hY : ConnectedSpace Y.left) :
    IsHorizontal (D.comapFiniteEtale Y) ∧ BoundaryCondition (D.comapFiniteEtale Y)

Module documentation

Lemma 2.4: stability under finite etale covers

Declarations

finite_etale_stability_2_4