Divisor_pullbackAlong_pushforwardAlong_eq_sum_of_decomposition.lean

theorem algebra_adjoin_eq_top_of_intermediateField {K F E : Type*} [Field K] [Field F]
  [Field E]
    [Algebra K F] [Algebra K E] [Algebra F E] [IsScalarTower K F E] [FiniteDimensional F E]
    {S : Set E} (hS : IntermediateField.adjoin K S = ⊤) : Algebra.adjoin F S = ⊤

theorem det_pi_hetero {R : Type*} [CommRing R] : ∀ {n : ℕ} (Z : Fin n → Type*)
    [∀ i, AddCommGroup (Z i)] [∀ i, Module R (Z i)]
    [∀ i, Module.Free R (Z i)] [∀ i, Module.Finite R (Z i)]
    (f : ∀ i, Z i →ₗ[R] Z i),
    LinearMap.det (LinearMap.pi fun i => f i ∘ₗ LinearMap.proj i)
      = ∏ i, LinearMap.det (f i)
  | 0, Z, _, _, _, _, f => by
    have : Subsingleton (∀ i : Fin 0, Z i) :=
      ⟨fun a b => funext fun i => i.elim0⟩
    rw [Finset.univ_eq_empty, Finset.prod_empty]
    exact LinearMap.det_eq_one_of_subsingleton _
  | (n + 1), Z, _, _, _, _, f => by
    have hconj : LinearMap.pi (fun i => f i ∘ₗ LinearMap.proj i)
        = (Fin.consLinearEquiv R Z).toLinearMap ∘ₗ
          (LinearMap.prodMap (f 0)
            (LinearMap.pi fun i : Fin n => f i.succ ∘ₗ LinearMap.proj i)) ∘ₗ
          (Fin.consLinearEquiv R Z).symm.toLinearMap := by
      apply LinearMap.ext
      intro x
      funext j
      refine Fin.cases ?_ (fun i => ?_) j <;>
        simp [Fin.consLinearEquiv, Fin.consEquiv, LinearMap.pi_apply,
          LinearMap.prodMap_apply, Fin.cons_zero, Fin.cons_succ, Fin.tail]
    rw [hconj]
    have h1 : LinearMap.det ((Fin.consLinearEquiv R Z).toLinearMap ∘ₗ
          (LinearMap.prodMap (f 0)
            (LinearMap.pi fun i : Fin n => f i.succ ∘ₗ LinearMap.proj i)) ∘ₗ
          (Fin.consLinearEquiv R Z).symm.toLinearMap)
        = LinearMap.det (LinearMap.prodMap (f 0)
            (LinearMap.pi fun i : Fin n => f i.succ ∘ₗ LinearMap.proj i)) :=
      LinearMap.det_conj _ (Fin.consLinearEquiv R Z)
    rw [h1, LinearMap.det_prodMap, det_pi_hetero]
    exact (Fin.prod_univ_succ fun i => LinearMap.det (f i)).symm

theorem algebraMap_norm_eq_prod_norm_of_decomposition
    {F F₁ F₂ : Type*} [Field F] [Field F₁] [Field F₂]
    [Algebra F F₁] [Algebra F F₂]
    [FiniteDimensional F F₁] [FiniteDimensional F F₂]
    (n : ℕ) (Z : Fin n → Type*) [∀ i, Field (Z i)]
    [∀ i, Algebra F (Z i)] [∀ i, Algebra F₁ (Z i)] [∀ i, Algebra F₂ (Z i)]
    [∀ i, IsScalarTower F F₁ (Z i)] [∀ i, IsScalarTower F F₂ (Z i)]
    [∀ i, FiniteDimensional F₁ (Z i)]
    (hgen : ∀ i, Algebra.adjoin F
      (Set.range (algebraMap F₁ (Z i)) ∪ Set.range (algebraMap F₂ (Z i))) = ⊤)
    (hdeg : ∑ i, Module.finrank F₁ (Z i) = Module.finrank F F₂)
    (hsep : ∀ i j, i ≠ j → ∃ t : F₂ ⊗[F] F₁,
      Algebra.TensorProduct.productMap (IsScalarTower.toAlgHom F F₂ (Z i))
        (IsScalarTower.toAlgHom F F₁ (Z i)) t = 0 ∧
      Algebra.TensorProduct.productMap (IsScalarTower.toAlgHom F F₂ (Z j))
        (IsScalarTower.toAlgHom F F₁ (Z j)) t ≠ 0)
    (g : F₁) :
    algebraMap F F₂ (Algebra.norm F g) = ∏ i, Algebra.norm F₂ (algebraMap F₁ (Z i) g)

