Module

OpenNormalPullbackModel.lean

Nyll.EtaleFundamentalGroups.GaloisCovers.OpenNormalPullbackModel

10 declarations indexed from sourceView source ↗

Module documentation

Geometric models of open-normal pullbacks

Every open normal subgroup of the target fundamental group determines an actual pointed finite-etale Galois cover and an actual pointed Galois component of its pullback. This file packages those choices uniformly, so the local finite-cover extension argument can be passed directly to the open-normal prosolvable criterion.

Imports2

Imported by2

structure

OpenNormalPullbackModel

L35 ↗

AlgebraicGeometry.FiniteEtale.OpenNormalPullbackModel

Documentation

An actual geometric realization of the restriction of a fundamental group map over one open normal subgroup of its target.

Source context 8 commands

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

noncomputable section
open CategoryTheory
open CategoryTheory.PreGaloisCategory
open ProCGroups.FiniteStepSolvableQuotients
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {X Y : Scheme.{u}} [ConnectedSpace X] [ConnectedSpace Y]
variable {Omega : Type u} [Field Omega] [IsSepClosed Omega]

Lean source · full declaration

structure OpenNormalPullbackModel
    (f : X ⟶ Y) (xi : Spec (.of Omega) ⟶ X)
    (U : OpenNormalSubgroup π₁ᵉᵗ(xi ≫ f)) where
  /-- The finite etale Galois cover of the target realizing the subgroup. -/
  targetCover : FiniteEtale Y
  /-- The chosen geometric point in the fiber of the target cover. -/
  targetPoint : (fiber (xi ≫ f)).obj targetCover
  /-- The Galois component of the pulled-back target cover. -/
  sourceCover : FiniteEtale X
  /-- The inclusion of the source component into the pullback cover. -/
  inclusion : sourceCover ⟶ (pullback f).obj targetCover
  /-- The chosen geometric point in the fiber of the source component. -/
  sourcePoint : (fiber xi).obj sourceCover
  /-- The target cover is a Galois object. -/
  targetIsGalois : IsGalois targetCover
  /-- The source component is a Galois object. -/
  sourceIsGalois : IsGalois sourceCover
  /-- The component inclusion is a monomorphism. -/
  inclusionMono : Mono inclusion
  /-- The source fundamental group identifies with the inverse-image subgroup. -/
  sourceEquiv :
    π₁ᵉᵗ((fiberObjEquivHom xi sourceCover sourcePoint).left) ≃ₜ*
      ProCGroups.OpenNormalSubgroup.comap
        (fundamentalGroupHom f xi).toMonoidHom
        (fundamentalGroupHom f xi).continuous_toFun U
  /-- The target-cover fundamental group identifies with the target subgroup. -/
  targetEquiv :
    π₁ᵉᵗ((fiberObjEquivHom xi sourceCover sourcePoint).left ≫
      (inclusion.left ≫ Limits.pullback.fst targetCover.hom f)) ≃ₜ* U
  /-- The fundamental group map agrees with restriction under these identifications. -/
  commutes : ∀ a,
    targetEquiv
        (fundamentalGroupHom
          (inclusion.left ≫ Limits.pullback.fst targetCover.hom f)
          (fiberObjEquivHom xi sourceCover sourcePoint).left a) =
      ProCGroups.ContinuousMonoidHom.restrictPreimage
        (fundamentalGroupHom f xi) (U : Subgroup π₁ᵉᵗ(xi ≫ f))
        (sourceEquiv a)

theorem

nonempty_openNormalPullbackModel

L76 ↗

AlgebraicGeometry.FiniteEtale.nonempty_openNormalPullbackModel

Documentation

The geometric pullback-component construction supplies a model for every open normal subgroup.

Source context 8 commands

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

noncomputable section
open CategoryTheory
open CategoryTheory.PreGaloisCategory
open ProCGroups.FiniteStepSolvableQuotients
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {X Y : Scheme.{u}} [ConnectedSpace X] [ConnectedSpace Y]
variable {Omega : Type u} [Field Omega] [IsSepClosed Omega]

Lean source · statement

