AlgebraicGeometry.FiniteEtale.prosolvableBoundaryEquivOfPullbackModelExtensions
Actual extensions of all finite abelian covers over the geometric open-normal pullback models identify the maximal prosolvable quotients across the boundary complement.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory
open CategoryTheory.PreGaloisCategory
open ProCGroups.FiniteStepSolvableQuotients
open scoped ProCGroupsSolvableQuotients
namespace AlgebraicGeometry.FiniteEtale
universe uLean source · statement
def prosolvableBoundaryEquivOfPullbackModelExtensions
{X : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]
[IsLocallyNoetherian X]
(D : X.EffectiveCartierDivisor)
[ConnectedSpace D.1.supportComplement]
{Omega : Type u} [Field Omega] [IsSepClosed Omega]
(xi : Spec (.of Omega) ⟶ D.1.supportComplement)
(extend : ∀
(U : OpenNormalSubgroup
π₁ᵉᵗ(xi ≫ D.1.supportComplement.ι))
(W : FiniteEtale
(openNormalPullbackModel D.1.supportComplement.ι xi U).sourceScheme)
(_hW : IsGalois W),
IsMulCommutative (Aut W) →
Σ Z : FiniteEtale
(openNormalPullbackModel D.1.supportComplement.ι xi U).targetScheme,
(pullback
(openNormalPullbackModel D.1.supportComplement.ι xi U).hom).obj Z ≅ W) :
(π₁ᵉᵗ(xi) ⧸ ProCGroups.ProC.proCResidualCore
ProCGroups.FiniteGroupClass.solvable π₁ᵉᵗ(xi)) ≃ₜ*
(π₁ᵉᵗ(xi ≫ D.1.supportComplement.ι) ⧸
ProCGroups.ProC.proCResidualCore ProCGroups.FiniteGroupClass.solvable
π₁ᵉᵗ(xi ≫ D.1.supportComplement.ι))