Nyll.EtaleFundamentalGroups.GaloisCovers.OpenNormalExtendedQuotientKernel

theorem

finiteDiscreteAbelianMapsKillKernel_of_continuousMulEquiv

ProCGroups.ProC.finiteDiscreteAbelianMapsKillKernel_of_continuousMulEquiv

Documentation

The condition that all finite discrete abelian maps kill a kernel can be transported across a commutative square whose horizontal maps are topological group isomorphisms.

Source context 3 commands

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

noncomputable section
namespace ProCGroups.ProC
universe u

Lean source · statement

theorem finiteDiscreteAbelianMapsKillKernel_of_continuousMulEquiv
    {G Q G' Q' : Type u}
    [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
    [TopologicalSpace G'] [Group G'] [IsTopologicalGroup G']
    [TopologicalSpace Q'] [Group Q'] [IsTopologicalGroup Q']
    (f : G →ₜ* Q) (f' : G' →ₜ* Q')
    (eG : G' ≃ₜ* G) (eQ : Q' ≃ₜ* Q)
    (hcomm : ∀ x, eQ (f' x) = f (eG x))
    (hkill : FiniteDiscreteAbelianMapsKillKernel f') :
    FiniteDiscreteAbelianMapsKillKernel f

theorem

fundamentalGroupHom_openNormalFiniteDiscreteAbelianMapsKillKernel_of_local_extensions

L76 ↗

AlgebraicGeometry.FiniteEtale.fundamentalGroupHom_openNormalFiniteDiscreteAbelianMapsKillKernel_of_local_extensions

Documentation

Suppose every open-normal restriction of a fundamental-group map is realized by a geometric local model, compatibly with topological group isomorphisms. If every abelian Galois quotient cover on each source model has an actual finite-etale extension on its target model, then all open-normal finite discrete abelian maps kill the corresponding restricted kernel.

Source context 8 commands

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

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

Lean source · statement

theorem fundamentalGroupHom_openNormalFiniteDiscreteAbelianMapsKillKernel_of_local_extensions
    (f : X ⟶ Y) (xi : Spec (.of Omega) ⟶ X)
    (X' Y' : OpenNormalSubgroup (π₁ᵉᵗ(xi ≫ f)) → Scheme.{u})
    [∀ H, ConnectedSpace (X' H)] [∀ H, ConnectedSpace (Y' H)]
    (g : ∀ H, X' H ⟶ Y' H)
    (xi' : ∀ H, Spec (.of Omega) ⟶ X' H)
    (eSource : ∀ H,
      π₁ᵉᵗ(xi' H) ≃ₜ*
        ProCGroups.OpenNormalSubgroup.comap
          (fundamentalGroupHom f xi).toMonoidHom
          (fundamentalGroupHom f xi).continuous_toFun H)
    (eTarget : ∀ H, π₁ᵉᵗ(xi' H ≫ g H) ≃ₜ* H)
    (hcomm : ∀ H a,
      eTarget H (fundamentalGroupHom (g H) (xi' H) a) =
        ProCGroups.ContinuousMonoidHom.restrictPreimage
          (fundamentalGroupHom f xi) (H : Subgroup π₁ᵉᵗ(xi ≫ f))
          (eSource H a))
    (extend : ∀ H (W : FiniteEtale (X' H)) (_hW : IsGalois W),
      IsMulCommutative (Aut W) →
        Σ Z : FiniteEtale (Y' H), (pullback (g H)).obj Z ≅ W) :
    OpenNormalFiniteDiscreteAbelianMapsKillKernel
      (fundamentalGroupHom f xi)

OpenNormalExtendedQuotientKernel.lean

Module documentation

Finite-abelian kernel tests on open-normal local models

finiteDiscreteAbelianMapsKillKernel_of_continuousMulEquiv

fundamentalGroupHom_openNormalFiniteDiscreteAbelianMapsKillKernel_of_local_extensions

Module documentation

Finite-abelian kernel tests on open-normal local models

Declarations

finiteDiscreteAbelianMapsKillKernel_of_continuousMulEquiv

fundamentalGroupHom_openNormalFiniteDiscreteAbelianMapsKillKernel_of_local_extensions