NYLL
Module

NormalizationEtale.lean

Nyll.EtaleFundamentalGroups.Kummer.SelectedRoot.Prime.NormalizationEtale
7 declarations indexed from sourceView source ↗

Module documentation

Etaleness at the selected root prime

This file connects the literal selected-root localization to the complete higher-radical factor theorem. The first junction below refines a fixed post-root tensor component after extending the left field. It is the exact surjective map needed to keep both the original global component and a chosen completed component fixed.

Imports6
Imported by4

Declarations

def

genericTensorRefineChosenComponentMap

L44 ↗
EtaleFundamentalGroups.Kummer.genericTensorRefineChosenComponentMap
Documentation

The canonical map from the original tensor product to the tensor product with a fixed intermediate component. It simultaneously extends the left field K₁ → F and applies the quotient selecting m on the right.

Source context 11 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups.Kummer
universe uK₀ uK₁ uF uL
section ComponentRefinement
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]
Lean source · statement
def genericTensorRefineChosenComponentMap
    (m : Ideal (K₁ ⊗[K₀] L)) [m.IsMaximal] :
    (F ⊗[K₀] L) →ₐ[F]
      (F ⊗[K₁] GenericTensorFieldComponent m)
theorem

genericTensorRefineChosenComponentMap_tmul

L62 ↗
EtaleFundamentalGroups.Kummer.genericTensorRefineChosenComponentMap_tmul
Source context 11 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups.Kummer
universe uK₀ uK₁ uF uL
section ComponentRefinement
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]
Lean source · statement
theorem genericTensorRefineChosenComponentMap_tmul
    (m : Ideal (K₁ ⊗[K₀] L)) [m.IsMaximal]
    (x : F) (y : L) :
    genericTensorRefineChosenComponentMap m (x ⊗ₜ[K₀] y) =
      x ⊗ₜ[K₁]
        (Ideal.Quotient.mk m
          ((1 : K₁) ⊗ₜ[K₀] y))
theorem

genericTensorRefineChosenComponentMap_surjective

L73 ↗
EtaleFundamentalGroups.Kummer.genericTensorRefineChosenComponentMap_surjective
Documentation

The component-refinement map is onto.

Source context 11 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups.Kummer
universe uK₀ uK₁ uF uL
section ComponentRefinement
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]
Lean source · statement
theorem genericTensorRefineChosenComponentMap_surjective
    (m : Ideal (K₁ ⊗[K₀] L)) [m.IsMaximal] :
    Function.Surjective
      (genericTensorRefineChosenComponentMap
        (K₀ := K₀) (K₁ := K₁) (F := F) (L := L) m)
def

genericTensorRefineChosenComponentIdeal

L111 ↗
EtaleFundamentalGroups.Kummer.genericTensorRefineChosenComponentIdeal
Documentation

Pulling back a maximal completed component along the refinement map selects a maximal component of the original completed tensor product.

Source context 11 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups.Kummer
universe uK₀ uK₁ uF uL
section ComponentRefinement
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]
Lean source · statement
def genericTensorRefineChosenComponentIdeal
    (m : Ideal (K₁ ⊗[K₀] L)) [m.IsMaximal]
    (q : Ideal (F ⊗[K₁] GenericTensorFieldComponent m))
    [q.IsMaximal] : Ideal (F ⊗[K₀] L)
theorem

genericTensorRefineChosenComponentIdeal_isMaximal

L119 ↗
EtaleFundamentalGroups.Kummer.genericTensorRefineChosenComponentIdeal_isMaximal
Source context 11 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups.Kummer
universe uK₀ uK₁ uF uL
section ComponentRefinement
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]
Lean source · statement
theorem genericTensorRefineChosenComponentIdeal_isMaximal
    (m : Ideal (K₁ ⊗[K₀] L)) [m.IsMaximal]
    (q : Ideal (F ⊗[K₁] GenericTensorFieldComponent m))
    [q.IsMaximal] :
    (genericTensorRefineChosenComponentIdeal m q).IsMaximal
theorem

genericTensorRefineChosenComponentIdeal_tower_second

L137 ↗
EtaleFundamentalGroups.Kummer.genericTensorRefineChosenComponentIdeal_tower_second
Documentation

Refining the contracted component by the second-stage component selected by m recovers the original ideal m literally.

