Module

FractionFieldTensorComponent.lean

Nyll.EtaleFundamentalGroups.FiniteEtale.ChosenPrime.FractionFieldTensorComponent

11 declarations indexed from sourceView source ↗

Module documentation

Field-tensor coordinates for an actual chosen generic component

Let C / R be finite and let L be a field over the fraction field of R. The literal generic algebra C ⊗[R] L is canonically the field tensor product

FractionRing C ⊗[FractionRing R] L.

This file transports a specified maximal component, a normalization prime, and its prime localization across that canonical comparison. In particular, a component produced by EtaleChosenPrimeLocalFactor is not reselected after passing to fraction fields.

Imports3

Imported by2

def

finiteBaseFractionRingAlgebra

L44 ↗

EtaleFundamentalGroups.finiteBaseFractionRingAlgebra

Documentation

The fraction-field extension induced by a faithful finite map R → C.

Source context 10 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uR uC uL
variable {R : Type uR} {C : Type uC} {L : Type uL}
variable [CommRing R] [IsDomain R]
variable [CommRing C] [IsDomain C]
variable [Algebra R C] [FaithfulSMul R C]
variable [Field L] [Algebra R L]
variable [Algebra (FractionRing R) L]

Lean source · statement

def finiteBaseFractionRingAlgebra :
    Algebra (FractionRing R) (FractionRing C)

instance

finiteBaseFractionRingAlgebraInstance

L50 ↗

EtaleFundamentalGroups.finiteBaseFractionRingAlgebraInstance

Source context 10 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uR uC uL
variable {R : Type uR} {C : Type uC} {L : Type uL}
variable [CommRing R] [IsDomain R]
variable [CommRing C] [IsDomain C]
variable [Algebra R C] [FaithfulSMul R C]
variable [Field L] [Algebra R L]
variable [Algebra (FractionRing R) L]

Lean source · statement

instance finiteBaseFractionRingAlgebraInstance :
    Algebra (FractionRing R) (FractionRing C)

def

finiteBaseFractionFieldTensorAlgebra

L57 ↗

EtaleFundamentalGroups.finiteBaseFractionFieldTensorAlgebra

Documentation

The scalar action of C on the field tensor product is the literal left-factor action through FractionRing C.

Source context 11 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uR uC uL
variable {R : Type uR} {C : Type uC} {L : Type uL}
variable [CommRing R] [IsDomain R]
variable [CommRing C] [IsDomain C]
variable [Algebra R C] [FaithfulSMul R C]
variable [Field L] [Algebra R L]
variable [Algebra (FractionRing R) L]
local instance finiteBaseFractionRingAlgebraInstance :
    Algebra (FractionRing R) (FractionRing C) :=
  finiteBaseFractionRingAlgebra (R := R) (C := C)

Lean source · full declaration

def finiteBaseFractionFieldTensorAlgebra :
    let K := FractionRing R
    let E := FractionRing C
    Algebra C (E ⊗[K] L) := by
  dsimp only
  exact genericTensorProductLeftScalarAlgebra
    (R := C) (K := FractionRing R) (F := FractionRing C) (L := L)

def

finiteBaseFractionFieldTensorAlgEquiv

L70 ↗

EtaleFundamentalGroups.finiteBaseFractionFieldTensorAlgEquiv

Documentation

Canonical comparison between the literal finite generic fibre and the tensor product of the two fraction fields.

It is linear over C: on the target, C acts through the left copy of FractionRing C.

Source context 11 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uR uC uL
variable {R : Type uR} {C : Type uC} {L : Type uL}
variable [CommRing R] [IsDomain R]
variable [CommRing C] [IsDomain C]
variable [Algebra R C] [FaithfulSMul R C]
variable [Field L] [Algebra R L]
variable [Algebra (FractionRing R) L]
local instance finiteBaseFractionRingAlgebraInstance :
    Algebra (FractionRing R) (FractionRing C) :=
  finiteBaseFractionRingAlgebra (R := R) (C := C)

Lean source · full declaration

