Module

GenericTensorComponent.lean

Nyll.EtaleFundamentalGroups.FiniteEtale.BaseChange.GenericTensorComponent

2 declarations indexed from sourceView source ↗

Module documentation

Fixed tensor components after finite-etale base change

Let T / A be finite etale and let E / F be its generic fibre, where F and E are fraction fields of A and T. After replacing A by a normal domain B with fraction field K, a specified maximal ideal of K tensor[F] E selects an actual field component. The normalization of B in that same component is finite etale.

This is the component-preserving form used on the complement of the boundary: the maximal ideal is data produced by the global chosen component, rather than an abstract field or a postulated comparison isomorphism.

Imports3

Imported by5

theorem

integralClosure_genericTensorFieldComponent_etale_of_finiteEtale_baseChange

L39 ↗

EtaleFundamentalGroups.integralClosure_genericTensorFieldComponent_etale_of_finiteEtale_baseChange

Documentation

A specified generic tensor component of a finite-etale algebra remains finite etale after normalization over a normal base change.

The generic-fibre equivalence, the iterated base-change equivalence, and the surjection to the selected quotient component are all constructed in the proof.

Source context 4 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uA uB uT uF uE uK uR uC

Lean source · full declaration

theorem integralClosure_genericTensorFieldComponent_etale_of_finiteEtale_baseChange
    {A : Type uA} {B : Type uB} {T : Type uT}
    {F : Type uF} {E : Type uE} {K : Type uK}
    [CommRing A] [IsDomain A]
    [CommRing B] [IsDomain B] [IsIntegrallyClosed B] [Algebra A B]
    [CommRing T] [IsDomain T] [Algebra A T]
    [Module.Finite A T] [Algebra.Etale A T]
    [Field F] [Algebra A F] [IsFractionRing A F]
    [Field E] [Algebra T E] [IsFractionRing T E]
    [Algebra A E] [IsScalarTower A T E]
    [Algebra F E] [IsScalarTower A F E]
    [Field K] [Algebra B K] [IsFractionRing B K]
    [Algebra A K] [Algebra F K]
    [IsScalarTower A B K] [IsScalarTower A F K]
    (m : Ideal (K ⊗[F] E)) [m.IsMaximal] :
    let M := GenericTensorFieldComponent m
    Algebra.Etale B (integralClosure B M) := by
  let M := GenericTensorFieldComponent m
  let : IsScalarTower B K M := inferInstance
  let eGeneric : (F ⊗[A] T) ≃ₐ[F] E :=
    finiteGenericFiberAlgEquiv (R := A) (C := T) (K := F) (E := E)
  let eFactor : (K ⊗[A] T) ≃ₐ[K] (K ⊗[F] E) :=
    iteratedGenericFiberEquiv A F K T E eGeneric
  let quotient : (K ⊗[F] E) →ₐ[K] M :=
    Ideal.Quotient.mkₐ K m
  let componentMap : (K ⊗[A] T) →ₐ[K] M :=
    quotient.comp eFactor.toAlgHom
  apply integralClosure_etale_of_surjective_reassociatedGenericFiber
    (A := A) (B := B) (T := T) (K := K) componentMap
  exact Ideal.Quotient.mk_surjective.comp eFactor.surjective

theorem

integralClosure_genericTensorFieldComponent_etale_of_away_isUnit

L79 ↗

EtaleFundamentalGroups.integralClosure_genericTensorFieldComponent_etale_of_away_isUnit

Documentation

Away-branch form of integralClosure_genericTensorFieldComponent_etale_of_finiteEtale_baseChange.

If f is a unit on the new normal base B, the map from R to B extends canonically across R[1/f]. The induced embedding of its fraction field into Frac(B) and all scalar towers are constructed in the proof. A specified maximal ideal of the resulting generic tensor product therefore gives an etale normalization over B without postulating a field-component comparison.