AlgebraicGeometry.FiniteEtale.henselianSpecializationFundamentalGroupEquiv_eq_of_point_actions
Equality of the proved literal point actions identifies the actual specialized fiber automorphism with the given residue fiber automorphism.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory
namespace AlgebraicGeometry.FiniteEtale
universe u
variable (H R L : Type u) [CommRing H] [CommRing R]
[HenselianLocalRing R] [IsIntegrallyClosed R] [Field L]
[Algebra H R] [Algebra R L] [IsFractionRing R L]
[Algebra H L] [IsScalarTower H R L]
[IsSepClosed L] [IsSepClosed (IsLocalRing.ResidueField R)]Lean source · statement
theorem henselianSpecializationFundamentalGroupEquiv_eq_of_point_actions
(τ : R ≃ₐ[H] R) (σ : L ≃ₐ[H] L)
(hcompat : ∀ r : R, σ (algebraMap R L r) = algebraMap R L (τ r))
(ρ : L →+* L) (hσ : σ.toRingHom = ρ)
(η : IsLocalRing.ResidueField R →+* IsLocalRing.ResidueField R)
(hτ : (SchemeTheory.residueAlgEquiv H R τ).toRingHom = η)
(a : π₁ᵉᵗ(Spec.algebraMap H L))
(b : π₁ᵉᵗ(Spec.algebraMap H (IsLocalRing.ResidueField R)))
(ha : ∀ (X : FiniteEtale (Spec (.of H))) (x : (fiber (Spec.algebraMap H L)).obj X),
(fiberObjEquivHom (Spec.algebraMap H L) X (a.hom.app X x)).left =
Spec.map (CommRingCat.ofHom ρ) ≫
(fiberObjEquivHom (Spec.algebraMap H L) X x).left)
(hb : ∀ (X : FiniteEtale (Spec (.of H)))
(x : (fiber (Spec.algebraMap H (IsLocalRing.ResidueField R))).obj X),
(fiberObjEquivHom (Spec.algebraMap H (IsLocalRing.ResidueField R)) X
(b.hom.app X x)).left = Spec.map (CommRingCat.ofHom η) ≫
(fiberObjEquivHom (Spec.algebraMap H (IsLocalRing.ResidueField R)) X x).left) :
henselianSpecializationFundamentalGroupEquiv H R L a = b