CurveModel_placeOfPoint_ofGenerator_iotaInf_comap.lean

theorem mem_valuationSubring_iff_exists {R F : Type*} [CommRing R] [IsDedekindDomain R] [Field F]
    [Algebra R F] [IsFractionRing R F] (w : HeightOneSpectrum R) (x : F) :
    x ∈ (w.valuation F).valuationSubring ↔
      ∃ a s : R, s ∉ w.asIdeal ∧ x = algebraMap R F a * (algebraMap R F s)⁻¹

theorem toSubring_ofHeightOneSpectrum_comap
    {K₀ K F₀ F : Type*} [Field K₀] [Field K] [Field F₀] [Field F] [Algebra K₀ F₀] [Algebra K F]
    {R₀ R : Type*} [CommRing R₀] [IsDedekindDomain R₀] [Algebra R₀ F₀] [IsFractionRing R₀ F₀]
    [Algebra K₀ R₀] [IsScalarTower K₀ R₀ F₀]
    [CommRing R] [IsDedekindDomain R] [Algebra R F] [IsFractionRing R F]
    [Algebra K R] [IsScalarTower K R F]
    (φ : F₀ →+* F) (ψ : R₀ →+* R) (hφψ : ∀ a : R₀, φ (algebraMap R₀ F₀ a) = algebraMap R F (ψ a))
    (w₀ : HeightOneSpectrum R₀) (w : HeightOneSpectrum R)
    (hw : w₀.asIdeal = w.asIdeal.comap ψ) :
    (Place.ofHeightOneSpectrum (K := K) w).toValuationSubring.toSubring.comap φ =
      (Place.ofHeightOneSpectrum (K := K₀) w₀).toValuationSubring.toSubring