theorem nonempty_openNormalPullbackModel
    (f : X ⟶ Y) (xi : Spec (.of Omega) ⟶ X)
    (U : OpenNormalSubgroup π₁ᵉᵗ(xi ≫ f)) :
    Nonempty (OpenNormalPullbackModel f xi U)

def

openNormalPullbackModel

L98 ↗

AlgebraicGeometry.FiniteEtale.openNormalPullbackModel

Documentation

A fixed actual model for an open normal subgroup.

Source context 8 commands

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

noncomputable section
open CategoryTheory
open CategoryTheory.PreGaloisCategory
open ProCGroups.FiniteStepSolvableQuotients
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {X Y : Scheme.{u}} [ConnectedSpace X] [ConnectedSpace Y]
variable {Omega : Type u} [Field Omega] [IsSepClosed Omega]

Lean source · statement

def openNormalPullbackModel
    (f : X ⟶ Y) (xi : Spec (.of Omega) ⟶ X)
    (U : OpenNormalSubgroup π₁ᵉᵗ(xi ≫ f)) :
    OpenNormalPullbackModel f xi U

abbrev

sourceScheme

L110 ↗

AlgebraicGeometry.FiniteEtale.OpenNormalPullbackModel.sourceScheme

Documentation

The source scheme in the selected geometric model.

Source context 11 commands

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

noncomputable section
open CategoryTheory
open CategoryTheory.PreGaloisCategory
open ProCGroups.FiniteStepSolvableQuotients
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {X Y : Scheme.{u}} [ConnectedSpace X] [ConnectedSpace Y]
variable {Omega : Type u} [Field Omega] [IsSepClosed Omega]
namespace OpenNormalPullbackModel
variable {f : X ⟶ Y} {xi : Spec (.of Omega) ⟶ X}
variable {U : OpenNormalSubgroup π₁ᵉᵗ(xi ≫ f)}

Lean source · statement

abbrev sourceScheme (M : OpenNormalPullbackModel f xi U) : Scheme.{u}

abbrev

targetScheme

L114 ↗

AlgebraicGeometry.FiniteEtale.OpenNormalPullbackModel.targetScheme

Documentation

The target scheme in the selected geometric model.

Source context 11 commands

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

noncomputable section
open CategoryTheory
open CategoryTheory.PreGaloisCategory
open ProCGroups.FiniteStepSolvableQuotients
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {X Y : Scheme.{u}} [ConnectedSpace X] [ConnectedSpace Y]
variable {Omega : Type u} [Field Omega] [IsSepClosed Omega]
namespace OpenNormalPullbackModel
variable {f : X ⟶ Y} {xi : Spec (.of Omega) ⟶ X}
variable {U : OpenNormalSubgroup π₁ᵉᵗ(xi ≫ f)}

Lean source · statement

abbrev targetScheme (M : OpenNormalPullbackModel f xi U) : Scheme.{u}

abbrev

hom

L118 ↗

AlgebraicGeometry.FiniteEtale.OpenNormalPullbackModel.hom

Documentation

The actual morphism from the pullback component to the target cover.

Source context 11 commands

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

noncomputable section
open CategoryTheory
open CategoryTheory.PreGaloisCategory
open ProCGroups.FiniteStepSolvableQuotients
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {X Y : Scheme.{u}} [ConnectedSpace X] [ConnectedSpace Y]
variable {Omega : Type u} [Field Omega] [IsSepClosed Omega]
namespace OpenNormalPullbackModel
variable {f : X ⟶ Y} {xi : Spec (.of Omega) ⟶ X}
variable {U : OpenNormalSubgroup π₁ᵉᵗ(xi ≫ f)}

Lean source · statement

abbrev hom (M : OpenNormalPullbackModel f xi U) :
    M.sourceScheme ⟶ M.targetScheme

abbrev

geometricPoint

L123 ↗

AlgebraicGeometry.FiniteEtale.OpenNormalPullbackModel.geometricPoint

Documentation

The geometric point on the source component.

Source context 11 commands

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