def finiteBaseFractionFieldTensorAlgEquiv
    [Module.Finite R C]
    [IsScalarTower R (FractionRing R) L] :
    let K := FractionRing R
    let E := FractionRing C
    letI : Algebra C (E ⊗[K] L) :=
      finiteBaseFractionFieldTensorAlgebra (R := R) (C := C) (L := L)
    (C ⊗[R] L) ≃ₐ[C] (E ⊗[K] L) := by
  dsimp only
  let K := FractionRing R
  let E := FractionRing C
  letI : IsScalarTower R K E :=
    FractionRing.isScalarTower_liftAlgebra R E
  letI : Algebra C (E ⊗[K] L) :=
    finiteBaseFractionFieldTensorAlgebra (R := R) (C := C) (L := L)
  letI : Algebra L (C ⊗[R] L) :=
    Algebra.TensorProduct.rightAlgebra
  letI : Algebra L (E ⊗[K] L) :=
    Algebra.TensorProduct.rightAlgebra
  let eGeneric : (K ⊗[R] C) ≃ₐ[K] E :=
    finiteGenericFiberAlgEquiv
      (R := R) (C := C) (K := K) (E := E)
  let eL : (C ⊗[R] L) ≃ₐ[L] (E ⊗[K] L) :=
    (Algebra.TensorProduct.commRight R L C).symm |>.trans
      (iteratedGenericFiberEquiv R K L C E eGeneric) |>.trans
      (Algebra.TensorProduct.commRight K L E)
  refine
    { toRingEquiv := eL.toRingEquiv
      commutes' := ?_ }
  intro c
  change eL (c ⊗ₜ[R] (1 : L)) =
    (algebraMap C E c) ⊗ₜ[K] (1 : L)
  simp [eL, eGeneric, iteratedGenericFiberEquiv]

def

finiteBaseFractionFieldTensorIdeal

L106 ↗

EtaleFundamentalGroups.finiteBaseFractionFieldTensorIdeal

Documentation

The literal maximal ideal of the fraction-field tensor product obtained from the already selected component of C ⊗[R] L.

Source context 11 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uR uC uL
variable {R : Type uR} {C : Type uC} {L : Type uL}
variable [CommRing R] [IsDomain R]
variable [CommRing C] [IsDomain C]
variable [Algebra R C] [FaithfulSMul R C]
variable [Field L] [Algebra R L]
variable [Algebra (FractionRing R) L]
local instance finiteBaseFractionRingAlgebraInstance :
    Algebra (FractionRing R) (FractionRing C) :=
  finiteBaseFractionRingAlgebra (R := R) (C := C)

Lean source · statement

def finiteBaseFractionFieldTensorIdeal
    [Module.Finite R C]
    [IsScalarTower R (FractionRing R) L]
    (m : Ideal (C ⊗[R] L)) :
    Ideal ((FractionRing C) ⊗[FractionRing R] L)

theorem

finiteBaseFractionFieldTensorIdeal_isMaximal

L119 ↗

EtaleFundamentalGroups.finiteBaseFractionFieldTensorIdeal_isMaximal

Documentation

The transported fraction-field tensor ideal is maximal.

Source context 11 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uR uC uL
variable {R : Type uR} {C : Type uC} {L : Type uL}
variable [CommRing R] [IsDomain R]
variable [CommRing C] [IsDomain C]
variable [Algebra R C] [FaithfulSMul R C]
variable [Field L] [Algebra R L]
variable [Algebra (FractionRing R) L]
local instance finiteBaseFractionRingAlgebraInstance :
    Algebra (FractionRing R) (FractionRing C) :=
  finiteBaseFractionRingAlgebra (R := R) (C := C)

Lean source · statement

theorem finiteBaseFractionFieldTensorIdeal_isMaximal
    [Module.Finite R C]
    [IsScalarTower R (FractionRing R) L]
    (m : Ideal (C ⊗[R] L)) [m.IsMaximal] :
    (finiteBaseFractionFieldTensorIdeal
      (R := R) (C := C) (L := L) m).IsMaximal

def

finiteBaseFractionFieldTensorComponentAlgEquiv

L136 ↗

EtaleFundamentalGroups.finiteBaseFractionFieldTensorComponentAlgEquiv

Documentation

The actual quotient component produced before fieldification is canonically the literal generic tensor component after fieldification.

Source context 11 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uR uC uL
variable {R : Type uR} {C : Type uC} {L : Type uL}
variable [CommRing R] [IsDomain R]
variable [CommRing C] [IsDomain C]
variable [Algebra R C] [FaithfulSMul R C]
variable [Field L] [Algebra R L]
variable [Algebra (FractionRing R) L]
local instance finiteBaseFractionRingAlgebraInstance :
    Algebra (FractionRing R) (FractionRing C) :=
  finiteBaseFractionRingAlgebra (R := R) (C := C)

Lean source · full declaration

def finiteBaseFractionFieldTensorComponentAlgEquiv
    [Module.Finite R C]
    [IsScalarTower R (FractionRing R) L]
    (m : Ideal (C ⊗[R] L)) [m.IsMaximal] :
    let n := finiteBaseFractionFieldTensorIdeal
      (R := R) (C := C) (L := L) m
    letI : n.IsMaximal :=
      finiteBaseFractionFieldTensorIdeal_isMaximal
        (R := R) (C := C) (L := L) m
    letI : Algebra C (GenericTensorFieldComponent n) :=
      genericTensorFieldComponentLeftScalarAlgebra (R := C) n
    FiniteEtaleGenericFiberComponent m ≃ₐ[C]
      GenericTensorFieldComponent n := by
  dsimp only
  let T := (FractionRing C) ⊗[FractionRing R] L
  letI : Algebra C T :=
    finiteBaseFractionFieldTensorAlgebra (R := R) (C := C) (L := L)
  let E : (C ⊗[R] L) ≃ₐ[C] T :=
    finiteBaseFractionFieldTensorAlgEquiv
      (R := R) (C := C) (L := L)
  let n : Ideal T := finiteBaseFractionFieldTensorIdeal
    (R := R) (C := C) (L := L) m
  letI : n.IsMaximal :=
    finiteBaseFractionFieldTensorIdeal_isMaximal
      (R := R) (C := C) (L := L) m
  letI : Algebra C (GenericTensorFieldComponent n) :=
    genericTensorFieldComponentLeftScalarAlgebra (R := C) n
  let qE : ((C ⊗[R] L) ⧸ m) ≃+* (T ⧸ n) :=
    Ideal.quotientEquiv m n E.toRingEquiv rfl
  exact AlgEquiv.ofRingEquiv (f := qE) fun c ↦ by
    change qE (Ideal.Quotient.mk m
      (algebraMap C (C ⊗[R] L) c)) =
        algebraMap C (T ⧸ n) c
    dsimp only [qE]
    rw [Ideal.quotientEquiv_mk m n E.toRingEquiv rfl]
    exact congrArg (Ideal.Quotient.mk n) (E.commutes c)

def

finiteBaseFractionFieldTensorIntegralClosureAlgEquiv

L175 ↗

EtaleFundamentalGroups.finiteBaseFractionFieldTensorIntegralClosureAlgEquiv

Documentation

Integral closures in the two presentations of the same actual component are canonically equivalent.

Source context 11 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uR uC uL
variable {R : Type uR} {C : Type uC} {L : Type uL}
variable [CommRing R] [IsDomain R]
variable [CommRing C] [IsDomain C]
variable [Algebra R C] [FaithfulSMul R C]
variable [Field L] [Algebra R L]
variable [Algebra (FractionRing R) L]
local instance finiteBaseFractionRingAlgebraInstance :
    Algebra (FractionRing R) (FractionRing C) :=
  finiteBaseFractionRingAlgebra (R := R) (C := C)

Lean source · full declaration

def finiteBaseFractionFieldTensorIntegralClosureAlgEquiv
    [Module.Finite R C]
    [IsScalarTower R (FractionRing R) L]
    (m : Ideal (C ⊗[R] L)) [m.IsMaximal] :
    let n := finiteBaseFractionFieldTensorIdeal
      (R := R) (C := C) (L := L) m
    letI : n.IsMaximal :=
      finiteBaseFractionFieldTensorIdeal_isMaximal
        (R := R) (C := C) (L := L) m
    letI : Algebra C (GenericTensorFieldComponent n) :=
      genericTensorFieldComponentLeftScalarAlgebra (R := C) n
    integralClosure C (FiniteEtaleGenericFiberComponent m) ≃ₐ[C]
      integralClosure C (GenericTensorFieldComponent n) := by
  dsimp only
  let n := finiteBaseFractionFieldTensorIdeal
    (R := R) (C := C) (L := L) m
  letI : n.IsMaximal :=
    finiteBaseFractionFieldTensorIdeal_isMaximal
      (R := R) (C := C) (L := L) m
  letI : Algebra C (GenericTensorFieldComponent n) :=
    genericTensorFieldComponentLeftScalarAlgebra (R := C) n
  let E := finiteBaseFractionFieldTensorComponentAlgEquiv
    (R := R) (C := C) (L := L) m
  exact E.mapIntegralClosure

def

finiteBaseFractionFieldTensorIntegralClosurePrime

L202 ↗

EtaleFundamentalGroups.finiteBaseFractionFieldTensorIntegralClosurePrime

Documentation

The normalization prime obtained by literal transport to the fraction-field tensor component.

Source context 11 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uR uC uL
variable {R : Type uR} {C : Type uC} {L : Type uL}
variable [CommRing R] [IsDomain R]
variable [CommRing C] [IsDomain C]
variable [Algebra R C] [FaithfulSMul R C]
variable [Field L] [Algebra R L]
variable [Algebra (FractionRing R) L]
local instance finiteBaseFractionRingAlgebraInstance :
    Algebra (FractionRing R) (FractionRing C) :=
  finiteBaseFractionRingAlgebra (R := R) (C := C)

Lean source · full declaration

def finiteBaseFractionFieldTensorIntegralClosurePrime
    [Module.Finite R C]
    [IsScalarTower R (FractionRing R) L]
    (m : Ideal (C ⊗[R] L)) [m.IsMaximal]
    (q : Ideal (integralClosure C
      (FiniteEtaleGenericFiberComponent m))) :
    let n := finiteBaseFractionFieldTensorIdeal
      (R := R) (C := C) (L := L) m
    letI : n.IsMaximal :=
      finiteBaseFractionFieldTensorIdeal_isMaximal
        (R := R) (C := C) (L := L) m
    letI : Algebra C (GenericTensorFieldComponent n) :=
      genericTensorFieldComponentLeftScalarAlgebra (R := C) n
    Ideal (integralClosure C (GenericTensorFieldComponent n)) := by
  dsimp only
  exact q.map
    (finiteBaseFractionFieldTensorIntegralClosureAlgEquiv
      (R := R) (C := C) (L := L) m).toRingEquiv

theorem

finiteBaseFractionFieldTensorIntegralClosurePrime_isPrime

L222 ↗

EtaleFundamentalGroups.finiteBaseFractionFieldTensorIntegralClosurePrime_isPrime

Documentation

Literal transport of a normalization prime preserves primality.

Source context 11 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uR uC uL
variable {R : Type uR} {C : Type uC} {L : Type uL}
variable [CommRing R] [IsDomain R]
variable [CommRing C] [IsDomain C]
variable [Algebra R C] [FaithfulSMul R C]
variable [Field L] [Algebra R L]
variable [Algebra (FractionRing R) L]
local instance finiteBaseFractionRingAlgebraInstance :
    Algebra (FractionRing R) (FractionRing C) :=
  finiteBaseFractionRingAlgebra (R := R) (C := C)

Lean source · full declaration

theorem finiteBaseFractionFieldTensorIntegralClosurePrime_isPrime
    [Module.Finite R C]
    [IsScalarTower R (FractionRing R) L]
    (m : Ideal (C ⊗[R] L)) [m.IsMaximal]
    (q : Ideal (integralClosure C
      (FiniteEtaleGenericFiberComponent m))) [q.IsPrime] :
    let n := finiteBaseFractionFieldTensorIdeal
      (R := R) (C := C) (L := L) m
    letI : n.IsMaximal :=
      finiteBaseFractionFieldTensorIdeal_isMaximal
        (R := R) (C := C) (L := L) m
    letI : Algebra C (GenericTensorFieldComponent n) :=
      genericTensorFieldComponentLeftScalarAlgebra (R := C) n
    (finiteBaseFractionFieldTensorIntegralClosurePrime
      (R := R) (C := C) (L := L) m q).IsPrime := by
  dsimp only
  let E := finiteBaseFractionFieldTensorIntegralClosureAlgEquiv
    (R := R) (C := C) (L := L) m
  apply Ideal.map_isPrime_of_surjective E.surjective
  intro x hx
  have hx0 : x = 0 := E.injective (hx.trans (map_zero E).symm)
  subst x
  exact q.zero_mem

def

finiteBaseFractionFieldTensorIntegralClosureLocalizationAlgEquiv

L248 ↗

EtaleFundamentalGroups.finiteBaseFractionFieldTensorIntegralClosureLocalizationAlgEquiv

Documentation

Prime localization of the actual chosen component is unchanged by the canonical field-tensor presentation.

Source context 11 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uR uC uL
variable {R : Type uR} {C : Type uC} {L : Type uL}
variable [CommRing R] [IsDomain R]
variable [CommRing C] [IsDomain C]
variable [Algebra R C] [FaithfulSMul R C]
variable [Field L] [Algebra R L]
variable [Algebra (FractionRing R) L]
local instance finiteBaseFractionRingAlgebraInstance :
    Algebra (FractionRing R) (FractionRing C) :=
  finiteBaseFractionRingAlgebra (R := R) (C := C)

Lean source · full declaration

def
    finiteBaseFractionFieldTensorIntegralClosureLocalizationAlgEquiv
    [Module.Finite R C]
    [IsScalarTower R (FractionRing R) L]
    (m : Ideal (C ⊗[R] L)) [m.IsMaximal]
    (q : Ideal (integralClosure C
      (FiniteEtaleGenericFiberComponent m))) [q.IsPrime] :
    let n := finiteBaseFractionFieldTensorIdeal
      (R := R) (C := C) (L := L) m
    letI : n.IsMaximal :=
      finiteBaseFractionFieldTensorIdeal_isMaximal
        (R := R) (C := C) (L := L) m
    letI : Algebra C (GenericTensorFieldComponent n) :=
      genericTensorFieldComponentLeftScalarAlgebra (R := C) n
    let q' := finiteBaseFractionFieldTensorIntegralClosurePrime
      (R := R) (C := C) (L := L) m q
    letI : q'.IsPrime :=
      finiteBaseFractionFieldTensorIntegralClosurePrime_isPrime
        (R := R) (C := C) (L := L) m q
    Localization.AtPrime q ≃ₐ[C] Localization.AtPrime q' := by
  dsimp only
  let E := finiteBaseFractionFieldTensorIntegralClosureAlgEquiv
    (R := R) (C := C) (L := L) m
  let q' := finiteBaseFractionFieldTensorIntegralClosurePrime
    (R := R) (C := C) (L := L) m q
  letI : q'.IsPrime :=
    finiteBaseFractionFieldTensorIntegralClosurePrime_isPrime
      (R := R) (C := C) (L := L) m q
  have hcomap : q = q'.comap E.toRingHom := by
    symm
    exact Ideal.comap_map_of_bijective E.toRingEquiv E.bijective
  exact Localization.localAlgEquiv q q' E hcomap

Module documentation

Field-tensor coordinates for an actual chosen generic component

Declarations