AlgebraicGeometry.FiniteEtale.henselianSpecializationFiberIso_equivariant
The actual natural isomorphism intertwines the compatible original fraction-field and residue-field point actions.
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 henselianSpecializationFiberIso_equivariant
(τ : R ≃ₐ[H] R) (σ : L ≃ₐ[H] L)
(hσ : ∀ r : R, σ (algebraMap R L r) = algebraMap R L (τ r))
(X : FiniteEtale (Spec (.of H))) (x : (fiber (Spec.algebraMap H L)).obj X) :
fiberObjEquivHom (Spec.algebraMap H (IsLocalRing.ResidueField R)) X
((henselianSpecializationFiberIso H R L).hom.app X
((fiberObjEquivHom (Spec.algebraMap H L) X).symm
(mapPointHom H L σ X (fiberObjEquivHom (Spec.algebraMap H L) X x)))) =
mapPointHom H (IsLocalRing.ResidueField R) (SchemeTheory.residueAlgEquiv H R τ) X
(fiberObjEquivHom (Spec.algebraMap H (IsLocalRing.ResidueField R)) X
((henselianSpecializationFiberIso H R L).hom.app X x))