noncomputable section
open CategoryTheory
open CategoryTheory.PreGaloisCategory
open ProCGroups.FiniteStepSolvableQuotients
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {X Y : Scheme.{u}} [ConnectedSpace X] [ConnectedSpace Y]
variable {Omega : Type u} [Field Omega] [IsSepClosed Omega]
namespace OpenNormalPullbackModel
variable {f : X ⟶ Y} {xi : Spec (.of Omega) ⟶ X}
variable {U : OpenNormalSubgroup π₁ᵉᵗ(xi ≫ f)}

Lean source · statement

abbrev geometricPoint (M : OpenNormalPullbackModel f xi U) :
    Spec (.of Omega) ⟶ M.sourceScheme

instance

sourceConnectedSpace

L127 ↗

AlgebraicGeometry.FiniteEtale.OpenNormalPullbackModel.sourceConnectedSpace

Source context 11 commands

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

noncomputable section
open CategoryTheory
open CategoryTheory.PreGaloisCategory
open ProCGroups.FiniteStepSolvableQuotients
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {X Y : Scheme.{u}} [ConnectedSpace X] [ConnectedSpace Y]
variable {Omega : Type u} [Field Omega] [IsSepClosed Omega]
namespace OpenNormalPullbackModel
variable {f : X ⟶ Y} {xi : Spec (.of Omega) ⟶ X}
variable {U : OpenNormalSubgroup π₁ᵉᵗ(xi ≫ f)}

Lean source · statement

instance sourceConnectedSpace
    (M : OpenNormalPullbackModel f xi U) : ConnectedSpace M.sourceScheme

instance

targetConnectedSpace

L132 ↗

AlgebraicGeometry.FiniteEtale.OpenNormalPullbackModel.targetConnectedSpace

Source context 11 commands

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

noncomputable section
open CategoryTheory
open CategoryTheory.PreGaloisCategory
open ProCGroups.FiniteStepSolvableQuotients
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {X Y : Scheme.{u}} [ConnectedSpace X] [ConnectedSpace Y]
variable {Omega : Type u} [Field Omega] [IsSepClosed Omega]
namespace OpenNormalPullbackModel
variable {f : X ⟶ Y} {xi : Spec (.of Omega) ⟶ X}
variable {U : OpenNormalSubgroup π₁ᵉᵗ(xi ≫ f)}

Lean source · statement

instance targetConnectedSpace
    (M : OpenNormalPullbackModel f xi U) : ConnectedSpace M.targetScheme

theorem

fundamentalGroupHom_openNormalFiniteDiscreteAbelianMapsKillKernel_of_pullbackModel_extensions

L142 ↗

AlgebraicGeometry.FiniteEtale.fundamentalGroupHom_openNormalFiniteDiscreteAbelianMapsKillKernel_of_pullbackModel_extensions

Documentation

Specializing the general open-normal kernel bridge to the uniformly selected actual pullback components leaves only the geometric cover-extension input. No fundamental-group square is assumed.

Source context 8 commands

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

noncomputable section
open CategoryTheory
open CategoryTheory.PreGaloisCategory
open ProCGroups.FiniteStepSolvableQuotients
namespace AlgebraicGeometry.FiniteEtale
universe u
variable {X Y : Scheme.{u}} [ConnectedSpace X] [ConnectedSpace Y]
variable {Omega : Type u} [Field Omega] [IsSepClosed Omega]

Lean source · statement

theorem
    fundamentalGroupHom_openNormalFiniteDiscreteAbelianMapsKillKernel_of_pullbackModel_extensions
    (f : X ⟶ Y) (xi : Spec (.of Omega) ⟶ X)
    (extend : ∀ (U : OpenNormalSubgroup π₁ᵉᵗ(xi ≫ f))
      (W : FiniteEtale (openNormalPullbackModel f xi U).sourceScheme)
      (_hW : IsGalois W),
      IsMulCommutative (Aut W) →
        Σ Z : FiniteEtale (openNormalPullbackModel f xi U).targetScheme,
          (pullback (openNormalPullbackModel f xi U).hom).obj Z ≅ W) :
    OpenNormalFiniteDiscreteAbelianMapsKillKernel
      (fundamentalGroupHom f xi)

Module documentation

Geometric models of open-normal pullbacks

Declarations