theorem gluedPlaceOfPoint_ι₀_comap
    (K₀ : Type u) [Field K₀] {L₀ : Type u} [Field L₀] [Algebra K₀ L₀] (t₀ : L₀)
    (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
    [CharZero K₀] [Fact (t₀ ≠ 0)] [FiniteDimensional K₀⟮t₀⟯ L₀] [FiniteDimensional K₀⟮t₀⁻¹⟯ L₀]
    [CharZero K] [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L]
    (ht₀ : Transcendental K₀ t₀) (ht : Transcendental K t)
    (φ : L₀ →+* L) (ψ : chartRing K₀ ({t₀} : Set L₀) →+* chartRing K ({t} : Set L))
    (hφψ : ∀ a : chartRing K₀ ({t₀} : Set L₀), φ (a : L₀) = (ψ a : L))
    (xb : X₀ K t) (hxb : (ι₀ K t).base xb ∈ closedPoints (glued K t))
    (yb : X₀ K₀ t₀) (hyb : (ι₀ K₀ t₀).base yb ∈ closedPoints (glued K₀ t₀))
    (h : yb.asIdeal = xb.asIdeal.comap ψ) :
    (gluedPlaceOfPoint K t ht ⟨(ι₀ K t).base xb, hxb⟩).toValuationSubring.toSubring.comap φ =
      (gluedPlaceOfPoint K₀ t₀ ht₀ ⟨(ι₀ K₀ t₀).base yb, hyb⟩).toValuationSubring.toSubring

theorem gluedPlaceOfPoint_ιInf_comap
    (K₀ : Type u) [Field K₀] {L₀ : Type u} [Field L₀] [Algebra K₀ L₀] (t₀ : L₀)
    (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
    [CharZero K₀] [Fact (t₀ ≠ 0)] [FiniteDimensional K₀⟮t₀⟯ L₀] [FiniteDimensional K₀⟮t₀⁻¹⟯ L₀]
    [CharZero K] [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L]
    (ht₀ : Transcendental K₀ t₀) (ht : Transcendental K t)
    (φ : L₀ →+* L) (ψ : chartRing K₀ ({t₀⁻¹} : Set L₀) →+* chartRing K ({t⁻¹} : Set L))
    (hφψ : ∀ a : chartRing K₀ ({t₀⁻¹} : Set L₀), φ (a : L₀) = (ψ a : L))
    (x : closedPoints (glued K t)) (hx : x.1 ∉ Set.range (ι₀ K t).base)
    (xb : XInf K t) (hxb : (ιInf K t).base xb = x.1)
    (y : closedPoints (glued K₀ t₀)) (hy : y.1 ∉ Set.range (ι₀ K₀ t₀).base)
    (yb : XInf K₀ t₀) (hyb : (ιInf K₀ t₀).base yb = y.1)
    (h : yb.asIdeal = xb.asIdeal.comap ψ) :
    (gluedPlaceOfPoint K t ht x).toValuationSubring.toSubring.comap φ =
      (gluedPlaceOfPoint K₀ t₀ ht₀ y).toValuationSubring.toSubring

theorem placeOfPoint_ofGenerator_iota0_comap
    (K₀ : Type u) [Field K₀] {L₀ : Type u} [Field L₀] [Algebra K₀ L₀] (t₀ : L₀)
    (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
    [CharZero K₀] [Fact (t₀ ≠ 0)] [FiniteDimensional K₀⟮t₀⟯ L₀] [FiniteDimensional K₀⟮t₀⁻¹⟯ L₀]
    [CharZero K] [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L]
    (ht₀ : Transcendental K₀ t₀) (ht : Transcendental K t)
    (φ : L₀ →+* L) (ψ : chartRing K₀ ({t₀} : Set L₀) →+* chartRing K ({t} : Set L))
    (hφψ : ∀ a : chartRing K₀ ({t₀} : Set L₀), φ (a : L₀) = (ψ a : L))
    (xb : X₀ K t) (hxb : (ι₀ K t).base xb ∈ closedPoints (CurveModel.ofGenerator K t ht).C)
    (yb : X₀ K₀ t₀) (hyb : (ι₀ K₀ t₀).base yb ∈ closedPoints (CurveModel.ofGenerator K₀ t₀ ht₀).C)
    (h : yb.asIdeal = xb.asIdeal.comap ψ) :
    ((CurveModel.ofGenerator K t ht).placeOfPoint ⟨(ι₀ K t).base xb,
      hxb⟩).toValuationSubring.toSubring.comap φ =
      ((CurveModel.ofGenerator K₀ t₀ ht₀).placeOfPoint ⟨(ι₀ K₀ t₀).base yb,
        hyb⟩).toValuationSubring.toSubring

theorem placeOfPoint_ofGenerator_iotaInf_comap'
    (K₀ : Type u) [Field K₀] {L₀ : Type u} [Field L₀] [Algebra K₀ L₀] (t₀ : L₀)
    (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
    [CharZero K₀] [Fact (t₀ ≠ 0)] [FiniteDimensional K₀⟮t₀⟯ L₀] [FiniteDimensional K₀⟮t₀⁻¹⟯ L₀]
    [CharZero K] [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L]
    (ht₀ : Transcendental K₀ t₀) (ht : Transcendental K t)
    (φ : L₀ →+* L) (ψ : chartRing K₀ ({t₀⁻¹} : Set L₀) →+* chartRing K ({t⁻¹} : Set L))
    (hφψ : ∀ a : chartRing K₀ ({t₀⁻¹} : Set L₀), φ (a : L₀) = (ψ a : L))
    (x : closedPoints (CurveModel.ofGenerator K t ht).C) (hx : x.1 ∉ Set.range (ι₀ K t).base)
    (xb : XInf K t) (hxb : (ιInf K t).base xb = x.1)
    (y : closedPoints (CurveModel.ofGenerator K₀ t₀ ht₀).C) (hy : y.1 ∉ Set.range (ι₀ K₀ t₀).base)
    (yb : XInf K₀ t₀) (hyb : (ιInf K₀ t₀).base yb = y.1)
    (h : yb.asIdeal = xb.asIdeal.comap ψ) :
    ((CurveModel.ofGenerator K t ht).placeOfPoint x).toValuationSubring.toSubring.comap φ =
      ((CurveModel.ofGenerator K₀ t₀ ht₀).placeOfPoint y).toValuationSubring.toSubring

theorem _root_.AlgebraicCurve.CurveModel.placeOfPoint_ofGenerator_iotaInf_comap
    (K₀ : Type u) [Field K₀] {L₀ : Type u} [Field L₀] [Algebra K₀ L₀] (t₀ : L₀)
    (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L] (t : L)
    [CharZero K₀] [Fact (t₀ ≠ 0)] [FiniteDimensional K₀⟮t₀⟯ L₀] [FiniteDimensional K₀⟮t₀⁻¹⟯ L₀]
    [CharZero K] [Fact (t ≠ 0)] [FiniteDimensional K⟮t⟯ L] [FiniteDimensional K⟮t⁻¹⟯ L]
    (ht₀ : Transcendental K₀ t₀) (ht : Transcendental K t)
    (φ : L₀ →+* L) (ψ : chartRing K₀ ({t₀⁻¹} : Set L₀) →+* chartRing K ({t⁻¹} : Set L))
    (hφψ : ∀ a : chartRing K₀ ({t₀⁻¹} : Set L₀), φ (a : L₀) = (ψ a : L))
    (x : closedPoints (CurveModel.ofGenerator K t ht).C) (hx : x.1 ∉ Set.range (ι₀ K t).base)
    (xb : XInf K t) (hxb : (ιInf K t).base xb = x.1)
    (y : closedPoints (CurveModel.ofGenerator K₀ t₀ ht₀).C) (hy : y.1 ∉ Set.range (ι₀ K₀ t₀).base)
    (yb : XInf K₀ t₀) (hyb : (ιInf K₀ t₀).base yb = y.1)
    (h : yb.asIdeal = xb.asIdeal.comap ψ) :
    ((CurveModel.ofGenerator K t ht).placeOfPoint x).toValuationSubring.toSubring.comap φ =
      ((CurveModel.ofGenerator K₀ t₀ ht₀).placeOfPoint y).toValuationSubring.toSubring