EtaleFundamentalGroups.finiteEtaleGaloisCoverQuotientOfMorphism_transport
Restriction along a scheme morphism and transport of the pointed fiber commute at the level of the resulting finite monodromy homomorphism.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory
open CategoryTheory.PreGaloisCategory
namespace EtaleFundamentalGroups
universe uLean source · full declaration
theorem finiteEtaleGaloisCoverQuotientOfMorphism_transport
{T U : Scheme.{u}} [ConnectedSpace U]
{Omega Omega' : Type u}
[Field Omega] [IsSepClosed Omega]
[Field Omega'] [IsSepClosed Omega']
(j : T ⟶ U) (xi : Spec (.of Omega) ⟶ T)
(xi' : Spec (.of Omega') ⟶ U)
(p : AlgebraicGeometry.FiniteEtale.fiber (xi ≫ j) ≅
AlgebraicGeometry.FiniteEtale.fiber xi')
(Y : AlgebraicGeometry.FiniteEtale U) (hY : IsGalois Y)
(y : (AlgebraicGeometry.FiniteEtale.fiber xi').obj Y) :
letI : IsGalois Y := hY
Inertia.finiteEtaleGaloisCoverQuotientOfMorphism
j xi Y hY (p.inv.app Y y) =
(EtaleFundamentalGroups.finiteEtaleGaloisCoverQuotientMonoidHom
xi' Y hY y).comp
(p.conjAut.toMonoidHom.comp
(AlgebraicGeometry.FiniteEtale.fundamentalGroupHom j xi).toMonoidHom) := by
let : IsGalois Y := hY
change
(finiteEtaleGaloisCoverQuotientMonoidHom
(xi ≫ j) Y hY (p.inv.app Y y)).comp
(AlgebraicGeometry.FiniteEtale.fundamentalGroupHom j xi).toMonoidHom = _
exact galoisObjectQuotientMonoidHom_transport_comp
(AlgebraicGeometry.FiniteEtale.fiber (xi ≫ j))
(AlgebraicGeometry.FiniteEtale.fiber xi') p Y y
(AlgebraicGeometry.FiniteEtale.fundamentalGroupHom j xi).toMonoidHom