EtaleFundamentalGroups.localization_away_integralClosure_genericTensorFieldComponent_etale_of_base_away
A fixed generic component after normal base change inherits the original finite-etale boundary complement as the literal away map of its normalization. The maximal tensor ideal m is preserved throughout.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uA uC uD uF uE uKLean source · full declaration
theorem
localization_away_integralClosure_genericTensorFieldComponent_etale_of_base_away
{A : Type uA} {C : Type uC} {D : Type uD}
{F : Type uF} {E : Type uE} {K : Type uK}
[CommRing A] [IsDomain A]
[CommRing C] [IsDomain C] [Algebra A C] [FaithfulSMul A C]
(f : A)
[Algebra (Localization.Away f)
(Localization.Away (algebraMap A C f))]
[Module.Finite (Localization.Away f)
(Localization.Away (algebraMap A C f))]
[Algebra.Etale (Localization.Away f)
(Localization.Away (algebraMap A C f))]
[Field F] [Algebra (Localization.Away f) F]
[IsFractionRing (Localization.Away f) F]
[Algebra A F] [IsScalarTower A (Localization.Away f) F]
[Field E] [Algebra (Localization.Away (algebraMap A C f)) E]
[IsFractionRing (Localization.Away (algebraMap A C f)) E]
[Algebra (Localization.Away f) E]
[IsScalarTower (Localization.Away f)
(Localization.Away (algebraMap A C f)) E]
[Algebra F E] [IsScalarTower (Localization.Away f) F E]
[CommRing D] [IsDomain D] [IsIntegrallyClosed D] [Algebra A D]
[Field K] [Algebra D K] [IsFractionRing D K]
[Algebra A K] [IsScalarTower A D K]
[Algebra F K] [IsScalarTower A F K]
(m : Ideal (K ⊗[F] E)) [m.IsMaximal] :
let M := GenericTensorFieldComponent m
letI : Algebra D M :=
genericTensorFieldComponentLeftScalarAlgebra (R := D) m
letI : SMul D M :=
(genericTensorFieldComponentLeftScalarAlgebra (R := D) m).toSMul
letI : IsScalarTower D K M :=
IsScalarTower.of_algebraMap_eq fun _ ↦ rfl
(Localization.awayMap (algebraMap D (integralClosure D M))
(algebraMap A D f)).Etale := by
dsimp only
let S := Localization.Away f
let fD : D := algebraMap A D f
have hfS : algebraMap A S f ≠ 0 := by
let : Nontrivial S := (algebraMap S F).domain_nontrivial
exact (IsLocalization.Away.algebraMap_isUnit f).ne_zero
have hfAF : algebraMap A F f ≠ 0 := by
rw [IsScalarTower.algebraMap_apply A S F]
simpa using (IsFractionRing.injective S F).ne hfS
have hfAK : algebraMap A K f ≠ 0 := by
rw [IsScalarTower.algebraMap_apply A F K]
simpa using (algebraMap F K).injective.ne hfAF
have hfD : fD ≠ 0 := by
intro hfDzero
apply hfAK
calc
algebraMap A K f = algebraMap D K (algebraMap A D f) :=
IsScalarTower.algebraMap_apply A D K f
_ = algebraMap D K fD := by rfl
_ = algebraMap D K 0 := congrArg (algebraMap D K) hfDzero
_ = 0 := map_zero (algebraMap D K)
let B := Localization.Away fD
let : IsDomain B := IsLocalization.Away.isDomain B hfD
let : Algebra B K :=
localizationAwayToExtensionAlgebra
(A := D) (K := K) (L := K) fD hfD
let : IsScalarTower D B K :=
localizationAwayToExtension_isScalarTower
(A := D) (K := K) (L := K) fD hfD
let : IsFractionRing B K :=
IsFractionRing.isFractionRing_of_isDomain_of_isLocalization
(Submonoid.powers fD) B K
let : IsIntegrallyClosed B :=
isIntegrallyClosed_of_isLocalization B (Submonoid.powers fD)
(Submonoid.powers_le.mpr (mem_nonZeroDivisors_iff_ne_zero.mpr hfD))
let : IsScalarTower A D B := by
apply IsScalarTower.of_algebraMap_eq
intro x
rfl
let : IsScalarTower A B K := by
apply IsScalarTower.of_algebraMap_eq
intro x
calc
algebraMap A K x = algebraMap D K (algebraMap A D x) :=
IsScalarTower.algebraMap_apply A D K x
_ = algebraMap B K (algebraMap D B (algebraMap A D x)) :=
IsScalarTower.algebraMap_apply D B K (algebraMap A D x)
_ = algebraMap B K (algebraMap A B x) := rfl
have hfB : IsUnit (algebraMap A B f) := by
change IsUnit (algebraMap D B fD)
exact IsLocalization.Away.algebraMap_isUnit fD
let M := GenericTensorFieldComponent m
have hlocalOld :=
integralClosure_genericTensorFieldComponent_etale_of_away_isUnit
(R := A) (C := C) (B := B) (F := F) (E := E) (K := K)
f hfB m
let : Algebra D M :=
genericTensorFieldComponentLeftScalarAlgebra (R := D) m
let : SMul D M :=
(genericTensorFieldComponentLeftScalarAlgebra (R := D) m).toSMul
let : IsScalarTower D K M :=
IsScalarTower.of_algebraMap_eq fun _ ↦ rfl
let quotientBM : Algebra B M :=
Ideal.instAlgebraQuotient B m
let canonicalBM : Algebra B M :=
localizationAwayToExtensionAlgebra
(A := D) (K := K) (L := M) fD hfD
have hAlgebra : quotientBM = canonicalBM := by
have hmaps :
@algebraMap B M _ _ quotientBM =
@algebraMap B M _ _ canonicalBM := by
apply IsLocalization.ringHom_ext (Submonoid.powers fD)
apply DFunLike.ext _ _
intro x
change algebraMap K M (algebraMap B K (algebraMap D B x)) =
(IsLocalization.Away.lift fD
(show IsUnit (algebraMap D M fD) by
rw [IsScalarTower.algebraMap_apply D K M]
exact (algebraMap K M).isUnit_map
(isUnit_iff_ne_zero.mpr
(by simpa using (IsFractionRing.injective D K).ne hfD))))
(algebraMap D B x)
rw [IsLocalization.Away.lift_eq]
calc
algebraMap K M (algebraMap B K (algebraMap D B x)) =
algebraMap K M (algebraMap D K x) := by
rw [IsScalarTower.algebraMap_apply D B K]
_ = algebraMap D M x :=
(IsScalarTower.algebraMap_apply D K M x).symm
apply Algebra.algebra_ext
intro z
exact DFunLike.congr_fun hmaps z
have hlocalCanonical :
@Algebra.Etale B
(@integralClosure B M _ _ canonicalBM)
_ _
(@integralClosure B M _ _ canonicalBM).algebra := by
exact hAlgebra ▸ hlocalOld
let : Algebra B M := canonicalBM
let : SMul B M := canonicalBM.toSMul
let : IsScalarTower D B M := by
apply IsScalarTower.of_algebraMap_eq
intro x
change algebraMap D M x =
(IsLocalization.Away.lift fD _) (algebraMap D B x)
rw [IsLocalization.Away.lift_eq]
exact localization_integralClosure_away_etale_of_local_integralClosure_etale
(A := D) (K := K) (L := M) fD hfD hlocalCanonical