Module

IntermediateFieldDiagram.lean

Nyll.EtaleFundamentalGroups.GenericTensor.FilteredColimit.IntermediateFieldDiagram

3 declarations indexed from sourceView source ↗

Module documentation

A field extension as a filtered colimit of actual intermediate fields

The finite subsets of an extension field index the intermediate fields they generate. The transition maps and cocone maps are the literal inclusions. For an algebraic extension these fields are finite dimensional, by the existing IntermediateField.finiteDimensional_adjoin theorem. The construction uses one universe for the rings and index, as required by finite-presentation descent.

Imports8

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.Defs

Imported by2

def

intermediateFieldAdjoinDiagram

L41 ↗

EtaleFundamentalGroups.intermediateFieldAdjoinDiagram

Documentation

The actual intermediate fields generated by finite sets of coefficients.

Source context 6 commands

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

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

Lean source · full declaration

def intermediateFieldAdjoinDiagram : Finset L ⥤ Under (CommRingCat.of k) where
  obj s := CommRingCat.mkUnder (CommRingCat.of k) (IntermediateField.adjoin k (s : Set L))
  map {s t} f := (IntermediateField.inclusion
    (IntermediateField.adjoin.mono k (s : Set L) (t : Set L)
      (Finset.coe_subset.mpr f.le))).toUnder
  map_id s := by
    ext x
    rfl
  map_comp f g := by
    ext x
    rfl

def

intermediateFieldAdjoinCocone

L54 ↗

EtaleFundamentalGroups.intermediateFieldAdjoinCocone

Documentation

The coefficient inclusions into the original extension field.

Source context 6 commands

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

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

Lean source · full declaration

def intermediateFieldAdjoinCocone : Cocone (intermediateFieldAdjoinDiagram k L) where
  pt := CommRingCat.mkUnder (CommRingCat.of k) L
  ι.app s := (IntermediateField.adjoin k (s : Set L)).val.toUnder
  ι.naturality s t f := by
    ext x
    rfl

def

intermediateFieldAdjoinCoconeIsColimit

L63 ↗

EtaleFundamentalGroups.intermediateFieldAdjoinCoconeIsColimit

Documentation

Every coefficient belongs to a singly generated intermediate field, and inclusion into the extension detects equality at each stage.

Source context 6 commands

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

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

Lean source · statement

def intermediateFieldAdjoinCoconeIsColimit :
    IsColimit (intermediateFieldAdjoinCocone k L)

Module documentation

A field extension as a filtered colimit of actual intermediate fields

Declarations

intermediateFieldAdjoinDiagram

intermediateFieldAdjoinCocone

intermediateFieldAdjoinCoconeIsColimit