EtaleFundamentalGroups.Inertia.actualTameCharacter_eq_one_iff
Identity in the actual root limit is detected by all of the original finite canonical coordinates, without changing their groups or characters.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
attribute [local instance] Ideal.Quotient.field
variable (A : Type u) (K : Type v) (L : Type w)
[CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
[Field K] [Field L] [Algebra A K] [IsFractionRing A K]
[Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
(Q : Ideal (normalizationCommAlgCat A L).carrier) [Q.IsMaximal]Lean source · statement
theorem actualTameCharacter_eq_one_iff
(σ : (actualNormalizationInertiaGroup A K L Q).carrier) :
(actualTameCharacter A K L Q).toFun σ = 1 ↔
∀ E : FiniteGaloisIntermediateField K L,
(actualFiniteTameCoordinate A K L Q E).hom'.toFun σ = 1