AlgebraicCurve.Place.restrictAlong_congrEquiv_and_existsUnique_iff
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_restrictAlong_congrEquiv_and_existsUnique_iff
open AlgebraicCurveLean source · statement
theorem _root_.AlgebraicCurve.Place.restrictAlong_congrEquiv_and_existsUnique_iff
{K E F F' : Type*} [Field K] [Field E] [Field F] [Field F'] [Algebra K E] [Algebra K F]
[Algebra K F']
(φ : E →ₐ[K] F) (hφ : φ.toRingHom.IsIntegral) (φ' : E →ₐ[K] F') (hφ' : φ'.toRingHom.IsIntegral)
(e : F ≃+* F') (he : ∀ a : K, e (algebraMap K F a) = algebraMap K F' a)
(hcomm : ∀ x : E, e (φ x) = φ' x) :
(∀ w : Place K F, (Place.congrEquiv e he w).restrictAlong φ' hφ' = w.restrictAlong φ hφ) ∧
(∀ s : Place K E, ∀ w' : Place K F', w'.restrictAlong φ' hφ' = s ↔
((Place.congrEquiv e he).symm w').restrictAlong φ hφ = s) ∧
(∀ s : Place K E, (∃! w : Place K F, w.restrictAlong φ hφ = s) ↔
(∃! w' : Place K F', w'.restrictAlong φ' hφ' = s))