Place_hasValue_norm_along_of_separableAlong.lean

def instModuleResidueQuotientMap (v : Place K F) :
    Module (v.toValuationSubring ⧸ IsLocalRing.maximalIdeal v.toValuationSubring)
      (Place.integralClosureAt F' v ⧸
        Ideal.map (algebraMap v.toValuationSubring (Place.integralClosureAt F' v))
          (IsLocalRing.maximalIdeal v.toValuationSubring))

def instModuleResidueQuotientPow (v : Place K F)
    (Q : Ideal (Place.integralClosureAt F' v)) :
    Module (v.toValuationSubring ⧸ IsLocalRing.maximalIdeal v.toValuationSubring)
      (Place.integralClosureAt F' v ⧸
        Q ^ (IsLocalRing.maximalIdeal v.toValuationSubring).ramificationIdx' Q)

theorem instAddMonoidHomClassQuotientMk (v : Place K F)
    (J : Ideal (Place.integralClosureAt F' v)) :
    AddMonoidHomClass (Place.integralClosureAt F' v →+* Place.integralClosureAt F' v ⧸ J)
      (Place.integralClosureAt F' v) (Place.integralClosureAt F' v ⧸ J)

def factorsPiQuotientEquiv
    {R S : Type*} [CommRing R] [CommRing S] [Algebra R S] [IsDedekindDomain S]
    (p : Ideal R) (hp : Ideal.map (algebraMap R S) p ≠ ⊥) :
    S ⧸ Ideal.map (algebraMap R S) p ≃+*
      ∀ P : (UniqueFactorizationMonoid.factors (Ideal.map (algebraMap R S) p)).toFinset,
        S ⧸ (P : Ideal S) ^ Ideal.ramificationIdx' p P.1

theorem factorsPiQuotientEquiv_mk
    {R S : Type*} [CommRing R] [CommRing S] [Algebra R S] [IsDedekindDomain S]
    (p : Ideal R) (hp : Ideal.map (algebraMap R S) p ≠ ⊥) (x : S) :
    factorsPiQuotientEquiv p hp (Ideal.Quotient.mk _ x) = fun _ => Ideal.Quotient.mk _ x :=
  rfl

theorem exists_unit_of_forall_hasValue {K F F' : Type*} [Field K] [Field F] [Field F']
    [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
    [FiniteDimensional F F'] [Algebra.IsSeparable F F']
    (v : Place K F) (g : F') (a : Place K F' → Kˣ)
    (ha : ∀ w ∈ v.fiberOver F', w.HasValue g (a w)) :
    ∃ b : (Place.integralClosureAt F' v)ˣ, algebraMap (Place.integralClosureAt F' v) F' b = g

theorem norm_algebraMap_integralClosureAt {K F F' : Type*} [Field K] [Field F] [Field F']
    [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
    [FiniteDimensional F F'] [Algebra.IsSeparable F F']
    (v : Place K F)
    (x : Place.integralClosureAt F' v) :
    Algebra.norm F (algebraMap (Place.integralClosureAt F' v) F' x) =
      algebraMap v.toValuationSubring F (Algebra.norm v.toValuationSubring x)

theorem mk_norm_eq_norm_quotient {K F F' : Type*} [Field K] [Field F] [Field F']
    [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
    [FiniteDimensional F F'] [Algebra.IsSeparable F F']
    (v : Place K F)
    (x : Place.integralClosureAt F' v) :
    Ideal.Quotient.mk (IsLocalRing.maximalIdeal v.toValuationSubring)
        (Algebra.norm v.toValuationSubring x) =
      Algebra.norm (v.toValuationSubring ⧸ IsLocalRing.maximalIdeal v.toValuationSubring)
        (Ideal.Quotient.mk
          (Ideal.map (algebraMap v.toValuationSubring (Place.integralClosureAt F' v))
            (IsLocalRing.maximalIdeal v.toValuationSubring)) x)

theorem sub_const_mem_fiberCenter {K F F' : Type*} [Field K] [Field F] [Field F']
    [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
    [FiniteDimensional F F'] [Algebra.IsSeparable F F']
    (v : Place K F) {w : Place K F'} (hw : w.restrict F = v)
    (x : Place.integralClosureAt F' v) (a : K)
    (hx : w.HasValue (algebraMap (Place.integralClosureAt F' v) F' x) a) :
    x - algebraMap v.toValuationSubring (Place.integralClosureAt F' v)
        ⟨algebraMap K F a, v.algebraMap_mem' a⟩ ∈
      (Place.fiberCenter F' v hw).asIdeal

theorem norm_algebraMap_add_of_isNilpotent {k A : Type*} [CommRing k] [IsDomain k]
    [CommRing A] [Algebra k A] [Module.Free k A] [Module.Finite k A]
    (c : k) (n : A) (hn : IsNilpotent n) :
    Algebra.norm k (algebraMap k A c + n) = c ^ Module.finrank k A

theorem norm_pi {R ι : Type*} [CommRing R] [Fintype ι] (A : ι → Type*)
    [∀ i, CommRing (A i)] [∀ i, Algebra R (A i)] [∀ i, Module.Free R (A i)]
    [∀ i, Module.Finite R (A i)] (x : ∀ i, A i) :
    Algebra.norm R x = ∏ i, Algebra.norm R (x i)

theorem free_quotient_pow_ramificationIdx {K F F' : Type*} [Field K] [Field F] [Field F']
    [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
    [FiniteDimensional F F'] [Algebra.IsSeparable F F']
    (v : Place K F) (Q : Ideal (Place.integralClosureAt F' v)) :
    Module.Free (v.toValuationSubring ⧸ IsLocalRing.maximalIdeal v.toValuationSubring)
      (Place.integralClosureAt F' v ⧸ Q ^
        (IsLocalRing.maximalIdeal v.toValuationSubring).ramificationIdx' Q)

theorem norm_mk_pow_fiberCenter {K F F' : Type*} [Field K] [Field F] [Field F']
    [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
    [FiniteDimensional F F'] [Algebra.IsSeparable F F']
    (v : Place K F) {w : Place K F'} (hw : w.restrict F = v)
    (P : IsDedekindDomain.HeightOneSpectrum (Place.integralClosureAt F' v))
    (hP : P = Place.fiberCenter F' v hw)
    (x : Place.integralClosureAt F' v) (a : K)
    (hx : w.HasValue (algebraMap (Place.integralClosureAt F' v) F' x) a) :
    Algebra.norm (v.toValuationSubring ⧸ IsLocalRing.maximalIdeal v.toValuationSubring)
        (Ideal.Quotient.mk (P.asIdeal ^
            (IsLocalRing.maximalIdeal v.toValuationSubring).ramificationIdx' P.asIdeal) x) =
      Ideal.Quotient.mk (IsLocalRing.maximalIdeal v.toValuationSubring)
          (algebraMap K v.toValuationSubring a) ^
        (w.ramificationIndex F * w.inertiaDeg F)

theorem fiberCenter_mem_factors {K F F' : Type*} [Field K] [Field F] [Field F']
    [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
    [FiniteDimensional F F'] [Algebra.IsSeparable F F']
    (v : Place K F) {w : Place K F'} (hw : w.restrict F = v) :
    (Place.fiberCenter F' v hw).asIdeal ∈ (UniqueFactorizationMonoid.factors
      ((IsLocalRing.maximalIdeal v.toValuationSubring).map
        (algebraMap v.toValuationSubring (Place.integralClosureAt F' v)))).toFinset

theorem piQuotientEquiv_algebraMap {K F F' : Type*} [Field K] [Field F] [Field F']
    [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
    [FiniteDimensional F F'] [Algebra.IsSeparable F F']
    (v : Place K F)
    (hmap : (IsLocalRing.maximalIdeal v.toValuationSubring).map
      (algebraMap v.toValuationSubring (Place.integralClosureAt F' v)) ≠ ⊥)
    (r : v.toValuationSubring ⧸ IsLocalRing.maximalIdeal v.toValuationSubring) :
    factorsPiQuotientEquiv (S := Place.integralClosureAt F' v)
        (IsLocalRing.maximalIdeal v.toValuationSubring) hmap
        (algebraMap (v.toValuationSubring ⧸ IsLocalRing.maximalIdeal v.toValuationSubring)
          (Place.integralClosureAt F' v ⧸ (IsLocalRing.maximalIdeal v.toValuationSubring).map
            (algebraMap v.toValuationSubring (Place.integralClosureAt F' v))) r) =
      algebraMap (v.toValuationSubring ⧸ IsLocalRing.maximalIdeal v.toValuationSubring)
        (∀ Q : (UniqueFactorizationMonoid.factors
          ((IsLocalRing.maximalIdeal v.toValuationSubring).map
            (algebraMap v.toValuationSubring (Place.integralClosureAt F' v)))).toFinset,
          Place.integralClosureAt F' v ⧸ ((Q : Ideal (Place.integralClosureAt F' v)) ^
            (IsLocalRing.maximalIdeal v.toValuationSubring).ramificationIdx'
              (Q : Ideal (Place.integralClosureAt F' v)))) r

theorem norm_mk_map_eq_norm_pi {K F F' : Type*} [Field K] [Field F] [Field F']
    [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
    [FiniteDimensional F F'] [Algebra.IsSeparable F F']
    (v : Place K F) (x : Place.integralClosureAt F' v) :
    Algebra.norm (v.toValuationSubring ⧸ IsLocalRing.maximalIdeal v.toValuationSubring)
        (Ideal.Quotient.mk
          (Ideal.map (algebraMap v.toValuationSubring (Place.integralClosureAt F' v))
            (IsLocalRing.maximalIdeal v.toValuationSubring)) x) =
      Algebra.norm (v.toValuationSubring ⧸ IsLocalRing.maximalIdeal v.toValuationSubring)
        (fun Q : (UniqueFactorizationMonoid.factors
          ((IsLocalRing.maximalIdeal v.toValuationSubring).map
            (algebraMap v.toValuationSubring (Place.integralClosureAt F' v)))).toFinset =>
          Ideal.Quotient.mk ((Q : Ideal (Place.integralClosureAt F' v)) ^
            (IsLocalRing.maximalIdeal v.toValuationSubring).ramificationIdx'
              (Q : Ideal (Place.integralClosureAt F' v))) x) := by
  have hmap : (IsLocalRing.maximalIdeal v.toValuationSubring).map
      (algebraMap v.toValuationSubring (Place.integralClosureAt F' v)) ≠ ⊥ :=
    Ideal.map_ne_bot_of_ne_bot (Place.maximalIdeal_ne_bot v)
  exact (Algebra.norm_eq_of_algEquiv
      (AlgEquiv.ofRingEquiv (piQuotientEquiv_algebraMap v hmap)) _).symm.trans
    (congrArg _ ((AlgEquiv.ofRingEquiv_apply _ _).trans
      (factorsPiQuotientEquiv_mk (S := Place.integralClosureAt F' v)
        (IsLocalRing.maximalIdeal v.toValuationSubring) hmap x)))

theorem free_quotient_pow_factors {K F F' : Type*} [Field K] [Field F] [Field F']
    [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
    [FiniteDimensional F F'] [Algebra.IsSeparable F F']
    (v : Place K F)
    (Q : (UniqueFactorizationMonoid.factors
          ((IsLocalRing.maximalIdeal v.toValuationSubring).map
            (algebraMap v.toValuationSubring (Place.integralClosureAt F' v)))).toFinset) :
    Module.Free (v.toValuationSubring ⧸ IsLocalRing.maximalIdeal v.toValuationSubring)
      (Place.integralClosureAt F' v ⧸ (Q : Ideal (Place.integralClosureAt F' v)) ^
          (IsLocalRing.maximalIdeal v.toValuationSubring).ramificationIdx'
            (Q : Ideal (Place.integralClosureAt F' v)))

theorem finite_quotient_pow_factors {K F F' : Type*} [Field K] [Field F] [Field F']
    [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
    [FiniteDimensional F F'] [Algebra.IsSeparable F F']
    (v : Place K F)
    (Q : (UniqueFactorizationMonoid.factors
          ((IsLocalRing.maximalIdeal v.toValuationSubring).map
            (algebraMap v.toValuationSubring (Place.integralClosureAt F' v)))).toFinset) :
    Module.Finite (v.toValuationSubring ⧸ IsLocalRing.maximalIdeal v.toValuationSubring)
      (Place.integralClosureAt F' v ⧸ (Q : Ideal (Place.integralClosureAt F' v)) ^
          (IsLocalRing.maximalIdeal v.toValuationSubring).ramificationIdx'
            (Q : Ideal (Place.integralClosureAt F' v)))

theorem norm_mk_map_eq_prod_factors {K F F' : Type*} [Field K] [Field F] [Field F']
    [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
    [FiniteDimensional F F'] [Algebra.IsSeparable F F']
    (v : Place K F) (x : Place.integralClosureAt F' v) :
    Algebra.norm (v.toValuationSubring ⧸ IsLocalRing.maximalIdeal v.toValuationSubring)
        (Ideal.Quotient.mk
          (Ideal.map (algebraMap v.toValuationSubring (Place.integralClosureAt F' v))
            (IsLocalRing.maximalIdeal v.toValuationSubring)) x) =
      ∏ Q : (UniqueFactorizationMonoid.factors
          ((IsLocalRing.maximalIdeal v.toValuationSubring).map
            (algebraMap v.toValuationSubring (Place.integralClosureAt F' v)))).toFinset,
        Algebra.norm (v.toValuationSubring ⧸ IsLocalRing.maximalIdeal v.toValuationSubring)
          (Ideal.Quotient.mk ((Q : Ideal (Place.integralClosureAt F' v)) ^
            (IsLocalRing.maximalIdeal v.toValuationSubring).ramificationIdx'
              (Q : Ideal (Place.integralClosureAt F' v))) x)

theorem prod_fiberOver_eq_prod_factors {K F F' : Type*} [Field K] [Field F] [Field F']
    [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
    [FiniteDimensional F F'] [Algebra.IsSeparable F F']
    (v : Place K F) {β : Type*} [CommMonoid β]
    (g : (UniqueFactorizationMonoid.factors
      ((IsLocalRing.maximalIdeal v.toValuationSubring).map
        (algebraMap v.toValuationSubring (Place.integralClosureAt F' v)))).toFinset → β)
    (h : Place K F' → β)
    (hgh : ∀ (w : Place K F') (hw : w.restrict F = v),
      h w = g ⟨(Place.fiberCenter F' v hw).asIdeal, fiberCenter_mem_factors v hw⟩) :
    ∏ w ∈ v.fiberOver F', h w = ∏ Q, g Q

theorem norm_quotient_eq_prod {K F F' : Type*} [Field K] [Field F] [Field F']
    [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
    [FiniteDimensional F F'] [Algebra.IsSeparable F F']
    (v : Place K F)
    (x : Place.integralClosureAt F' v) (a : Place K F' → Kˣ)
    (ha : ∀ w ∈ v.fiberOver F', w.HasValue (algebraMap (Place.integralClosureAt F' v) F' x) (a w)) :
    Algebra.norm (v.toValuationSubring ⧸ IsLocalRing.maximalIdeal v.toValuationSubring)
        (Ideal.Quotient.mk
          (Ideal.map (algebraMap v.toValuationSubring (Place.integralClosureAt F' v))
            (IsLocalRing.maximalIdeal v.toValuationSubring)) x) =
      algebraMap K v.ResidueField
        (∏ w ∈ v.fiberOver F', (a w : K) ^ (w.ramificationIndex F * w.inertiaDeg F))

theorem residue_norm_unit {K F F' : Type*} [Field K] [Field F] [Field F']
    [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
    [FiniteDimensional F F'] [Algebra.IsSeparable F F']
    (v : Place K F)
    (b : (Place.integralClosureAt F' v)ˣ) (a : Place K F' → Kˣ)
    (ha : ∀ w ∈ v.fiberOver F', w.HasValue (algebraMap (Place.integralClosureAt F' v) F' b) (a w)) :
    IsLocalRing.residue v.toValuationSubring
        (Algebra.norm v.toValuationSubring (b : Place.integralClosureAt F' v)) =
      algebraMap K v.ResidueField
        (∏ w ∈ v.fiberOver F', (a w : K) ^ (w.ramificationIndex F * w.inertiaDeg F))

theorem hasValue_norm_of_unit {K F F' : Type*} [Field K] [Field F] [Field F']
    [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
    [FiniteDimensional F F'] [Algebra.IsSeparable F F']
    (v : Place K F) (b : (Place.integralClosureAt F' v)ˣ) (a : Place K F' → Kˣ)
    (ha : ∀ w ∈ v.fiberOver F', w.HasValue (algebraMap (Place.integralClosureAt F' v) F' b) (a w)) :
    v.HasValue (Algebra.norm F (algebraMap (Place.integralClosureAt F' v) F' b))
      (∏ w ∈ v.fiberOver F', (a w : K) ^ (w.ramificationIndex F * w.inertiaDeg F))

theorem hasValue_norm_of_forall_hasValue {K F F' : Type*} [Field K] [Field F] [Field F']
    [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
    [FiniteDimensional F F'] [Algebra.IsSeparable F F']
    (v : Place K F) (g : F') (a : Place K F' → Kˣ)
    (ha : ∀ w ∈ v.fiberOver F', w.HasValue g (a w)) :
    v.HasValue (Algebra.norm F g)
      (∏ w ∈ v.fiberOver F', (a w : K) ^ (w.ramificationIndex F * w.inertiaDeg F))

theorem _root_.AlgebraicCurve.Place.hasValue_norm_along_of_separableAlong {K F F' : Type*} [Field
  K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
    [HasPrincipalDivisors K F']
    (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral)
    (hfin : FiniteAlong K φ) (hsep : SeparableAlong K φ)
    (v : Place K F) (g : F') (a : Place K F' → Kˣ)
    (ha : ∀ w ∈ Place.fiberAlong φ hφ v, w.HasValue g (a w)) :
    letI := algebraAlong φ
    v.HasValue (Algebra.norm F g)
      (∏ w ∈ Place.fiberAlong φ hφ v,
        (a w : K) ^ (w.ramificationIndexAlong φ * w.inertiaDegAlong φ hφ)) := by
  let := algebraAlong φ
  have := isScalarTower_along φ
  have := isIntegral_along φ hφ
  have : FiniteDimensional F F' := hfin
  have : Algebra.IsSeparable F F' := hsep
  have hfib : Place.fiberAlong φ hφ v = v.fiberOver F' := by
    change v.fiber F' = v.fiberOver F'
    exact Place.fiber_eq_fiberOver v
  have ha' : ∀ w ∈ v.fiberOver F', w.HasValue g (a w) := by
    intro w hw
    exact ha w (hfib ▸ hw)
  have h := hasValue_norm_of_forall_hasValue v g a ha'
  rw [hfib]
  exact h