These group objects store exactly the existing compatible-family limits. The stored coefficient algebra is installed in this field-only owner, before any original fraction field or tame-degree subset is introduced.
The full roots limit over the stored field, with its existing group.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory
universe u v
variable (k : Type u) [Field k] (E : Bundled Field.{v})def nativeFullRootsGroup : GrpCat.{v}Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory
universe u v
variable (k : Type u) [Field k] (E : Bundled Field.{v})instance nativeFullRootsGroup_topology :
TopologicalSpace (nativeFullRootsGroup k E).carrierA coordinate of the full roots group as a literal field element.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory
universe u v
variable (k : Type u) [Field k] (E : Bundled Field.{v})def nativeFullRootsScalar (n : InvertibleExponent k)
(x : (nativeFullRootsGroup k E).carrier) : E.αThe full roots limit of the relative separable closure under the stored action.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory
universe u v
variable (k : Type u) [Field k] (E : Bundled Field.{v})
variable (a : Algebra k E.α)def nativeSeparableRootsGroup : GrpCat.{v}Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory
universe u v
variable (k : Type u) [Field k] (E : Bundled Field.{v})
variable (a : Algebra k E.α)instance nativeSeparableRootsGroup_topology :
TopologicalSpace (nativeSeparableRootsGroup k E a).carrierThe actual separable coefficient at one full exponent.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory
universe u v
variable (k : Type u) [Field k] (E : Bundled Field.{v})
variable (a : Algebra k E.α)def nativeSeparableRootsCoordinate (n : InvertibleExponent k)
(x : (nativeSeparableRootsGroup k E a).carrier) :
(nativeSeparableResidueField k E a).αThe same coordinate viewed in the stored larger residue field.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory
universe u v
variable (k : Type u) [Field k] (E : Bundled Field.{v})
variable (a : Algebra k E.α)def nativeSeparableRootsScalar (n : InvertibleExponent k)
(x : (nativeSeparableRootsGroup k E a).carrier) : E.αLiteral scalar coordinates separate points of the full separable roots limit.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory
universe u v
variable (k : Type u) [Field k] (E : Bundled Field.{v})
variable (a : Algebra k E.α)theorem nativeSeparableRootsScalar_ext
(x y : (nativeSeparableRootsGroup k E a).carrier)
(h : ∀ n : InvertibleExponent k,
nativeSeparableRootsScalar k E a n x = nativeSeparableRootsScalar k E a n y) :
x = yRoot inclusion identifies the full roots groups of the two stored fields.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory
universe u v
variable (k : Type u) [Field k] (E : Bundled Field.{v})
variable (a : Algebra k E.α)def nativeSeparableRootsInclusionEquiv :
(nativeSeparableRootsGroup k E a).carrier ≃ₜ*
(nativeFullRootsGroup k E).carrierThe native comparison is the literal inclusion on every scalar coordinate.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory
universe u v
variable (k : Type u) [Field k] (E : Bundled Field.{v})
variable (a : Algebra k E.α)theorem nativeSeparableRootsInclusionEquiv_scalar
(n : InvertibleExponent k) (x : (nativeSeparableRootsGroup k E a).carrier) :
nativeFullRootsScalar k E n ((nativeSeparableRootsInclusionEquiv k E a).toFun x) =
nativeSeparableRootsScalar k E a n xThe existing separable residue automorphisms act on every full root coordinate.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory
universe u v
variable (k : Type u) [Field k] (E : Bundled Field.{v})
variable (a : Algebra k E.α)def nativeSeparableRootsAction :
(nativeSeparableResidueGroup k E a).carrier →*
Equiv.Perm (nativeSeparableRootsGroup k E a).carrierPlain application of the coefficient action on the full separable roots limit.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory
universe u v
variable (k : Type u) [Field k] (E : Bundled Field.{v})
variable (a : Algebra k E.α)def nativeSeparableRootsAction_apply
(σ : (nativeSeparableResidueGroup k E a).carrier)
(x : (nativeSeparableRootsGroup k E a).carrier) :
(nativeSeparableRootsGroup k E a).carrierA root-action coordinate is the stored separable residue action on that coefficient.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups.Inertia
open CategoryTheory
universe u v
variable (k : Type u) [Field k] (E : Bundled Field.{v})
variable (a : Algebra k E.α)theorem nativeSeparableRootsAction_scalar
(σ : (nativeSeparableResidueGroup k E a).carrier)
(n : InvertibleExponent k) (x : (nativeSeparableRootsGroup k E a).carrier) :
nativeSeparableRootsScalar k E a n (nativeSeparableRootsAction_apply k E a σ x) =
nativeSeparableResidueActionScalar k E a σ
(nativeSeparableRootsCoordinate k E a n x)