AlgebraicCurve.CurveModel.place_eq_of_pointEquivPlace_symm_comp_eq
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_place_eq_of_pointEquivPlace_symm_comp_eq
open CategoryTheory AlgebraicGeometry AlgebraicCurve
universe u vLean source · statement
theorem _root_.AlgebraicCurve.CurveModel.place_eq_of_pointEquivPlace_symm_comp_eq
{K : Type u} [Field K] [IsAlgClosed K] {L : Type v} [Field L] [Algebra K L]
(𝔐 : AlgebraicCurve.CurveModel K L)
{X B : Scheme.{u}} (πX : X ⟶ B) (s : Spec (CommRingCat.of K) ⟶ B)
(e : 𝔐.C ⟶ CategoryTheory.Limits.pullback πX s) (he : IsIso e)
(he_snd : e ≫ CategoryTheory.Limits.pullback.snd πX s = 𝔐.toBase)
(P Q : Place K L)
(h : (𝔐.pointEquivPlace.symm P).1 ≫ e ≫ CategoryTheory.Limits.pullback.fst πX s =
(𝔐.pointEquivPlace.symm Q).1 ≫ e ≫ CategoryTheory.Limits.pullback.fst πX s) :
P = Q