NYLL
Module

ActualAbsoluteRamificationData.lean

Nyll.EtaleFundamentalGroups.Inertia.ActualAbsoluteRamificationData
26 declarations indexed from sourceView source ↗

Module documentation

The actual full absolute ramification diagram

The field-only constructor shares the existing coefficient fields and algebra. The group constructor shares the original 5-F group objects, independent P, maps and topologies. The last constructor inserts the SAME absolute residue map and actual postcomposed character. Every stored datum and the intrinsically computed roots action has a concrete computation law.

Imports19
Imported by2

Declarations

def

actualAbsoluteRamificationResidues

L52 ↗
EtaleFundamentalGroups.Inertia.actualAbsoluteRamificationResidues
Documentation

The SAME literal residue fields, with their existing coefficient algebra.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
section ResidueData
variable (A : Type u) (Ω : Type w) [CommRing A] [IsLocalRing A]
  [CommRing Ω] [Algebra A Ω]
  (Q : Ideal (normalizationCommAlgCat A Ω).carrier) [Q.IsMaximal]
Lean source · full declaration
def actualAbsoluteRamificationResidues : NativeAbsoluteRamificationResidues.{u, w} where
  baseResidue := ⟨IsLocalRing.ResidueField A, inferInstanceAs (Field (IsLocalRing.ResidueField A))⟩
  residue := normalizationResidueFieldObject A Ω Q
  residueAlgebra := normalizationResidueFieldAlgebra A Ω Q
theorem

actualAbsoluteRamificationResidues_baseResidue

L58 ↗
EtaleFundamentalGroups.Inertia.actualAbsoluteRamificationResidues_baseResidue
Documentation

The stored base field is the original local residue field.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
section ResidueData
variable (A : Type u) (Ω : Type w) [CommRing A] [IsLocalRing A]
  [CommRing Ω] [Algebra A Ω]
  (Q : Ideal (normalizationCommAlgCat A Ω).carrier) [Q.IsMaximal]
Lean source · statement
theorem actualAbsoluteRamificationResidues_baseResidue :
    (actualAbsoluteRamificationResidues A Ω Q).baseResidue.α = IsLocalRing.ResidueField A
theorem

actualAbsoluteRamificationResidues_residue

L62 ↗
EtaleFundamentalGroups.Inertia.actualAbsoluteRamificationResidues_residue
Documentation

The stored upstairs field is the SAME literal maximal quotient object.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
section ResidueData
variable (A : Type u) (Ω : Type w) [CommRing A] [IsLocalRing A]
  [CommRing Ω] [Algebra A Ω]
  (Q : Ideal (normalizationCommAlgCat A Ω).carrier) [Q.IsMaximal]
Lean source · statement
theorem actualAbsoluteRamificationResidues_residue :
    (actualAbsoluteRamificationResidues A Ω Q).residue =
      normalizationResidueFieldObject A Ω Q
theorem

actualAbsoluteRamificationResidues_residue_carrier

L67 ↗
EtaleFundamentalGroups.Inertia.actualAbsoluteRamificationResidues_residue_carrier
Documentation

Its carrier is literally the original normalization quotient.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
section ResidueData
variable (A : Type u) (Ω : Type w) [CommRing A] [IsLocalRing A]
  [CommRing Ω] [Algebra A Ω]
  (Q : Ideal (normalizationCommAlgCat A Ω).carrier) [Q.IsMaximal]
Lean source · statement
theorem actualAbsoluteRamificationResidues_residue_carrier :
    (actualAbsoluteRamificationResidues A Ω Q).residue.α =
      ((normalizationCommAlgCat A Ω).carrier ⧸ Q)
theorem

actualAbsoluteRamificationResidues_residueAlgebra

L72 ↗
EtaleFundamentalGroups.Inertia.actualAbsoluteRamificationResidues_residueAlgebra
Documentation

The stored algebra is the existing actual residue coefficient map.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
section ResidueData
variable (A : Type u) (Ω : Type w) [CommRing A] [IsLocalRing A]
  [CommRing Ω] [Algebra A Ω]
  (Q : Ideal (normalizationCommAlgCat A Ω).carrier) [Q.IsMaximal]
Lean source · statement
theorem actualAbsoluteRamificationResidues_residueAlgebra :
    (actualAbsoluteRamificationResidues A Ω Q).residueAlgebra =
      normalizationResidueFieldAlgebra A Ω Q
theorem

actualAbsoluteRamificationResidues_separableResidue