theorem ord_prod {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
    {ι : Type*} (s : Finset ι) (x : ι → F) (hx : ∀ i ∈ s, x i ≠ 0) :
    v.ord (∏ i ∈ s, x i) = ∑ i ∈ s, v.ord (x i)

theorem sum_sum_ramificationIndex_mul_inertiaDeg_exchange
    {K F F₁ F₂ : Type*} [Field K] [Field F] [Field F₁] [Field F₂]
    [Algebra K F] [Algebra K F₁] [Algebra K F₂]
    [Algebra F F₁] [Algebra F F₂]
    [IsScalarTower K F F₁] [IsScalarTower K F F₂]
    [FiniteDimensional F F₁] [FiniteDimensional F F₂] [CharZero F]
    (n : ℕ) (Z : Fin n → Type*) [∀ i, Field (Z i)]
    [∀ i, Algebra K (Z i)] [∀ i, Algebra F (Z i)]
    [∀ i, Algebra F₁ (Z i)] [∀ i, Algebra F₂ (Z i)]
    [∀ i, IsScalarTower K F (Z i)] [∀ i, IsScalarTower K F₁ (Z i)] [∀ i, IsScalarTower K F₂ (Z i)]
    [∀ i, IsScalarTower F F₁ (Z i)] [∀ i, IsScalarTower F F₂ (Z i)]
    [∀ i, FiniteDimensional F₁ (Z i)] [∀ i, FiniteDimensional F₂ (Z i)]
    (hgen : ∀ i, Algebra.adjoin F
      (Set.range (algebraMap F₁ (Z i)) ∪ Set.range (algebraMap F₂ (Z i))) = ⊤)
    (hdeg : ∑ i, Module.finrank F₁ (Z i) = Module.finrank F F₂)
    (hsep : ∀ i j, i ≠ j → ∃ t : F₂ ⊗[F] F₁,
      Algebra.TensorProduct.productMap (IsScalarTower.toAlgHom F F₂ (Z i))
        (IsScalarTower.toAlgHom F F₁ (Z i)) t = 0 ∧
      Algebra.TensorProduct.productMap (IsScalarTower.toAlgHom F F₂ (Z j))
        (IsScalarTower.toAlgHom F F₁ (Z j)) t ≠ 0)
    (w₁ : Place K F₁) (w₂ : Place K F₂) (hw : w₁.restrict F = w₂.restrict F)
    (T : ∀ i, Finset (Place K (Z i)))
    (hT : ∀ i W, W ∈ T i ↔ W.restrict F₁ = w₁ ∧ W.restrict F₂ = w₂) :
    ∑ i, ∑ W ∈ T i, W.ramificationIndex F₁ * W.inertiaDeg F₂
      = w₁.inertiaDeg F * w₂.ramificationIndex F

theorem _root_.AlgebraicCurve.Divisor.pullbackAlong_pushforwardAlong_eq_sum_of_decomposition
    {K F F₁ F₂ : Type} [Field K] [Field F] [Field F₁] [Field F₂]
    [Algebra K F] [Algebra K F₁] [Algebra K F₂] [CharZero K]
    [HasPrincipalDivisors K F₁]
    (φ : F →ₐ[K] F₁) (ψ' : F →ₐ[K] F₂)
    (hφ : φ.toRingHom.IsIntegral) (hψ' : ψ'.toRingHom.IsIntegral)
    (hφfin : FiniteAlong K φ) (hψ'fin : FiniteAlong K ψ')
    (n : ℕ) (Z : Fin n → Type)
    [∀ i, Field (Z i)] [∀ i, Algebra K (Z i)] [∀ i, HasPrincipalDivisors K (Z i)]
    (u : ∀ i, F₁ →ₐ[K] Z i) (u' : ∀ i, F₂ →ₐ[K] Z i)
    (hsq : ∀ i, (u i).comp φ = (u' i).comp ψ')
    (hu : ∀ i, (u i).toRingHom.IsIntegral) (hu' : ∀ i, (u' i).toRingHom.IsIntegral)
    (hufin : ∀ i, FiniteAlong K (u i)) (hu'fin : ∀ i, FiniteAlong K (u' i))
    (hgen : ∀ i, IntermediateField.adjoin K (Set.range (u i) ∪ Set.range (u' i)) = ⊤)
    (hdeg : ∑ i, finrankAlong K (u' i) = finrankAlong K φ)
    (hsep : ∀ i j, i ≠ j → ∃ t : F₁ ⊗[K] F₂,
      Algebra.TensorProduct.productMap (u i) (u' i) t = 0 ∧
      Algebra.TensorProduct.productMap (u j) (u' j) t ≠ 0)
    (D : Divisor K F₂) :
    Divisor.pullbackAlong φ hφ (Divisor.pushforwardAlong ψ' hψ' D)
      = ∑ i, Divisor.pushforwardAlong (u i) (hu i)
          (Divisor.pullbackAlong (u' i) (hu' i) D)