Module

Place_eq_of_comap_eq_of_forall_mem_nonunits_iff.lean

Nyll.AlgebraicCurves.Places.Place_eq_of_comap_eq_of_forall_mem_nonunits_iff

8 declarations indexed from sourceView source ↗

Module documentation

Place eq of comap eq of forall mem nonunits iff

Imports2

Imported by2

theorem

mem_nonunits_comap_iff

L36 ↗

AlgebraicCurves.Places.Proofs.Place_eq_of_comap_eq_of_forall_mem_nonunits_iff.AlgebraicCurve.ValLoc.mem_nonunits_comap_iff

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_eq_of_comap_eq_of_forall_mem_nonunits_iff
open _root_.AlgebraicCurve
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace ValLoc
open _root_.AlgebraicCurve
section Transport
variable {K K' : Type*} [Field K] [Field K']

Lean source · statement

theorem mem_nonunits_comap_iff (A : ValuationSubring K') (φ : K →+* K') (x : K) :
    x ∈ (A.comap φ).nonunits ↔ φ x ∈ A.nonunits

theorem

inv_mem_of_not_mem_nonunits

L42 ↗

AlgebraicCurves.Places.Proofs.Place_eq_of_comap_eq_of_forall_mem_nonunits_iff.AlgebraicCurve.ValLoc.inv_mem_of_not_mem_nonunits

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_eq_of_comap_eq_of_forall_mem_nonunits_iff
open _root_.AlgebraicCurve
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace ValLoc
open _root_.AlgebraicCurve
section Transport
variable {K K' : Type*} [Field K] [Field K']

Lean source · statement

theorem inv_mem_of_not_mem_nonunits (A : ValuationSubring K) {x : K} (h : x ∉ A.nonunits) : x⁻¹ ∈ A

theorem

ne_top_of_mem_nonunits

L47 ↗

AlgebraicCurves.Places.Proofs.Place_eq_of_comap_eq_of_forall_mem_nonunits_iff.AlgebraicCurve.ValLoc.ne_top_of_mem_nonunits

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_eq_of_comap_eq_of_forall_mem_nonunits_iff
open _root_.AlgebraicCurve
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace ValLoc
open _root_.AlgebraicCurve
section Transport
variable {K K' : Type*} [Field K] [Field K']

Lean source · statement

theorem ne_top_of_mem_nonunits (A : ValuationSubring K) {x : K} (hx : x ∈ A.nonunits) (hx0 : x ≠ 0)
  : A ≠ ⊤

theorem

exists_finset_mem_adjoin

L64 ↗

AlgebraicCurves.Places.Proofs.Place_eq_of_comap_eq_of_forall_mem_nonunits_iff.AlgebraicCurve.ValLoc.exists_finset_mem_adjoin

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_eq_of_comap_eq_of_forall_mem_nonunits_iff
open _root_.AlgebraicCurve
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace ValLoc
open _root_.AlgebraicCurve
section PrimElt
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']

Lean source · statement

theorem exists_finset_mem_adjoin (hgen : Algebra.adjoin F (Set.range (algebraMap κ' F')) = ⊤) (x :
  F') :
    ∃ T : Finset κ', x ∈ Algebra.adjoin F ((algebraMap κ' F') '' (T : Set κ'))

theorem

exists_mem_adjoin_simple

L90 ↗

AlgebraicCurves.Places.Proofs.Place_eq_of_comap_eq_of_forall_mem_nonunits_iff.AlgebraicCurve.ValLoc.exists_mem_adjoin_simple

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_eq_of_comap_eq_of_forall_mem_nonunits_iff
open _root_.AlgebraicCurve
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace ValLoc
open _root_.AlgebraicCurve
section PrimElt
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 [Algebra.IsAlgebraic κ κ'] [Algebra.IsSeparable κ κ']

Lean source · statement