L77 ↗
EtaleFundamentalGroups.Inertia.actualAbsoluteRamificationResidues_separableResidue
Documentation

The separable field is the SAME stored relative separable closure.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
section ResidueData
variable (A : Type u) (Ω : Type w) [CommRing A] [IsLocalRing A]
  [CommRing Ω] [Algebra A Ω]
  (Q : Ideal (normalizationCommAlgCat A Ω).carrier) [Q.IsMaximal]
Lean source · statement
theorem actualAbsoluteRamificationResidues_separableResidue :
    (actualAbsoluteRamificationResidues A Ω Q).separableResidue =
      nativeSeparableResidueField (IsLocalRing.ResidueField A)
        (normalizationResidueFieldObject A Ω Q) (normalizationResidueFieldAlgebra A Ω Q)
theorem

actualAbsoluteRamificationResidues_residueAutomorphisms

L83 ↗
EtaleFundamentalGroups.Inertia.actualAbsoluteRamificationResidues_residueAutomorphisms
Documentation

The residue target is the SAME original absolute residue Galois group.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
section ResidueData
variable (A : Type u) (Ω : Type w) [CommRing A] [IsLocalRing A]
  [CommRing Ω] [Algebra A Ω]
  (Q : Ideal (normalizationCommAlgCat A Ω).carrier) [Q.IsMaximal]
Lean source · statement
theorem actualAbsoluteRamificationResidues_residueAutomorphisms :
    (actualAbsoluteRamificationResidues A Ω Q).residueAutomorphisms =
      normalizationResidueSeparableGroup A Ω Q
theorem

actualAbsoluteRamificationResidues_rootsGroup

L88 ↗
EtaleFundamentalGroups.Inertia.actualAbsoluteRamificationResidues_rootsGroup
Documentation

The intrinsic full target is the SAME separable roots group of 6-C.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
section ResidueData
variable (A : Type u) (Ω : Type w) [CommRing A] [IsLocalRing A]
  [CommRing Ω] [Algebra A Ω]
  (Q : Ideal (normalizationCommAlgCat A Ω).carrier) [Q.IsMaximal]
Lean source · statement
theorem actualAbsoluteRamificationResidues_rootsGroup :
    (actualAbsoluteRamificationResidues A Ω Q).rootsGroup =
      normalizationSeparableRootsGroup A Ω Q
theorem

actualAbsoluteRamificationResidues_rootsTopology

L93 ↗
EtaleFundamentalGroups.Inertia.actualAbsoluteRamificationResidues_rootsTopology
Documentation

Its topology is the SAME full inverse-limit topology.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
section ResidueData
variable (A : Type u) (Ω : Type w) [CommRing A] [IsLocalRing A]
  [CommRing Ω] [Algebra A Ω]
  (Q : Ideal (normalizationCommAlgCat A Ω).carrier) [Q.IsMaximal]
Lean source · statement
theorem actualAbsoluteRamificationResidues_rootsTopology :
    NativeAbsoluteRamificationResidues.rootsGroup_topology
        (actualAbsoluteRamificationResidues A Ω Q) =
      normalizationSeparableRootsGroup_topology A Ω Q
def

actualAbsoluteRamificationGroups

L107 ↗
EtaleFundamentalGroups.Inertia.actualAbsoluteRamificationGroups
Documentation

