Module

FiniteFieldTensorDiagram.lean

Nyll.EtaleFundamentalGroups.GenericTensor.FilteredColimit.FiniteFieldTensorDiagram

6 declarations indexed from sourceView source ↗

Module documentation

Constant extensions as colimits with their native tensor actions

Finite intermediate fields index the actual algebras R ⊗[k] F. Their inclusions form a filtered diagram with colimit R ⊗[k] L for an algebraic extension L/k. We use the existing finite-coefficient tensor lift and flat tensor injectivity, retaining the native tensor actions at each point.

Imports11

Nyll.ValuedFieldTheory.Valuation.Completion.FiniteSubfieldTensor
Mathlib.Algebra.Category.Ring.FilteredColimits
Mathlib.Algebra.Category.Ring.Under.Basic
Mathlib.CategoryTheory.Category.Preorder
Mathlib.CategoryTheory.Filtered.Basic
Mathlib.CategoryTheory.Filtered.Connected
Mathlib.CategoryTheory.Limits.Constructions.Over.Connected
Mathlib.CategoryTheory.Limits.Types.Filtered
Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Mathlib.RingTheory.Flat.Basic
Mathlib.RingTheory.TensorProduct.Maps

Imported by4

abbrev

FiniteIntermediateFieldIndex

L40 ↗

EtaleFundamentalGroups.FiniteIntermediateFieldIndex

Documentation

The actual finite intermediate fields, ordered by inclusion.

Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
universe u
namespace EtaleFundamentalGroups
variable (k L : Type u) [Field k] [Field L] [Algebra k L]

Lean source · statement

abbrev FiniteIntermediateFieldIndex

instance

finiteIntermediateFieldIndexNonempty

L43 ↗

EtaleFundamentalGroups.finiteIntermediateFieldIndexNonempty

Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
universe u
namespace EtaleFundamentalGroups
variable (k L : Type u) [Field k] [Field L] [Algebra k L]

Lean source · statement

instance finiteIntermediateFieldIndexNonempty : Nonempty (FiniteIntermediateFieldIndex k L)

instance

finiteIntermediateFieldIndexDirected

L46 ↗

EtaleFundamentalGroups.finiteIntermediateFieldIndexDirected

Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
universe u
namespace EtaleFundamentalGroups
variable (k L : Type u) [Field k] [Field L] [Algebra k L]

Lean source · full declaration

instance finiteIntermediateFieldIndexDirected :
    IsDirectedOrder (FiniteIntermediateFieldIndex k L) where
  directed F E := by
    let : FiniteDimensional k F.val := F.property
    let : FiniteDimensional k E.val := E.property
    have hF : F.val ≤ F.val ⊔ E.val := le_sup_left
    have hE : E.val ≤ F.val ⊔ E.val := le_sup_right
    exact ⟨⟨F.val ⊔ E.val, inferInstance⟩, hF, hE⟩

def

finiteIntermediateFieldTensorDiagram

L58 ↗

EtaleFundamentalGroups.finiteIntermediateFieldTensorDiagram

Documentation

A filtered diagram using the native tensor product at every finite field.

Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
universe u
namespace EtaleFundamentalGroups
variable (k L : Type u) [Field k] [Field L] [Algebra k L]
variable (R : Type u) [CommRing R] [Algebra k R]

Lean source · full declaration

def finiteIntermediateFieldTensorDiagram :
    FiniteIntermediateFieldIndex k L ⥤ Under (CommRingCat.of R) where
  obj F := CommRingCat.mkUnder (CommRingCat.of R) (R ⊗[k] F.val.toSubalgebra)
  map {F E} f := (Algebra.TensorProduct.map (AlgHom.id R R)
    (Subalgebra.inclusion
      (show F.val.toSubalgebra ≤ E.val.toSubalgebra from f.le))).toUnder
  map_id F := by
    with_reducible_and_instances
      change AlgHom.toUnder (R := CommRingCat.of R)
        (Algebra.TensorProduct.map (AlgHom.id R R)
          (Subalgebra.inclusion (le_refl F.val.toSubalgebra))) = 𝟙 _
      rw [Subalgebra.inclusion_self, Algebra.TensorProduct.map_id]
      ext z
      simp only [AlgHom.toUnder_right, AlgHom.id_apply, Under.id_right, CommRingCat.id_apply]
  map_comp {F E G} f g := by
    have hi : (Subalgebra.inclusion
        (show E.val.toSubalgebra ≤ G.val.toSubalgebra from g.le)).comp
        (Subalgebra.inclusion
          (show F.val.toSubalgebra ≤ E.val.toSubalgebra from f.le)) =
        Subalgebra.inclusion
          (show F.val.toSubalgebra ≤ G.val.toSubalgebra from (f ≫ g).le) := by
      ext x
      rfl
    with_reducible_and_instances
      simp only [← AlgHom.toUnder_comp, ← Algebra.TensorProduct.map_id_comp, hi]

def

finiteIntermediateFieldTensorCocone

L85 ↗

EtaleFundamentalGroups.finiteIntermediateFieldTensorCocone

Documentation

The literal tensor maps of the finite-field inclusions into L.

Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
universe u
namespace EtaleFundamentalGroups
variable (k L : Type u) [Field k] [Field L] [Algebra k L]
variable (R : Type u) [CommRing R] [Algebra k R]

Lean source · full declaration

def finiteIntermediateFieldTensorCocone :
    Cocone (finiteIntermediateFieldTensorDiagram k L R) where
  pt := CommRingCat.mkUnder (CommRingCat.of R) (R ⊗[k] L)
  ι.app F := (Algebra.TensorProduct.map (AlgHom.id R R) F.val.toSubalgebra.val).toUnder
  ι.naturality F E f := by
    have hi : E.val.toSubalgebra.val.comp
        (Subalgebra.inclusion
          (show F.val.toSubalgebra ≤ E.val.toSubalgebra from f.le)) = F.val.toSubalgebra.val := by
      ext x
      rfl
    with_reducible_and_instances
      simp only [finiteIntermediateFieldTensorDiagram, ← AlgHom.toUnder_comp,
        ← Algebra.TensorProduct.map_id_comp, hi, CategoryTheory.Functor.const_obj_map]
      ext z
      rfl

def

finiteIntermediateFieldTensorCoconeIsColimit

L103 ↗

EtaleFundamentalGroups.finiteIntermediateFieldTensorCoconeIsColimit

Documentation

Finite-coefficient lifts give joint surjectivity; flatness detects equality at each actual finite-field tensor stage.

Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
universe u
namespace EtaleFundamentalGroups
variable (k L : Type u) [Field k] [Field L] [Algebra k L]
variable (R : Type u) [CommRing R] [Algebra k R]

Lean source · statement

def finiteIntermediateFieldTensorCoconeIsColimit [Algebra.IsAlgebraic k L] :
    IsColimit (finiteIntermediateFieldTensorCocone k L R)

Module documentation

Constant extensions as colimits with their native tensor actions

Declarations

FiniteIntermediateFieldIndex

finiteIntermediateFieldIndexNonempty

finiteIntermediateFieldIndexDirected

finiteIntermediateFieldTensorDiagram

finiteIntermediateFieldTensorCocone

finiteIntermediateFieldTensorCoconeIsColimit