theorem exists_mem_adjoin_simple (hgen : Algebra.adjoin F (Set.range (algebraMap κ' F')) = ⊤) (x :
  F') :
    ∃ c : F', c ∈ Set.range (algebraMap κ' F') ∧ IsIntegral κ c ∧ (minpoly κ c).Separable ∧
      x ∈ IntermediateField.adjoin F ({c} : Set F')

theorem

isIntegral_map_of_comap_eq

L140 ↗

AlgebraicCurves.Places.Proofs.Place_eq_of_comap_eq_of_forall_mem_nonunits_iff.AlgebraicCurve.ValLoc.isIntegral_map_of_comap_eq

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_eq_of_comap_eq_of_forall_mem_nonunits_iff
open _root_.AlgebraicCurve
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace ValLoc
open _root_.AlgebraicCurve
section Key
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']
omit [Algebra κ κ'] [Algebra κ F'] [IsScalarTower κ F F'] [IsScalarTower κ κ' F'] in

Lean source · statement

theorem isIntegral_map_of_comap_eq {P : Place κ F} {W : Place κ' F'}
    (hW : W.toValuationSubring.comap (algebraMap F F') = P.toValuationSubring)
    {L : IntermediateField F F'} {z : L}
    (hz : @IsIntegral P.toValuationSubring L _ _ (((algebraMap F L).comp
      P.toValuationSubring.subtype).toAlgebra) z) :
    IsIntegral W.toValuationSubring ((z : F'))

theorem

mem_iff_mem_of_mem_adjoin_simple

L164 ↗

AlgebraicCurves.Places.Proofs.Place_eq_of_comap_eq_of_forall_mem_nonunits_iff.AlgebraicCurve.ValLoc.mem_iff_mem_of_mem_adjoin_simple

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_eq_of_comap_eq_of_forall_mem_nonunits_iff
open _root_.AlgebraicCurve
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace ValLoc
open _root_.AlgebraicCurve
section Key
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']
omit [IsScalarTower κ κ' F'] in

Lean source · statement

theorem mem_iff_mem_of_mem_adjoin_simple [Algebra.IsAlgebraic κ κ'] [Algebra.IsSeparable κ κ']
    (P : Place κ F) (W₁ W₂ : Place κ' F')
    (h₁ : W₁.toValuationSubring.comap (algebraMap F F') = P.toValuationSubring)
    (h₂ : W₂.toValuationSubring.comap (algebraMap F F') = P.toValuationSubring)
    (hc : ∀ x ∈ Subring.closure
        ((algebraMap F F') '' (P.toValuationSubring : Set F) ∪ Set.range (algebraMap κ' F')),
      x ∈ W₁.toValuationSubring.nonunits ↔ x ∈ W₂.toValuationSubring.nonunits)
    (c : F') (hcR : c ∈ Set.range (algebraMap κ' F')) (hci : IsIntegral κ c) (hsep : (minpoly κ
      c).Separable)
    (x : F') (hx : x ∈ IntermediateField.adjoin F ({c} : Set F')) :
    x ∈ W₁.toValuationSubring ↔ x ∈ W₂.toValuationSubring

theorem

eq_of_comap_eq_of_forall_mem_nonunits_iff

L287 ↗

AlgebraicCurve.Place.eq_of_comap_eq_of_forall_mem_nonunits_iff

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_eq_of_comap_eq_of_forall_mem_nonunits_iff
open _root_.AlgebraicCurve
open scoped Pointwise
open AlgebraicCurve.ValLoc in

Lean source · statement

theorem _root_.AlgebraicCurve.Place.eq_of_comap_eq_of_forall_mem_nonunits_iff
    {κ : 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'] [Algebra.IsIntegral F F']
    (hgen : Algebra.adjoin F (Set.range (algebraMap κ' F')) = ⊤)
    (P : Place κ F) (W₁ W₂ : Place κ' F')
    (h₁ : W₁.toValuationSubring.comap (algebraMap F F') = P.toValuationSubring)
    (h₂ : W₂.toValuationSubring.comap (algebraMap F F') = P.toValuationSubring)
    (hc : ∀ x ∈ Subring.closure
        ((algebraMap F F') '' (P.toValuationSubring : Set F) ∪ Set.range (algebraMap κ' F')),
      x ∈ W₁.toValuationSubring.nonunits ↔ x ∈ W₂.toValuationSubring.nonunits) :
    W₁ = W₂

Module documentation

Place eq of comap eq of forall mem nonunits iff

Declarations