NYLL
Module

Place_smul_eq_of_comap_eq_of_forall_sub_mem_nonunits.lean

Nyll.AlgebraicCurves.Places.Place_smul_eq_of_comap_eq_of_forall_sub_mem_nonunits
16 declarations indexed from sourceView source ↗

Module documentation

Place smul eq of comap eq of forall sub mem nonunits

Imports2
Imported by1

Declarations

def

constantBaseRing

L41 ↗
AlgebraicCurves.Places.Proofs.Place_smul_eq_of_comap_eq_of_forall_sub_mem_nonunits.AlgebraicCurve.Place.constantBaseRing
Documentation

The subring generated by the original valuation ring and the extended constants.

Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_smul_eq_of_comap_eq_of_forall_sub_mem_nonunits
open _root_.AlgebraicCurve
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
variable {κ : Type*} [Field κ] {F : Type*} [Field F] [Algebra κ F]
  {κ' : Type*} [Field κ'] [Algebra κ κ']
  {F' : Type*} [Field F'] [Algebra κ' F'] [Algebra F F'] [Algebra κ F']
  [IsScalarTower κ F F'] [IsScalarTower κ κ' F']
variable (κ') in
Lean source · statement
def constantBaseRing (P : Place κ F) : Subring F'
def

constantBaseIdeal

L48 ↗
AlgebraicCurves.Places.Proofs.Place_smul_eq_of_comap_eq_of_forall_sub_mem_nonunits.AlgebraicCurve.Place.constantBaseIdeal
Documentation

The additive subgroup generated by products of original nonunits with the constant-extension ring.

Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_smul_eq_of_comap_eq_of_forall_sub_mem_nonunits
open _root_.AlgebraicCurve
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
variable {κ : Type*} [Field κ] {F : Type*} [Field F] [Algebra κ F]
  {κ' : Type*} [Field κ'] [Algebra κ κ']
  {F' : Type*} [Field F'] [Algebra κ' F'] [Algebra F F'] [Algebra κ F']
  [IsScalarTower κ F F'] [IsScalarTower κ κ' F']
variable (κ') in
variable (κ') in
Lean source · statement
def constantBaseIdeal (P : Place κ F) : AddSubgroup F'
theorem

algebraMap_mem_constantBaseRing

L53 ↗
AlgebraicCurves.Places.Proofs.Place_smul_eq_of_comap_eq_of_forall_sub_mem_nonunits.AlgebraicCurve.Place.algebraMap_mem_constantBaseRing
Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_smul_eq_of_comap_eq_of_forall_sub_mem_nonunits
open _root_.AlgebraicCurve
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
variable {κ : Type*} [Field κ] {F : Type*} [Field F] [Algebra κ F]
  {κ' : Type*} [Field κ'] [Algebra κ κ']
  {F' : Type*} [Field F'] [Algebra κ' F'] [Algebra F F'] [Algebra κ F']
  [IsScalarTower κ F F'] [IsScalarTower κ κ' F']
variable (κ') in
variable (κ') in
omit [Algebra κ κ'] [Algebra κ F'] [IsScalarTower κ F F'] [IsScalarTower κ κ' F'] in
Lean source · statement
theorem algebraMap_mem_constantBaseRing (P : Place κ F) {f : F} (hf : f ∈ P.toValuationSubring) :
    algebraMap F F' f ∈ constantBaseRing κ' P
theorem

algebraMap_const_mem_constantBaseRing

L57 ↗
AlgebraicCurves.Places.Proofs.Place_smul_eq_of_comap_eq_of_forall_sub_mem_nonunits.AlgebraicCurve.Place.algebraMap_const_mem_constantBaseRing
Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_smul_eq_of_comap_eq_of_forall_sub_mem_nonunits
open _root_.AlgebraicCurve
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
variable {κ : Type*} [Field κ] {F : Type*} [Field F] [Algebra κ F]
  {κ' : Type*} [Field κ'] [Algebra κ κ']
  {F' : Type*} [Field F'] [Algebra κ' F'] [Algebra F F'] [Algebra κ F']
  [IsScalarTower κ F F'] [IsScalarTower κ κ' F']
variable (κ') in
variable (κ') in
omit [Algebra κ κ'] [Algebra κ F'] [IsScalarTower κ F F'] [IsScalarTower κ κ' F'] in
Lean source · statement
theorem algebraMap_const_mem_constantBaseRing (P : Place κ F) (c : κ') :
    algebraMap κ' F' c ∈ constantBaseRing κ' (F := F) P
theorem

mul_mem_constantBaseIdeal

L61 ↗
AlgebraicCurves.Places.Proofs.Place_smul_eq_of_comap_eq_of_forall_sub_mem_nonunits.AlgebraicCurve.Place.mul_mem_constantBaseIdeal
Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_smul_eq_of_comap_eq_of_forall_sub_mem_nonunits
open _root_.AlgebraicCurve
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
variable {κ : Type*} [Field κ] {F : Type*} [Field F] [Algebra κ F]
  {κ' : Type*} [Field κ'] [Algebra κ κ']
  {F' : Type*} [Field F'] [Algebra κ' F'] [Algebra F F'] [Algebra κ F']
  [IsScalarTower κ F F'] [IsScalarTower κ κ' F']
variable (κ') in
variable (κ') in
omit [Algebra κ κ'] [Algebra κ F'] [IsScalarTower κ F F'] [IsScalarTower κ κ' F'] in
Lean source · statement
theorem mul_mem_constantBaseIdeal (P : Place κ F) {m : F} (hm : m ∈ P.toValuationSubring.nonunits)
  {r : F'}
    (hr : r ∈ constantBaseRing κ' P) : algebraMap F F' m * r ∈ constantBaseIdeal κ' P
theorem

constantBaseIdeal_mul_mem

L66 ↗
AlgebraicCurves.Places.Proofs.Place_smul_eq_of_comap_eq_of_forall_sub_mem_nonunits.AlgebraicCurve.Place.constantBaseIdeal_mul_mem
Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_smul_eq_of_comap_eq_of_forall_sub_mem_nonunits
open _root_.AlgebraicCurve
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
variable {κ : Type*} [Field κ] {F : Type*} [Field F] [Algebra κ F]
  {κ' : Type*} [Field κ'] [Algebra κ κ']
  {F' : Type*} [Field F'] [Algebra κ' F'] [Algebra F F'] [Algebra κ F']
  [IsScalarTower κ F F'] [IsScalarTower κ κ' F']
variable (κ') in
variable (κ') in
omit [Algebra κ κ'] [Algebra κ F'] [IsScalarTower κ F F'] [IsScalarTower κ κ' F'] in
Lean source · statement
theorem constantBaseIdeal_mul_mem (P : Place κ F) {y : F'} (hy : y ∈ constantBaseIdeal κ' P) {r :
  F'}
    (hr : r ∈ constantBaseRing κ' P) : y * r ∈ constantBaseIdeal κ' P
theorem

mul_constantBaseIdeal_mem

L78 ↗
AlgebraicCurves.Places.Proofs.Place_smul_eq_of_comap_eq_of_forall_sub_mem_nonunits.AlgebraicCurve.Place.mul_constantBaseIdeal_mem
Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_smul_eq_of_comap_eq_of_forall_sub_mem_nonunits
open _root_.AlgebraicCurve
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
variable {κ : Type*} [Field κ] {F : Type*} [Field F] [Algebra κ F]
  {κ' : Type*} [Field κ'] [Algebra κ κ']
  {F' : Type*} [Field F'] [Algebra κ' F'] [Algebra F F'] [Algebra κ F']
  [IsScalarTower κ F F'] [IsScalarTower κ κ' F']
variable (κ') in
variable (κ') in
omit [Algebra κ κ'] [Algebra κ F'] [IsScalarTower κ F F'] [IsScalarTower κ κ' F'] in
Lean source · statement
theorem mul_constantBaseIdeal_mem (P : Place κ F) {y : F'} (hy : y ∈ constantBaseIdeal κ' P) {r :
  F'}
    (hr : r ∈ constantBaseRing κ' P) : r * y ∈ constantBaseIdeal κ' P
theorem

smul_mem_of_smul_eq

L90 ↗
AlgebraicCurves.Places.Proofs.Place_smul_eq_of_comap_eq_of_forall_sub_mem_nonunits.AlgebraicCurve.Place.smul_mem_of_smul_eq
Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_smul_eq_of_comap_eq_of_forall_sub_mem_nonunits
open _root_.AlgebraicCurve
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
variable {κ : Type*} [Field κ] {F : Type*} [Field F] [Algebra κ F]
  {κ' : Type*} [Field κ'] [Algebra κ κ']
  {F' : Type*} [Field F'] [Algebra κ' F'] [Algebra F F'] [Algebra κ F']
  [IsScalarTower κ F F'] [IsScalarTower κ κ' F']
variable (κ') in
variable (κ') in
Lean source · statement
theorem smul_mem_of_smul_eq {σ : F ≃ₐ[κ] F} {P : Place κ F} (hP : σ • P = P) {f : F} (hf : f ∈
  P.toValuationSubring) :
    σ f ∈ P.toValuationSubring
theorem

smul_mem_constantBaseRing_and_sub_mem_of_forall_sub_mem_nonunits

L97 ↗
AlgebraicCurves.Places.Proofs.Place_smul_eq_of_comap_eq_of_forall_sub_mem_nonunits.AlgebraicCurve.Place.smul_mem_constantBaseRing_and_sub_mem_of_forall_sub_mem_nonunits
Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_smul_eq_of_comap_eq_of_forall_sub_mem_nonunits
open _root_.AlgebraicCurve
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
variable {κ : Type*} [Field κ] {F : Type*} [Field F] [Algebra κ F]
  {κ' : Type*} [Field κ'] [Algebra κ κ']
  {F' : Type*} [Field F'] [Algebra κ' F'] [Algebra F F'] [Algebra κ F']
  [IsScalarTower κ F F'] [IsScalarTower κ κ' F']
variable (κ') in
variable (κ') in
omit [Algebra κ κ'] [Algebra κ F'] [IsScalarTower κ F F'] [IsScalarTower κ κ' F'] in
Lean source · statement
theorem smul_mem_constantBaseRing_and_sub_mem_of_forall_sub_mem_nonunits
    (σ : F ≃ₐ[κ] F) (σ' : F' ≃ₐ[κ'] F')
    (hσ : ∀ f : F, σ' (algebraMap F F' f) = algebraMap F F' (σ f))
    (P : Place κ F) (hP : σ • P = P)
    (hI : ∀ e : F, e ∈ P.toValuationSubring → σ e - e ∈ P.toValuationSubring.nonunits)
    (x : F') (hx : x ∈ constantBaseRing κ' P) :
    σ' x ∈ constantBaseRing κ' P ∧ σ' x - x ∈ constantBaseIdeal κ' P
theorem

mem_of_comap_eq

L131 ↗
AlgebraicCurves.Places.Proofs.Place_smul_eq_of_comap_eq_of_forall_sub_mem_nonunits.AlgebraicCurve.Place.mem_of_comap_eq
Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_smul_eq_of_comap_eq_of_forall_sub_mem_nonunits
open _root_.AlgebraicCurve
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
variable {κ : Type*} [Field κ] {F : Type*} [Field F] [Algebra κ F]
  {κ' : Type*} [Field κ'] [Algebra κ κ']
  {F' : Type*} [Field F'] [Algebra κ' F'] [Algebra F F'] [Algebra κ F']
  [IsScalarTower κ F F'] [IsScalarTower κ κ' F']
variable (κ') in
variable (κ') in
omit [Algebra κ κ'] [Algebra κ F'] [IsScalarTower κ F F'] [IsScalarTower κ κ' F'] in
Lean source · statement
theorem mem_of_comap_eq {P : Place κ F} {P' : Place κ' F'}
    (hP' : P'.toValuationSubring.comap (algebraMap F F') = P.toValuationSubring) (f : F) :
    f ∈ P.toValuationSubring ↔ algebraMap F F' f ∈ P'.toValuationSubring
theorem

constantBaseRing_le

L136 ↗
AlgebraicCurves.Places.Proofs.Place_smul_eq_of_comap_eq_of_forall_sub_mem_nonunits.AlgebraicCurve.Place.constantBaseRing_le
Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_smul_eq_of_comap_eq_of_forall_sub_mem_nonunits
open _root_.AlgebraicCurve
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
variable {κ : Type*} [Field κ] {F : Type*} [Field F] [Algebra κ F]
  {κ' : Type*} [Field κ'] [Algebra κ κ']
  {F' : Type*} [Field F'] [Algebra κ' F'] [Algebra F F'] [Algebra κ F']
  [IsScalarTower κ F F'] [IsScalarTower κ κ' F']
variable (κ') in
variable (κ') in
omit [Algebra κ κ'] [Algebra κ F'] [IsScalarTower κ F F'] [IsScalarTower κ κ' F'] in
Lean source · statement
theorem constantBaseRing_le {P : Place κ F} {P' : Place κ' F'}
    (hP' : P'.toValuationSubring.comap (algebraMap F F') = P.toValuationSubring) :
    constantBaseRing κ' P ≤ P'.toValuationSubring.toSubring
theorem

algebraMap_mem_nonunits

L144 ↗
AlgebraicCurves.Places.Proofs.Place_smul_eq_of_comap_eq_of_forall_sub_mem_nonunits.AlgebraicCurve.Place.algebraMap_mem_nonunits
Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_smul_eq_of_comap_eq_of_forall_sub_mem_nonunits
open _root_.AlgebraicCurve
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
variable {κ : Type*} [Field κ] {F : Type*} [Field F] [Algebra κ F]
  {κ' : Type*} [Field κ'] [Algebra κ κ']
  {F' : Type*} [Field F'] [Algebra κ' F'] [Algebra F F'] [Algebra κ F']
  [IsScalarTower κ F F'] [IsScalarTower κ κ' F']
variable (κ') in
variable (κ') in
omit [Algebra κ κ'] [Algebra κ F'] [IsScalarTower κ F F'] [IsScalarTower κ κ' F'] in
Lean source · statement
theorem algebraMap_mem_nonunits {P : Place κ F} {P' : Place κ' F'}
    (hP' : P'.toValuationSubring.comap (algebraMap F F') = P.toValuationSubring) {m : F}
    (hm : m ∈ P.toValuationSubring.nonunits) : algebraMap F F' m ∈ P'.toValuationSubring.nonunits
theorem

constantBaseIdeal_le_nonunits

L155 ↗
AlgebraicCurves.Places.Proofs.Place_smul_eq_of_comap_eq_of_forall_sub_mem_nonunits.AlgebraicCurve.Place.constantBaseIdeal_le_nonunits
Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_smul_eq_of_comap_eq_of_forall_sub_mem_nonunits
open _root_.AlgebraicCurve
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
variable {κ : Type*} [Field κ] {F : Type*} [Field F] [Algebra κ F]
  {κ' : Type*} [Field κ'] [Algebra κ κ']
  {F' : Type*} [Field F'] [Algebra κ' F'] [Algebra F F'] [Algebra κ F']
  [IsScalarTower κ F F'] [IsScalarTower κ κ' F']
variable (κ') in
variable (κ') in
omit [Algebra κ κ'] [Algebra κ F'] [IsScalarTower κ F F'] [IsScalarTower κ κ' F'] in
Lean source · statement
theorem constantBaseIdeal_le_nonunits {P : Place κ F} {P' : Place κ' F'}
    (hP' : P'.toValuationSubring.comap (algebraMap F F') = P.toValuationSubring) {y : F'}
    (hy : y ∈ constantBaseIdeal κ' P) : y ∈ P'.toValuationSubring.nonunits
theorem

mem_nonunits_iff_smul_mem

L173 ↗
AlgebraicCurves.Places.Proofs.Place_smul_eq_of_comap_eq_of_forall_sub_mem_nonunits.AlgebraicCurve.Place.mem_nonunits_iff_smul_mem
Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_smul_eq_of_comap_eq_of_forall_sub_mem_nonunits
open _root_.AlgebraicCurve
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
variable {κ : Type*} [Field κ] {F : Type*} [Field F] [Algebra κ F]
  {κ' : Type*} [Field κ'] [Algebra κ κ']
  {F' : Type*} [Field F'] [Algebra κ' F'] [Algebra F F'] [Algebra κ F']
  [IsScalarTower κ F F'] [IsScalarTower κ κ' F']
variable (κ') in
variable (κ') in
omit [Algebra κ κ'] [Algebra κ F'] [IsScalarTower κ F F'] [IsScalarTower κ κ' F'] in
Lean source · statement
theorem mem_nonunits_iff_smul_mem (σ : F ≃ₐ[κ] F) (σ' : F' ≃ₐ[κ'] F')
    (hσ : ∀ f : F, σ' (algebraMap F F' f) = algebraMap F F' (σ f))
    (P : Place κ F) (hP : σ • P = P)
    (hI : ∀ e : F, e ∈ P.toValuationSubring → σ e - e ∈ P.toValuationSubring.nonunits)
    {P' : Place κ' F'} (hP' : P'.toValuationSubring.comap (algebraMap F F') = P.toValuationSubring)
    {x : F'} (hx : x ∈ constantBaseRing κ' P) :
    x ∈ P'.toValuationSubring.nonunits ↔ σ' x ∈ P'.toValuationSubring.nonunits
theorem

mem_nonunits_smul_iff

L191 ↗
AlgebraicCurves.Places.Proofs.Place_smul_eq_of_comap_eq_of_forall_sub_mem_nonunits.AlgebraicCurve.Place.mem_nonunits_smul_iff
Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_smul_eq_of_comap_eq_of_forall_sub_mem_nonunits
open _root_.AlgebraicCurve
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
variable {κ : Type*} [Field κ] {F : Type*} [Field F] [Algebra κ F]
  {κ' : Type*} [Field κ'] [Algebra κ κ']
  {F' : Type*} [Field F'] [Algebra κ' F'] [Algebra F F'] [Algebra κ F']
  [IsScalarTower κ F F'] [IsScalarTower κ κ' F']
variable (κ') in
variable (κ') in
Lean source · statement
theorem mem_nonunits_smul_iff (σ' : F' ≃ₐ[κ'] F') (P' : Place κ' F') (x : F') :
    x ∈ (σ' • P').toValuationSubring.nonunits ↔ σ'.symm x ∈ P'.toValuationSubring.nonunits
theorem

smul_eq_of_comap_eq_of_forall_sub_mem_nonunits

L202 ↗
AlgebraicCurve.Place.smul_eq_of_comap_eq_of_forall_sub_mem_nonunits
Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_smul_eq_of_comap_eq_of_forall_sub_mem_nonunits
open _root_.AlgebraicCurve
open scoped Pointwise
open _root_.AlgebraicCurve.Place AlgebraicCurve.Place in
Lean source · statement
theorem _root_.AlgebraicCurve.Place.smul_eq_of_comap_eq_of_forall_sub_mem_nonunits
    {κ : Type*} [Field κ] {F : Type*} [Field F] [Algebra κ F]
    {κ' : Type*} [Field κ'] [Algebra κ κ'] [Algebra.IsAlgebraic κ κ'] [Algebra.IsSeparable κ κ']
    {F' : Type*} [Field F'] [Algebra κ' F'] [Algebra F F'] [Algebra κ F']
    [IsScalarTower κ F F'] [IsScalarTower κ κ' F']
    (hgen : Algebra.adjoin F (Set.range (algebraMap κ' F')) = ⊤)
    (σ : F ≃ₐ[κ] F) (σ' : F' ≃ₐ[κ'] F')
    (hσ : ∀ f : F, σ' (algebraMap F F' f) = algebraMap F F' (σ f))
    (P : Place κ F) (hP : σ • P = P)
    (hI : ∀ e : F, e ∈ P.toValuationSubring → σ e - e ∈ P.toValuationSubring.nonunits)
    (P' : Place κ' F')
    (hP' : P'.toValuationSubring.comap (algebraMap F F') = P.toValuationSubring) :
    σ' • P' = P'

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.