NYLL
Module

ComponentRestrictBase.lean

Nyll.EtaleFundamentalGroups.GenericTensor.ComponentRestrictBase
6 declarations indexed from sourceView source ↗

Module documentation

Restricting the base of a selected generic tensor component

For field towers K₀ → K₁ → F and K₀ → K₁ → L, the canonical balancing map

F ⊗[K₀] L → F ⊗[K₁] L

is onto. Consequently a fixed literal maximal component on the right is the same quotient field as the component cut out by the kernel of the composite quotient map on the left. This keeps completed chosen components fixed while passing to the earlier field used for a common degree bound.

Imports1
Imported by3

Declarations

def

genericTensorRestrictBaseMap

L41 ↗
EtaleFundamentalGroups.genericTensorRestrictBaseMap
Documentation

The canonical surjection imposing the additional K₁-balancing relations on a tensor product originally formed over K₀.

Source context 11 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uK₀ uK₁ uF uL
variable {K₀ : Type uK₀} {K₁ : Type uK₁}
variable {F : Type uF} {L : Type uL}
variable [Field K₀] [Field K₁] [Field F] [Field L]
variable [Algebra K₀ K₁] [Algebra K₁ F] [Algebra K₀ F]
variable [IsScalarTower K₀ K₁ F]
variable [Algebra K₀ L] [Algebra K₁ L]
variable [IsScalarTower K₀ K₁ L]
Lean source · statement
def genericTensorRestrictBaseMap :
    (F ⊗[K₀] L) →ₐ[F] (F ⊗[K₁] L)
theorem

genericTensorRestrictBaseMap_tmul

L51 ↗
EtaleFundamentalGroups.genericTensorRestrictBaseMap_tmul
Source context 11 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uK₀ uK₁ uF uL
variable {K₀ : Type uK₀} {K₁ : Type uK₁}
variable {F : Type uF} {L : Type uL}
variable [Field K₀] [Field K₁] [Field F] [Field L]
variable [Algebra K₀ K₁] [Algebra K₁ F] [Algebra K₀ F]
variable [IsScalarTower K₀ K₁ F]
variable [Algebra K₀ L] [Algebra K₁ L]
variable [IsScalarTower K₀ K₁ L]
Lean source · statement
theorem genericTensorRestrictBaseMap_tmul (x : F) (y : L) :
    genericTensorRestrictBaseMap (K₀ := K₀) (K₁ := K₁)
        (x ⊗ₜ[K₀] y) =
      x ⊗ₜ[K₁] y
theorem

genericTensorRestrictBaseMap_surjective

L59 ↗
EtaleFundamentalGroups.genericTensorRestrictBaseMap_surjective
Documentation

The base-restriction tensor map is surjective.

Source context 11 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uK₀ uK₁ uF uL
variable {K₀ : Type uK₀} {K₁ : Type uK₁}
variable {F : Type uF} {L : Type uL}
variable [Field K₀] [Field K₁] [Field F] [Field L]
variable [Algebra K₀ K₁] [Algebra K₁ F] [Algebra K₀ F]
variable [IsScalarTower K₀ K₁ F]
variable [Algebra K₀ L] [Algebra K₁ L]
variable [IsScalarTower K₀ K₁ L]
Lean source · statement
theorem genericTensorRestrictBaseMap_surjective :
    Function.Surjective
      (genericTensorRestrictBaseMap
        (K₀ := K₀) (K₁ := K₁) (F := F) (L := L))
def

genericTensorRestrictBaseIdeal

L73 ↗
EtaleFundamentalGroups.genericTensorRestrictBaseIdeal
Documentation

The maximal ideal on the earlier-base tensor product selecting a fixed maximal component after imposing the K₁-balancing relations.

Source context 11 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uK₀ uK₁ uF uL
variable {K₀ : Type uK₀} {K₁ : Type uK₁}
variable {F : Type uF} {L : Type uL}
variable [Field K₀] [Field K₁] [Field F] [Field L]
variable [Algebra K₀ K₁] [Algebra K₁ F] [Algebra K₀ F]
variable [IsScalarTower K₀ K₁ F]
variable [Algebra K₀ L] [Algebra K₁ L]
variable [IsScalarTower K₀ K₁ L]
Lean source · statement
def genericTensorRestrictBaseIdeal
    (m : Ideal (F ⊗[K₁] L)) [m.IsMaximal] :
    Ideal (F ⊗[K₀] L)
theorem

genericTensorRestrictBaseIdeal_isMaximal

L83 ↗
EtaleFundamentalGroups.genericTensorRestrictBaseIdeal_isMaximal
Documentation

The pulled-back component ideal is maximal because its defining map is onto the same fixed quotient field.

Source context 11 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uK₀ uK₁ uF uL
variable {K₀ : Type uK₀} {K₁ : Type uK₁}
variable {F : Type uF} {L : Type uL}
variable [Field K₀] [Field K₁] [Field F] [Field L]
variable [Algebra K₀ K₁] [Algebra K₁ F] [Algebra K₀ F]
variable [IsScalarTower K₀ K₁ F]
variable [Algebra K₀ L] [Algebra K₁ L]
variable [IsScalarTower K₀ K₁ L]
Lean source · statement
theorem genericTensorRestrictBaseIdeal_isMaximal
    (m : Ideal (F ⊗[K₁] L)) [m.IsMaximal] :
    (genericTensorRestrictBaseIdeal
      (K₀ := K₀) (K₁ := K₁) (F := F) (L := L) m).IsMaximal
def

genericTensorRestrictBaseComponentAlgEquiv

L99 ↗
EtaleFundamentalGroups.genericTensorRestrictBaseComponentAlgEquiv
Documentation

Restricting the tensor base does not change the selected quotient-field component.

Source context 11 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uK₀ uK₁ uF uL
variable {K₀ : Type uK₀} {K₁ : Type uK₁}
variable {F : Type uF} {L : Type uL}
variable [Field K₀] [Field K₁] [Field F] [Field L]
variable [Algebra K₀ K₁] [Algebra K₁ F] [Algebra K₀ F]
variable [IsScalarTower K₀ K₁ F]
variable [Algebra K₀ L] [Algebra K₁ L]
variable [IsScalarTower K₀ K₁ L]
Lean source · full declaration
def genericTensorRestrictBaseComponentAlgEquiv
    (m : Ideal (F ⊗[K₁] L)) [m.IsMaximal] :
    let n := genericTensorRestrictBaseIdeal
      (K₀ := K₀) (K₁ := K₁) (F := F) (L := L) m
    letI : n.IsMaximal := genericTensorRestrictBaseIdeal_isMaximal m
    GenericTensorFieldComponent n ≃ₐ[F] GenericTensorFieldComponent m := by
  dsimp only
  let g : (F ⊗[K₀] L) →ₐ[F] GenericTensorFieldComponent m :=
    (Ideal.Quotient.mkₐ F m).comp
      (genericTensorRestrictBaseMap
        (K₀ := K₀) (K₁ := K₁) (F := F) (L := L))
  have hg : Function.Surjective g :=
    Ideal.Quotient.mk_surjective.comp
      (genericTensorRestrictBaseMap_surjective
        (K₀ := K₀) (K₁ := K₁) (F := F) (L := L))
  exact Ideal.quotientKerAlgEquivOfSurjective hg

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