AlgebraicGeometry.FiniteEtale.prosolvableResidualQuotientContinuousMulEquiv_of_pullbackModel_extensions
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
prosolvableResidualQuotientContinuousMulEquiv_of_pullbackModel_extensions
{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.ι))