Share the original groups, independent P and quotient/topologies once.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) (K : Type v) (Ω : Type w)
  [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
  [Field K] [Field Ω] [Algebra A K] [IsFractionRing A K]
  [Algebra K Ω] [Algebra A Ω] [IsScalarTower A K Ω] [IsSepClosure K Ω]
  (Q : Ideal (normalizationCommAlgCat A Ω).carrier) [Q.IsMaximal]
Lean source · statement
def actualAbsoluteRamificationGroups : NativeAbsoluteRamificationGroups.{w}
def

actualAbsoluteRamificationDiagram

L112 ↗
EtaleFundamentalGroups.Inertia.actualAbsoluteRamificationDiagram
Documentation

Insert the SAME actual absolute maps into their literal full targets.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) (K : Type v) (Ω : Type w)
  [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
  [Field K] [Field Ω] [Algebra A K] [IsFractionRing A K]
  [Algebra K Ω] [Algebra A Ω] [IsScalarTower A K Ω] [IsSepClosure K Ω]
  (Q : Ideal (normalizationCommAlgCat A Ω).carrier) [Q.IsMaximal]
Lean source · full declaration
def actualAbsoluteRamificationDiagram :
    NativeAbsoluteRamificationDiagram (actualAbsoluteRamificationResidues A Ω Q)
      (actualAbsoluteRamificationGroups A K Ω Q) where
  residueMorphism := normalizationAbsoluteResidueMorphism A K Ω Q
  character := actualAbsoluteTameCharacterMorphism A K Ω Q
theorem

actualAbsoluteRamificationGroups_decomposition

L119 ↗
EtaleFundamentalGroups.Inertia.actualAbsoluteRamificationGroups_decomposition
Documentation

The stored D is the original normalization decomposition group.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) (K : Type v) (Ω : Type w)
  [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
  [Field K] [Field Ω] [Algebra A K] [IsFractionRing A K]
  [Algebra K Ω] [Algebra A Ω] [IsScalarTower A K Ω] [IsSepClosure K Ω]
  (Q : Ideal (normalizationCommAlgCat A Ω).carrier) [Q.IsMaximal]
Lean source · statement
theorem actualAbsoluteRamificationGroups_decomposition :
    (actualAbsoluteRamificationGroups A K Ω Q).decomposition =
      normalizationDecompositionGroup A K Ω Q
theorem

actualAbsoluteRamificationGroups_inertia

L124 ↗
EtaleFundamentalGroups.Inertia.actualAbsoluteRamificationGroups_inertia
Documentation

The stored I is the original normalization inertia group.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) (K : Type v) (Ω : Type w)
  [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
  [Field K] [Field Ω] [Algebra A K] [IsFractionRing A K]
  [Algebra K Ω] [Algebra A Ω] [IsScalarTower A K Ω] [IsSepClosure K Ω]
  (Q : Ideal (normalizationCommAlgCat A Ω).carrier) [Q.IsMaximal]
Lean source · statement
theorem actualAbsoluteRamificationGroups_inertia :
    (actualAbsoluteRamificationGroups A K Ω Q).inertia =
      actualNormalizationInertiaGroup A K Ω Q
theorem

actualAbsoluteRamificationGroups_tameQuotient

L129 ↗
EtaleFundamentalGroups.Inertia.actualAbsoluteRamificationGroups_tameQuotient
Documentation

The stored I/P is the SAME literal original quotient.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) (K : Type v) (Ω : Type w)
  [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
  [Field K] [Field Ω] [Algebra A K] [IsFractionRing A K]
  [Algebra K Ω] [Algebra A Ω] [IsScalarTower A K Ω] [IsSepClosure K Ω]
  (Q : Ideal (normalizationCommAlgCat A Ω).carrier) [Q.IsMaximal]
Lean source · statement
theorem actualAbsoluteRamificationGroups_tameQuotient :
    (actualAbsoluteRamificationGroups A K Ω Q).tameQuotient =
      actualTameQuotientGroup A K Ω Q
theorem

actualAbsoluteRamificationGroups_wild

L134 ↗
EtaleFundamentalGroups.Inertia.actualAbsoluteRamificationGroups_wild
Documentation

The stored P is the SAME independently defined principal-unit subgroup.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) (K : Type v) (Ω : Type w)
  [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
  [Field K] [Field Ω] [Algebra A K] [IsFractionRing A K]
  [Algebra K Ω] [Algebra A Ω] [IsScalarTower A K Ω] [IsSepClosure K Ω]
  (Q : Ideal (normalizationCommAlgCat A Ω).carrier) [Q.IsMaximal]
Lean source · statement
theorem actualAbsoluteRamificationGroups_wild :
    (actualAbsoluteRamificationGroups A K Ω Q).wild =
      actualNormalizationWildSubgroup A K Ω Q
theorem

actualAbsoluteRamificationGroups_inertiaInclusion

L139 ↗
EtaleFundamentalGroups.Inertia.actualAbsoluteRamificationGroups_inertiaInclusion
Documentation

The inclusion is the SAME literal I-to-D map.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) (K : Type v) (Ω : Type w)
  [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
  [Field K] [Field Ω] [Algebra A K] [IsFractionRing A K]
  [Algebra K Ω] [Algebra A Ω] [IsScalarTower A K Ω] [IsSepClosure K Ω]
  (Q : Ideal (normalizationCommAlgCat A Ω).carrier) [Q.IsMaximal]
Lean source · statement
theorem actualAbsoluteRamificationGroups_inertiaInclusion :
    (actualAbsoluteRamificationGroups A K Ω Q).inertiaInclusion.hom' =
      actualNormalizationInertiaToDecomposition A K Ω Q
theorem

actualAbsoluteRamificationGroups_quotientProjection

L144 ↗
EtaleFundamentalGroups.Inertia.actualAbsoluteRamificationGroups_quotientProjection
Documentation

The quotient map is the SAME original quotient projection.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) (K : Type v) (Ω : Type w)
  [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
  [Field K] [Field Ω] [Algebra A K] [IsFractionRing A K]
  [Algebra K Ω] [Algebra A Ω] [IsScalarTower A K Ω] [IsSepClosure K Ω]
  (Q : Ideal (normalizationCommAlgCat A Ω).carrier) [Q.IsMaximal]
Lean source · statement
theorem actualAbsoluteRamificationGroups_quotientProjection :
    (actualAbsoluteRamificationGroups A K Ω Q).quotientProjection =
      actualTameQuotientProjection A K Ω Q
theorem

actualAbsoluteRamificationGroups_conjugate

L149 ↗
EtaleFundamentalGroups.Inertia.actualAbsoluteRamificationGroups_conjugate
Documentation

Conjugation is the original decomposition conjugation on inertia.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) (K : Type v) (Ω : Type w)
  [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
  [Field K] [Field Ω] [Algebra A K] [IsFractionRing A K]
  [Algebra K Ω] [Algebra A Ω] [IsScalarTower A K Ω] [IsSepClosure K Ω]
  (Q : Ideal (normalizationCommAlgCat A Ω).carrier) [Q.IsMaximal]
Lean source · statement
theorem actualAbsoluteRamificationGroups_conjugate
    (d : (normalizationDecompositionGroup A K Ω Q).carrier)
    (σ : (actualNormalizationInertiaGroup A K Ω Q).carrier) :
    (actualAbsoluteRamificationGroups A K Ω Q).conjugate d σ =
      originalFiniteNormalizationInertiaConjugate A K Ω Q d σ
theorem

actualAbsoluteRamificationGroups_inertiaTopology

L156 ↗
EtaleFundamentalGroups.Inertia.actualAbsoluteRamificationGroups_inertiaTopology
Documentation

The inertia topology is the original Krull-subgroup topology.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) (K : Type v) (Ω : Type w)
  [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
  [Field K] [Field Ω] [Algebra A K] [IsFractionRing A K]
  [Algebra K Ω] [Algebra A Ω] [IsScalarTower A K Ω] [IsSepClosure K Ω]
  (Q : Ideal (normalizationCommAlgCat A Ω).carrier) [Q.IsMaximal]
Lean source · statement
theorem actualAbsoluteRamificationGroups_inertiaTopology :
    (actualAbsoluteRamificationGroups A K Ω Q).inertiaTopology =
      actualNormalizationInertiaGroup_topologicalSpace A K Ω Q
theorem

actualAbsoluteRamificationGroups_tameQuotientTopology

L161 ↗
EtaleFundamentalGroups.Inertia.actualAbsoluteRamificationGroups_tameQuotientTopology
Documentation

The tame topology is the original literal quotient topology.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) (K : Type v) (Ω : Type w)
  [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
  [Field K] [Field Ω] [Algebra A K] [IsFractionRing A K]
  [Algebra K Ω] [Algebra A Ω] [IsScalarTower A K Ω] [IsSepClosure K Ω]
  (Q : Ideal (normalizationCommAlgCat A Ω).carrier) [Q.IsMaximal]
Lean source · statement
theorem actualAbsoluteRamificationGroups_tameQuotientTopology :
    (actualAbsoluteRamificationGroups A K Ω Q).tameQuotientTopology =
      actualTameQuotientGroup_topologicalSpace A K Ω Q
theorem

actualAbsoluteRamificationGroups_wildTopology

L166 ↗
EtaleFundamentalGroups.Inertia.actualAbsoluteRamificationGroups_wildTopology
Documentation

The wild topology is the SAME independently defined subgroup topology.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) (K : Type v) (Ω : Type w)
  [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
  [Field K] [Field Ω] [Algebra A K] [IsFractionRing A K]
  [Algebra K Ω] [Algebra A Ω] [IsScalarTower A K Ω] [IsSepClosure K Ω]
  (Q : Ideal (normalizationCommAlgCat A Ω).carrier) [Q.IsMaximal]
Lean source · full declaration
theorem actualAbsoluteRamificationGroups_wildTopology :
    TopologicalSpace.induced
        (fun σ : Subtype (actualAbsoluteRamificationGroups A K Ω Q).wild.carrier =>
          (show (actualAbsoluteRamificationGroups A K Ω Q).inertia.carrier from σ.val))
        (actualAbsoluteRamificationGroups A K Ω Q).inertiaTopology =
      actualNormalizationWildGroup_topologicalSpace A K Ω Q := rfl
theorem

actualAbsoluteRamificationDiagram_residueMorphism

L174 ↗
EtaleFundamentalGroups.Inertia.actualAbsoluteRamificationDiagram_residueMorphism
Documentation

The first sequence uses the SAME original absolute residue map.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) (K : Type v) (Ω : Type w)
  [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
  [Field K] [Field Ω] [Algebra A K] [IsFractionRing A K]
  [Algebra K Ω] [Algebra A Ω] [IsScalarTower A K Ω] [IsSepClosure K Ω]
  (Q : Ideal (normalizationCommAlgCat A Ω).carrier) [Q.IsMaximal]
Lean source · statement
theorem actualAbsoluteRamificationDiagram_residueMorphism :
    (actualAbsoluteRamificationDiagram A K Ω Q).residueMorphism =
      normalizationAbsoluteResidueMorphism A K Ω Q
theorem

actualAbsoluteRamificationDiagram_character

L179 ↗
EtaleFundamentalGroups.Inertia.actualAbsoluteRamificationDiagram_character
Documentation

The second sequence uses the SAME postcomposed canonical character.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) (K : Type v) (Ω : Type w)
  [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
  [Field K] [Field Ω] [Algebra A K] [IsFractionRing A K]
  [Algebra K Ω] [Algebra A Ω] [IsScalarTower A K Ω] [IsSepClosure K Ω]
  (Q : Ideal (normalizationCommAlgCat A Ω).carrier) [Q.IsMaximal]
Lean source · statement
theorem actualAbsoluteRamificationDiagram_character :
    (actualAbsoluteRamificationDiagram A K Ω Q).character =
      actualAbsoluteTameCharacterMorphism A K Ω Q
theorem

actualAbsoluteRamificationDiagram_rootsAction

L184 ↗
EtaleFundamentalGroups.Inertia.actualAbsoluteRamificationDiagram_rootsAction
Documentation

Its computed action is the SAME original action already compared in 6-C.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) (K : Type v) (Ω : Type w)
  [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
  [Field K] [Field Ω] [Algebra A K] [IsFractionRing A K]
  [Algebra K Ω] [Algebra A Ω] [IsScalarTower A K Ω] [IsSepClosure K Ω]
  (Q : Ideal (normalizationCommAlgCat A Ω).carrier) [Q.IsMaximal]
Lean source · statement
theorem actualAbsoluteRamificationDiagram_rootsAction
    (d : (normalizationDecompositionGroup A K Ω Q).carrier)
    (x : (normalizationSeparableRootsGroup A Ω Q).carrier) :
    (actualAbsoluteRamificationDiagram A K Ω Q).rootsAction d x =
      actualSeparableRootsAction_apply A K Ω Q d x
theorem

actualAbsoluteRamificationResidue_isAlgClosed

L192 ↗
EtaleFundamentalGroups.Inertia.actualAbsoluteRamificationResidue_isAlgClosed
Documentation

Close the literal quotient interface in the SAME stored actual residue field.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) (K : Type v) (Ω : Type w)
  [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
  [Field K] [Field Ω] [Algebra A K] [IsFractionRing A K]
  [Algebra K Ω] [Algebra A Ω] [IsScalarTower A K Ω] [IsSepClosure K Ω]
  (Q : Ideal (normalizationCommAlgCat A Ω).carrier) [Q.IsMaximal]
include K in
Lean source · statement
theorem actualAbsoluteRamificationResidue_isAlgClosed :
    IsAlgClosed (actualAbsoluteRamificationResidues A Ω Q).residue.α
theorem

actualAbsoluteRamificationResidueConclusions

L198 ↗
EtaleFundamentalGroups.Inertia.actualAbsoluteRamificationResidueConclusions
Documentation

The actual algebraicity and closedness suppliers prove all field-only output clauses.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) (K : Type v) (Ω : Type w)
  [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
  [Field K] [Field Ω] [Algebra A K] [IsFractionRing A K]
  [Algebra K Ω] [Algebra A Ω] [IsScalarTower A K Ω] [IsSepClosure K Ω]
  (Q : Ideal (normalizationCommAlgCat A Ω).carrier) [Q.IsMaximal]
include K in
Lean source · statement
theorem actualAbsoluteRamificationResidueConclusions :
    NativeAbsoluteResidueConclusions (actualAbsoluteRamificationResidues A Ω Q)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.