AlgebraicCurves.Divisors.Proofs.Divisor_pullbackAlong_pushforwardAlong_eq_add_of_normFormulaAlong.AlgebraicCurve.BaseChangeTwo.map_norm_eq_norm_mul_norm
Source context 11 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_pullbackAlong_pushforwardAlong_eq_add_of_normFormulaAlong
noncomputable section
open _root_.AlgebraicCurve
open _root_.TensorProduct
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace BaseChangeTwo
section Tensor
variable {K F F₁ F₂ Z Z' : Type*} [Field K] [Field F] [Field F₁] [Field F₂] [Field Z] [Field Z']
[Algebra K F] [Algebra K F₁] [Algebra K F₂] [Algebra K Z] [Algebra K Z']
Lean source · full declarationtheorem map_norm_eq_norm_mul_norm
(φ : F →ₐ[K] F₁) (ψ' : F →ₐ[K] F₂)
(u : F₁ →ₐ[K] Z) (u' : F₂ →ₐ[K] Z) (s : F₁ →ₐ[K] Z') (s' : F₂ →ₐ[K] Z')
(hsq : u.comp φ = u'.comp ψ') (hsq' : s.comp φ = s'.comp ψ')
(hψ'fin : FiniteAlong K ψ') (hufin : FiniteAlong K u) (hsfin : FiniteAlong K s)
(hgen : IntermediateField.adjoin K (Set.range u ∪ Set.range u') = ⊤)
(hgen' : IntermediateField.adjoin K (Set.range s ∪ Set.range s') = ⊤)
(hdeg : finrankAlong K u + finrankAlong K s = finrankAlong K ψ')
(hne : ∃ (a : F₁) (b : F₂), s a = s' b ∧ u a ≠ u' b) (g : F₂) :
φ (letI := algebraAlong ψ'; Algebra.norm F g) =
(letI := algebraAlong u; Algebra.norm F₁ (u' g)) *
(letI := algebraAlong s; Algebra.norm F₁ (s' g)) := by
let iF1 : Algebra F F₁ := algebraAlong φ
let iF2 : Algebra F F₂ := algebraAlong ψ'
let iZ1 : Algebra F₁ Z := algebraAlong u
let iZ2 : Algebra F₂ Z := algebraAlong u'
let iZ : Algebra F Z := algebraAlong (u.comp φ)
let iZ'1 : Algebra F₁ Z' := algebraAlong s
let iZ'2 : Algebra F₂ Z' := algebraAlong s'
let iZ' : Algebra F Z' := algebraAlong (s.comp φ)
have : IsScalarTower F F₁ Z := IsScalarTower.of_algebraMap_eq fun x => rfl
have : IsScalarTower F F₂ Z :=
IsScalarTower.of_algebraMap_eq fun x => (AlgHom.congr_fun hsq x : u (φ x) = u' (ψ' x))
have : IsScalarTower F F₁ Z' := IsScalarTower.of_algebraMap_eq fun x => rfl
have : IsScalarTower F F₂ Z' :=
IsScalarTower.of_algebraMap_eq fun x => (AlgHom.congr_fun hsq' x : s (φ x) = s' (ψ' x))
have : Module.Finite F F₂ := hψ'fin
have : Module.Finite F₁ Z := hufin
have : Module.Finite F₁ Z' := hsfin
let gZ : F₂ →ₐ[F] Z := IsScalarTower.toAlgHom F F₂ Z
let gZ' : F₂ →ₐ[F] Z' := IsScalarTower.toAlgHom F F₂ Z'
let PP : F₁ ⊗[F] F₂ →ₐ[F₁] Z × Z' :=
Algebra.TensorProduct.lift (Algebra.ofId F₁ (Z × Z')) (gZ.prod gZ') (fun _ _ => Commute.all _ _)
have hPP : ∀ (a : F₁) (b : F₂), PP (a ⊗ₜ b) = (u a * u' b, s a * s' b) := by
intro a b
rw [Algebra.TensorProduct.lift_tmul]
rfl
let Pfst : F₁ ⊗[F] F₂ →ₐ[F₁] Z := (AlgHom.fst F₁ Z Z').comp PP
let Psnd : F₁ ⊗[F] F₂ →ₐ[F₁] Z' := (AlgHom.snd F₁ Z Z').comp PP
have hPfst : ∀ (a : F₁) (b : F₂), Pfst (a ⊗ₜ b) = u a * u' b := fun a b => by
change (PP (a ⊗ₜ b)).1 = _; rw [hPP]
have hPsnd : ∀ (a : F₁) (b : F₂), Psnd (a ⊗ₜ b) = s a * s' b := fun a b => by
change (PP (a ⊗ₜ b)).2 = _; rw [hPP]
have hsurj₁ : Function.Surjective Pfst := by
have htop : Pfst.range = ⊤ := by
refine subalgebra_eq_top_of_adjoin_eq_top u hufin (Set.range u') hgen Pfst.range ?_
rintro _ ⟨b, rfl⟩
refine ⟨1 ⊗ₜ b, ?_⟩
change Pfst (1 ⊗ₜ b) = _
rw [hPfst, map_one, one_mul]
exact fun z => by
have hz : z ∈ Pfst.range := by rw [htop]; exact Algebra.mem_top
exact hz
have hsurj₂ : Function.Surjective Psnd := by
have htop : Psnd.range = ⊤ := by
refine subalgebra_eq_top_of_adjoin_eq_top s hsfin (Set.range s') hgen' Psnd.range ?_
rintro _ ⟨b, rfl⟩
refine ⟨1 ⊗ₜ b, ?_⟩
change Psnd (1 ⊗ₜ b) = _
rw [hPsnd, map_one, one_mul]
exact fun z => by
have hz : z ∈ Psnd.range := by rw [htop]; exact Algebra.mem_top
exact hz
have hmax₁ : (RingHom.ker Pfst.toRingHom).IsMaximal :=
RingHom.ker_isMaximal_of_surjective Pfst.toRingHom hsurj₁
have hmax₂ : (RingHom.ker Psnd.toRingHom).IsMaximal :=
RingHom.ker_isMaximal_of_surjective Psnd.toRingHom hsurj₂
have hne' : RingHom.ker Pfst.toRingHom ≠ RingHom.ker Psnd.toRingHom := by
obtain ⟨a, b, hab, hab'⟩ := hne
intro h
have hmem : (a ⊗ₜ[F] (1 : F₂) - (1 : F₁) ⊗ₜ[F] b) ∈ RingHom.ker Psnd.toRingHom := by
rw [RingHom.mem_ker]
change Psnd _ = 0
rw [map_sub, hPsnd, hPsnd, map_one, map_one, mul_one, one_mul, hab, sub_self]
rw [← h, RingHom.mem_ker] at hmem
apply hab'
have : Pfst (a ⊗ₜ[F] (1 : F₂) - (1 : F₁) ⊗ₜ[F] b) = 0 := hmem
rwa [map_sub, hPfst, hPfst, map_one, map_one, mul_one, one_mul, sub_eq_zero] at this
have hcop : RingHom.ker Pfst.toRingHom ⊔ RingHom.ker Psnd.toRingHom = ⊤ :=
Ideal.IsMaximal.coprime_of_ne hmax₁ hmax₂ hne'
obtain ⟨x, hx, y, hy, hxy⟩ := Submodule.mem_sup.mp
((Ideal.eq_top_iff_one _).mp hcop)
have hx₁ : Pfst x = 0 := hx
have hy₂ : Psnd y = 0 := hy
have hy₁ : Pfst y = 1 := by
have := congrArg Pfst hxy
rwa [map_add, hx₁, zero_add, map_one] at this
have hx₂ : Psnd x = 1 := by
have := congrArg Psnd hxy
rwa [map_add, hy₂, add_zero, map_one] at this
have hsurj : Function.Surjective PP := by
rintro ⟨z, z'⟩
obtain ⟨a₁, rfl⟩ := hsurj₁ z
obtain ⟨a₂, rfl⟩ := hsurj₂ z'
refine ⟨a₁ * y + a₂ * x, Prod.ext ?_ ?_⟩
· change Pfst (a₁ * y + a₂ * x) = Pfst a₁
rw [map_add, map_mul, map_mul, hy₁, hx₁, mul_one, mul_zero, add_zero]
· change Psnd (a₁ * y + a₂ * x) = Psnd a₂
rw [map_add, map_mul, map_mul, hy₂, hx₂, mul_zero, mul_one, zero_add]
have hdim : Module.finrank F₁ (F₁ ⊗[F] F₂) = Module.finrank F₁ (Z × Z') := by
rw [Module.finrank_baseChange, Module.finrank_prod]
exact hdeg.symm
have hinj : Function.Injective PP :=
(LinearMap.injective_iff_surjective_of_finrank_eq_finrank hdim (f := PP.toLinearMap)).mpr hsurj
let e : F₁ ⊗[F] F₂ ≃ₐ[F₁] Z × Z' := AlgEquiv.ofBijective PP ⟨hinj, hsurj⟩
have hlin : (Algebra.lmul F F₂ g).baseChange F₁ = Algebra.lmul F₁ (F₁ ⊗[F] F₂) ((1 : F₁) ⊗ₜ g) :=
by
apply LinearMap.ext
intro t
induction t using TensorProduct.inductionOn with
| add x y hx hy => simp only [map_add, hx, hy]
| tmul a b =>
rw [LinearMap.baseChange_tmul]
change a ⊗ₜ (g * b) = ((1 : F₁) ⊗ₜ[F] g) * (a ⊗ₜ[F] b)
rw [Algebra.TensorProduct.tmul_mul_tmul, one_mul]
have hprod : Algebra.lmul F₁ (Z × Z') (u' g, s' g) =
LinearMap.prodMap (Algebra.lmul F₁ Z (u' g)) (Algebra.lmul F₁ Z' (s' g)) := by
apply LinearMap.ext
rintro ⟨z, z'⟩
rfl
calc φ (Algebra.norm F g)
= algebraMap F F₁ (LinearMap.det (Algebra.lmul F F₂ g)) := by rw [Algebra.norm_apply]; rfl
_ = LinearMap.det (Algebra.lmul F₁ (F₁ ⊗[F] F₂) ((1 : F₁) ⊗ₜ g)) := by
rw [← hlin, LinearMap.det_baseChange]
_ = Algebra.norm F₁ ((1 : F₁) ⊗ₜ[F] g) := (Algebra.norm_apply F₁ _).symm
_ = Algebra.norm F₁ (e ((1 : F₁) ⊗ₜ[F] g)) := (Algebra.norm_eq_of_algEquiv e _).symm
_ = Algebra.norm F₁ ((u' g, s' g) : Z × Z') := by
congr 1
change PP ((1 : F₁) ⊗ₜ g) = _
rw [hPP, map_one, map_one, one_mul, one_mul]
_ = LinearMap.det (Algebra.lmul F₁ Z (u' g)) * LinearMap.det (Algebra.lmul F₁ Z' (s' g)) := by
rw [Algebra.norm_apply, hprod, LinearMap.det_prodMap]
_ = Algebra.norm F₁ (u' g) * Algebra.norm F₁ (s' g) := by
rw [← Algebra.norm_apply, ← Algebra.norm_apply]