EtaleFundamentalGroups.Inertia.actualFiniteNormalizationRestrictionRingHom_conjugate
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v wLean source · statement
theorem actualFiniteNormalizationRestrictionRingHom_conjugate
(A : Type u) (K : Type v) (L : Type w)
[CommRing A] [Field K] [Field L]
[Algebra A K] [IsFractionRing A K]
[Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
(E : FiniteGaloisIntermediateField K L) (g s : Gal(L/K)) :
actualFiniteNormalizationRestrictionRingHom A K L E (g * s * g⁻¹) =
(actualFiniteNormalizationRestrictionRingHom A K L E g).comp
((actualFiniteNormalizationRestrictionRingHom A K L E s).comp
(actualFiniteNormalizationRestrictionRingHom A K L E g⁻¹))