EtaleFundamentalGroups.exists_integralClosure_genericTensorFieldComponent_prime_liesOver_span_ramificationIdx_eq
A prime in a fixed generic tensor component after finite-etale base change, retaining both the literal boundary prime and the original ramification index.
The finiteness of integralClosure A M is the standard source that makes M its fraction field. In the height-two application it is produced by the existing finite-normalization theorem.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe uLean source · full declaration
theorem
exists_integralClosure_genericTensorFieldComponent_prime_liesOver_span_ramificationIdx_eq
{A C F KC M : Type u}
[CommRing A] [IsDomain A]
[CommRing C] [IsDomain C] [Algebra A C]
[Module.Finite A C] [Algebra.Etale A C] [FaithfulSMul A C]
[Field F] [Algebra A F] [IsFractionRing A F]
[Field KC] [Algebra C KC] [IsFractionRing C KC]
[Algebra A KC] [IsScalarTower A C KC]
[Algebra F KC] [IsScalarTower A F KC]
[Field M] [Algebra F M] [FiniteDimensional F M]
[Algebra A M] [IsScalarTower A F M]
[Module.Finite A (integralClosure A M)]
(y : A)
(m : Ideal (KC ⊗[F] M)) [m.IsMaximal]
(q : Ideal (integralClosure A M)) [q.IsPrime]
[q.LiesOver (Ideal.span ({y} : Set A))]
(hpC : (Ideal.span ({algebraMap A C y} : Set C)).IsPrime) :
let Omega := GenericTensorFieldComponent m
letI : Algebra C Omega :=
genericTensorFieldComponentLeftScalarAlgebra (R := C) m
∃ Q : Ideal (integralClosure C Omega), Q.IsPrime ∧
Q.LiesOver (Ideal.span ({algebraMap A C y} : Set C)) ∧
Q.ramificationIdx C = q.ramificationIdx A := by
classical
dsimp only
let Omega := GenericTensorFieldComponent m
let C0 := integralClosure A M
let pA := Ideal.span ({y} : Set A)
let pC := Ideal.span ({algebraMap A C y} : Set C)
let : Algebra.IsIntegral A C := Algebra.IsIntegral.of_finite A C
let : Module.FaithfullyFlat A C := inferInstance
let : pC.IsPrime := hpC
/- Keep the two field coordinates of the literal quotient component.
The direct `A`-action is taken through the right coordinate `M`; the
tensor relation proves that it is also the action through `C` and `KC`. -/
let : Algebra C Omega :=
genericTensorFieldComponentLeftScalarAlgebra (R := C) m
let : SMul C Omega :=
(genericTensorFieldComponentLeftScalarAlgebra (R := C) m).toSMul
let : Algebra M Omega := genericTensorFieldComponentRightAlgebra m
let : SMul M Omega :=
(genericTensorFieldComponentRightAlgebra m).toSMul
let : Algebra A Omega :=
genericTensorFieldComponentLeftScalarAlgebra (R := A) m
let : SMul A Omega :=
(genericTensorFieldComponentLeftScalarAlgebra (R := A) m).toSMul
let : IsScalarTower F KC Omega :=
genericTensorFieldComponent_isScalarTower m
let : IsScalarTower F M Omega :=
genericTensorFieldComponent_right_isScalarTower m
let : IsScalarTower A C Omega := by
apply IsScalarTower.of_algebraMap_eq'
ext a
change
algebraMap KC Omega (algebraMap A KC a) =
algebraMap KC Omega (algebraMap C KC (algebraMap A C a))
rw [IsScalarTower.algebraMap_apply A C KC]
let : IsScalarTower A M Omega := by
apply IsScalarTower.of_algebraMap_eq
intro a
change
algebraMap KC Omega (algebraMap A KC a) =
algebraMap M Omega (algebraMap A M a)
calc
algebraMap KC Omega (algebraMap A KC a) =
algebraMap KC Omega (algebraMap F KC (algebraMap A F a)) := by
rw [IsScalarTower.algebraMap_apply A F KC]
_ = algebraMap F Omega (algebraMap A F a) :=
(IsScalarTower.algebraMap_apply F KC Omega _).symm
_ = algebraMap M Omega (algebraMap F M (algebraMap A F a)) :=
IsScalarTower.algebraMap_apply F M Omega _
_ = algebraMap M Omega (algebraMap A M a) := by
rw [IsScalarTower.algebraMap_apply A F M]
/- Regard `Omega` as the selected generic component of the finite-etale
algebra `C / A`, after changing the normal base from `A` to `C0`.
The last map is the literal quotient by `m`. -/
let : Algebra M (KC ⊗[F] M) := Algebra.TensorProduct.rightAlgebra
let eGeneric : (F ⊗[A] C) ≃ₐ[F] KC :=
finiteGenericFiberAlgEquiv (R := A) (C := C) (K := F) (E := KC)
let eFactor0 : (M ⊗[A] C) ≃ₐ[M] (M ⊗[F] KC) :=
iteratedGenericFiberEquiv A F M C KC eGeneric
let eComm : (M ⊗[F] KC) ≃ₐ[M] (KC ⊗[F] M) :=
Algebra.TensorProduct.commRight F M KC
let eFactor : (M ⊗[A] C) ≃ₐ[M] (KC ⊗[F] M) :=
eFactor0.trans eComm
let quotient : (KC ⊗[F] M) →ₐ[M] Omega := Ideal.Quotient.mkₐ M m
let componentMap : (M ⊗[A] C) →ₐ[M] Omega :=
quotient.comp eFactor.toAlgHom
let : IsFractionRing C0 M :=
IsIntegralClosure.isFractionRing_of_finite_extension A F M C0
let : IsIntegrallyClosed C0 :=
integralClosure.isIntegrallyClosedOfFiniteExtension F
let c0OmegaAlgebra : Algebra C0 Omega :=
((algebraMap M Omega).comp (algebraMap C0 M)).toAlgebra
let : Algebra C0 Omega := c0OmegaAlgebra
let : SMul C0 Omega := c0OmegaAlgebra.toSMul
let : IsScalarTower C0 M Omega := IsScalarTower.of_algebraMap_eq' rfl
let : IsScalarTower A C0 Omega := by
apply IsScalarTower.of_algebraMap_eq'
ext a
calc
algebraMap A Omega a = algebraMap M Omega (algebraMap A M a) :=
IsScalarTower.algebraMap_apply A M Omega a
_ = algebraMap M Omega (algebraMap C0 M (algebraMap A C0 a)) := by
rw [IsScalarTower.algebraMap_apply A C0 M]
_ = algebraMap C0 Omega (algebraMap A C0 a) :=
(IsScalarTower.algebraMap_apply C0 M Omega _).symm
have hEtale0 : Algebra.Etale C0 (integralClosure C0 Omega) := by
apply integralClosure_etale_of_surjective_reassociatedGenericFiber
(A := A) (B := C0) (T := C) (K := M) componentMap
exact Ideal.Quotient.mk_surjective.comp eFactor.surjective
/- The normalizations over `C0` and over `C` are the same subring of
`Omega`. Transport etaleness across that canonical, ambient-identity
equivalence. -/
let : Algebra C0 (integralClosure C Omega) :=
integralClosureTwoIntegralBasesAlgebra
(A := A) (B := C0) (C := C) (L := Omega)
let eNorm :
integralClosure C0 Omega ≃ₐ[C0] integralClosure C Omega :=
integralClosureTwoIntegralBasesAlgEquiv
(A := A) (B := C0) (C := C) (L := Omega)
let : IsScalarTower C (integralClosure C Omega) Omega :=
IsScalarTower.of_algebraMap_eq fun _ ↦ rfl
let : Algebra.Etale C0 (integralClosure C0 Omega) := hEtale0
let : Algebra.Etale C0 (integralClosure C Omega) :=
Algebra.Etale.of_equiv eNorm
have hIntegral0 : Algebra.IsIntegral C0 (integralClosure C0 Omega) :=
IsIntegralClosure.isIntegral_algebra C0 Omega
let : Algebra.IsIntegral C0 (integralClosure C Omega) :=
eNorm.isIntegral_iff.mp hIntegral0
have hBaseAmbient (x : C0) :
algebraMap (integralClosure C Omega) Omega
(algebraMap C0 (integralClosure C Omega) x) =
algebraMap C0 Omega x := by
calc
algebraMap (integralClosure C Omega) Omega
(algebraMap C0 (integralClosure C Omega) x) =
algebraMap (integralClosure C Omega) Omega
(eNorm (algebraMap C0 (integralClosure C0 Omega) x)) := by
rw [eNorm.commutes]
_ = algebraMap (integralClosure C0 Omega) Omega
(algebraMap C0 (integralClosure C0 Omega) x) :=
algebraMap_integralClosureTwoIntegralBasesAlgEquiv
(A := A) (B := C0) (C := C) (L := Omega) _
_ = algebraMap C0 Omega x :=
(IsScalarTower.algebraMap_apply
C0 (integralClosure C0 Omega) Omega x).symm
have hC0OmegaInjective : Function.Injective (algebraMap C0 Omega) := by
intro x x' hxx'
apply IsFractionRing.injective C0 M
apply (algebraMap M Omega).injective
change algebraMap C0 Omega x = algebraMap C0 Omega x'
exact hxx'
have hC0SInjective :
Function.Injective (algebraMap C0 (integralClosure C Omega)) := by
intro x x' hxx'
apply hC0OmegaInjective
rw [← hBaseAmbient x, ← hBaseAmbient x', hxx']
/- Install the direct `A`-action through `C0`. Compatibility with the
`C`-action is checked after embedding the normalization into `Omega`. -/
let aSAlgebra : Algebra A (integralClosure C Omega) :=
((algebraMap C0 (integralClosure C Omega)).comp
(algebraMap A C0)).toAlgebra
let : Algebra A (integralClosure C Omega) := aSAlgebra
let : IsScalarTower A C0 (integralClosure C Omega) :=
IsScalarTower.of_algebraMap_eq' rfl
let : IsScalarTower A C (integralClosure C Omega) := by
apply IsScalarTower.of_algebraMap_eq
intro a
apply Subtype.ext
change
algebraMap (integralClosure C Omega) Omega
(algebraMap A (integralClosure C Omega) a) =
algebraMap (integralClosure C Omega) Omega
(algebraMap C (integralClosure C Omega) (algebraMap A C a))
calc
algebraMap (integralClosure C Omega) Omega
(algebraMap A (integralClosure C Omega) a) =
algebraMap C0 Omega (algebraMap A C0 a) :=
hBaseAmbient (algebraMap A C0 a)
_ = algebraMap A Omega a :=
(IsScalarTower.algebraMap_apply A C0 Omega a).symm
_ = algebraMap C Omega (algebraMap A C a) :=
IsScalarTower.algebraMap_apply A C Omega a
_ = algebraMap (integralClosure C Omega) Omega
(algebraMap C (integralClosure C Omega) (algebraMap A C a)) :=
(IsScalarTower.algebraMap_apply
C (integralClosure C Omega) Omega _).symm
/- Going-up now chooses a prime in the already fixed component `Omega`.
It cannot drift to another tensor factor because `S` was fixed before the
prime was chosen. -/
obtain ⟨Q, -, hQPrime, hQComap⟩ :=
Ideal.exists_ideal_over_prime_of_isIntegral q
(⊥ : Ideal (integralClosure C Omega)) (by
rw [Ideal.under, ← RingHom.ker_eq_comap_bot,
(RingHom.injective_iff_ker_eq_bot _).mp hC0SInjective]
exact bot_le)
let : Q.IsPrime := hQPrime
have hQOverq : Q.LiesOver q :=
(Ideal.liesOver_iff Q q).mpr hQComap.symm
let : Q.LiesOver q := hQOverq
let P := Q.under C
let : P.IsPrime := inferInstance
let : Q.LiesOver P := inferInstance
have hQOverpA : Q.LiesOver pA := Ideal.LiesOver.trans Q q pA
let : Q.LiesOver pA := hQOverpA
have hPOverpA : P.LiesOver pA := Ideal.LiesOver.tower_bot Q P pA
let : P.LiesOver pA := hPOverpA
have hpCOverpA : pC.LiesOver pA := by
refine ⟨?_⟩
rw [show pC = pA.map (algebraMap A C) by
simp only [pA, pC, Ideal.map_span, Set.image_singleton]]
exact
(Ideal.comap_map_eq_self_of_faithfullyFlat
(B := C) pA).symm
let : pC.LiesOver pA := hpCOverpA
have hpCLe : pC ≤ P := by
apply P.span_singleton_le_iff_mem.mpr
exact (Ideal.mem_of_liesOver P pA y).mp
(Ideal.mem_span_singleton_self y)
have hpCEq : pC = P := by
rcases lt_or_eq_of_le hpCLe with hlt | heq
· have hUnderLt :=
Ideal.IsIntegral.under_lt_under (R := A) (A := C) hlt
change pC.under A < P.under A at hUnderLt
rw [← pC.over_def pA, ← P.over_def pA] at hUnderLt
exact (lt_irrefl pA hUnderLt).elim
· exact heq
have hQOverpC : Q.LiesOver pC := by
rw [hpCEq]
infer_instance
refine ⟨Q, hQPrime, ?_, ?_⟩
· simpa only [Omega, pC] using hQOverpC
exact ramificationIdx_eq_of_etale_square
(R := A) (B := C0) (C := C)
(S := integralClosure C Omega) q Q