NYLL
Module

BoundaryAbelianizationPullback.lean

Nyll.Yamaguchi26SolvableCoverings.Geometry.BoundaryAbelianizationPullback
3 declarations indexed from sourceView source ↗

Module documentation

開正規部分群の上での境界アーベル化比較

定理 2.5 の幾何学的な段階。開正規部分群に対応する有限 étale 被覆とその引き戻しは EFG の OpenNormalPullbackModel から実際に構成する。補題 2.1 と 2.4 によって 引き戻し全体が連結であることを示し、選んだ連結成分と境界補集合を同一視する。 その補集合に補題 2.1 を適用し、任意の有限離散可換群への連続準同型が局所的な核を 消すことを証明する。基本群の射の合成に伴う共役は、単位元に送られる条件を変えない。

この段階の証明は原稿の補題 2.1・2.4 に依存する。それらの証明が未完了である 限り、このファイルだけによって幾何学的な議論全体が完成したことにはならない。

Imports8
Imported by2

Declarations

theorem

finiteEtale_pullback_isEquivalence_of_isIso

L37 ↗
Yamaguchi26SolvableCoverings.finiteEtale_pullback_isEquivalence_of_isIso
Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open AlgebraicGeometry.FiniteEtale CategoryTheory.PreGaloisCategory
open ProCGroups.FiniteStepSolvableQuotients
namespace Yamaguchi26SolvableCoverings
Lean source · statement
theorem finiteEtale_pullback_isEquivalence_of_isIso
    {X Y : Scheme.{0}} (f : X ⟶ Y) [IsIso f] :
    (pullback f).IsEquivalence
theorem

fundamentalGroupHom_composite_eq_one

L51 ↗
Yamaguchi26SolvableCoverings.fundamentalGroupHom_composite_eq_one
Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open AlgebraicGeometry.FiniteEtale CategoryTheory.PreGaloisCategory
open ProCGroups.FiniteStepSolvableQuotients
namespace Yamaguchi26SolvableCoverings
Lean source · statement
theorem fundamentalGroupHom_composite_eq_one
    {X Y Z : Scheme.{0}} {Ω : Type} [Field Ω]
    (f : X ⟶ Y) (g : Y ⟶ Z) (point : Spec (.of Ω) ⟶ X)
    (a : π₁ᵉᵗ(point)) (ha : fundamentalGroupHom (f ≫ g) point a = 1) :
    fundamentalGroupHom g (point ≫ f) (fundamentalGroupHom f point a) = 1
theorem

boundary_openNormalFiniteDiscreteAbelianMapsKillKernel

L74 ↗
Yamaguchi26SolvableCoverings.boundary_openNormalFiniteDiscreteAbelianMapsKillKernel
Documentation

条件 (†) の下で、開正規部分群の逆像から有限離散可換群への写像は境界核を消す。

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open AlgebraicGeometry.FiniteEtale CategoryTheory.PreGaloisCategory
open ProCGroups.FiniteStepSolvableQuotients
namespace Yamaguchi26SolvableCoverings
Lean source · statement
theorem boundary_openNormalFiniteDiscreteAbelianMapsKillKernel
    {X : Scheme.{0}} [ConnectedSpace X] [IsLocallyNoetherian X]
    (D : X.EffectiveCartierDivisor) (hhor : IsHorizontal D)
    (hD : BoundaryCondition D) [ConnectedSpace D.1.supportComplement]
    {Ω : Type} [Field Ω] [IsSepClosed Ω]
    (point : Spec (.of Ω) ⟶ D.1.supportComplement) :
    OpenNormalFiniteDiscreteAbelianMapsKillKernel
      (fundamentalGroupHom D.1.supportComplement.ι point)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.