Source context 11 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups.Kummer
universe uK₀ uK₁ uF uL
section ComponentRefinement
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]
Lean source · full declaration
theorem genericTensorRefineChosenComponentIdeal_tower_second
    [FiniteDimensional K₁ F]
    (m : Ideal (F ⊗[K₀] L)) [m.IsMaximal] :
    let n := genericTensorTowerIntermediateIdeal
      (K := K₀) (F := K₁) (F' := F) (L := L) m
    letI : n.IsMaximal :=
      genericTensorTowerIntermediateIdeal_isMaximal
        (K := K₀) (F := K₁) (F' := F) (L := L) m
    let q := genericTensorTowerSecondIdeal
      (K := K₀) (F := K₁) (F' := F) (L := L) m
    letI : q.IsMaximal :=
      genericTensorTowerSecondIdeal_isMaximal
        (K := K₀) (F := K₁) (F' := F) (L := L) m
    genericTensorRefineChosenComponentIdeal
      (K₀ := K₀) (K₁ := K₁) (F := F) (L := L) n q = m := by
  dsimp only
  let n := genericTensorTowerIntermediateIdeal
    (K := K₀) (F := K₁) (F' := F) (L := L) m
  let : n.IsMaximal :=
    genericTensorTowerIntermediateIdeal_isMaximal
      (K := K₀) (F := K₁) (F' := F) (L := L) m
  let q := genericTensorTowerSecondIdeal
    (K := K₀) (F := K₁) (F' := F) (L := L) m
  let : q.IsMaximal :=
    genericTensorTowerSecondIdeal_isMaximal
      (K := K₀) (F := K₁) (F' := F) (L := L) m
  have hcomp (z : F ⊗[K₀] L) :
      genericTensorTowerSecondComponentMap
          (K := K₀) (F := K₁) (F' := F) (L := L) m
          (genericTensorRefineChosenComponentMap
            (K₀ := K₀) (K₁ := K₁) (F := F) (L := L) n z) =
        Ideal.Quotient.mk m z := by
    induction z using TensorProduct.inductionOn with
    | tmul x y =>
        rw [genericTensorRefineChosenComponentMap_tmul]
        change genericTensorFieldComponentLeft m x *
            genericTensorTowerIntermediateComponentMap
              (K := K₀) (F := K₁) (F' := F) (L := L) m
              (Ideal.Quotient.mk n ((1 : K₁) ⊗ₜ[K₀] y)) =
          Ideal.Quotient.mk m (x ⊗ₜ[K₀] y)
        rw [genericTensorTowerIntermediateComponentMap_mk]
        rw [genericTensorFieldComponentLeft_apply]
        rw [← map_mul]
        congr 1
        simp [genericTensorTowerMap]
    | add x y hx hy => simpa only [map_add] using congrArg₂ (· + ·) hx hy
  ext z
  change
    (Ideal.Quotient.mkₐ F q)
        (genericTensorRefineChosenComponentMap
          (K₀ := K₀) (K₁ := K₁) (F := F) (L := L) n z) = 0 ↔
      z ∈ m
  change
    Ideal.Quotient.mk q
        (genericTensorRefineChosenComponentMap
          (K₀ := K₀) (K₁ := K₁) (F := F) (L := L) n z) = 0 ↔
      z ∈ m
  rw [Ideal.Quotient.eq_zero_iff_mem]
  change
    genericTensorTowerSecondComponentMap
        (K := K₀) (F := K₁) (F' := F) (L := L) m
        (genericTensorRefineChosenComponentMap
          (K₀ := K₀) (K₁ := K₁) (F := F) (L := L) n z) = 0 ↔
      z ∈ m
  rw [hcomp]
  exact Ideal.Quotient.eq_zero_iff_mem
def

genericTensorRefineChosenComponentAlgEquiv

L206 ↗
EtaleFundamentalGroups.Kummer.genericTensorRefineChosenComponentAlgEquiv
Documentation

The pulled-back component is the same literal quotient field as the chosen completed component.

Source context 11 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups.Kummer
universe uK₀ uK₁ uF uL
section ComponentRefinement
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]
Lean source · full declaration
def genericTensorRefineChosenComponentAlgEquiv
    (m : Ideal (K₁ ⊗[K₀] L)) [m.IsMaximal]
    (q : Ideal (F ⊗[K₁] GenericTensorFieldComponent m))
    [q.IsMaximal] :
    let n := genericTensorRefineChosenComponentIdeal m q
    letI : n.IsMaximal :=
      genericTensorRefineChosenComponentIdeal_isMaximal m q
    GenericTensorFieldComponent n ≃ₐ[F]
      GenericTensorFieldComponent q := by
  dsimp only
  let g : (F ⊗[K₀] L) →ₐ[F]
      GenericTensorFieldComponent q :=
    (Ideal.Quotient.mkₐ F q).comp
      (genericTensorRefineChosenComponentMap
        (K₀ := K₀) (K₁ := K₁) (F := F) (L := L) m)
  have hg : Function.Surjective g :=
    Ideal.Quotient.mk_surjective.comp
      (genericTensorRefineChosenComponentMap_surjective
        (K₀ := K₀) (K₁ := K₁) (F := F) (L := L) m)
  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.