Module

exists_pow_eq_of_section_fromNormalization_kummer.lean

Nyll.AlgebraicCurves.Geometry.Schemes.exists_pow_eq_of_section_fromNormalization_kummer

6 declarations indexed from sourceView source ↗

Module documentation

exists pow eq of section from Normalization kummer

Imports14

Mathlib.Algebra.Polynomial.Eval.Defs
Mathlib.Algebra.Polynomial.Monic
Mathlib.AlgebraicGeometry.AffineScheme
Mathlib.AlgebraicGeometry.FunctionField
Mathlib.AlgebraicGeometry.Normalization
Mathlib.AlgebraicGeometry.Scheme
Mathlib.AlgebraicGeometry.Stalk
Mathlib.RingTheory.AdjoinRoot
Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Mathlib.RingTheory.IntegralClosure.IsIntegral.Defs
Mathlib.RingTheory.Localization.FractionRing
Mathlib.Topology.Sheaves.Stalks
Mathlib.Tactic.FieldSimp
Mathlib.Tactic.Ring.RingNF

Imported by3

lemma

map_op_congr

L46 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_pow_eq_of_section_fromNormalization_kummer.SecRoot.map_op_congr

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.exists_pow_eq_of_section_fromNormalization_kummer
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace SecRoot
section thin
variable {Z : Scheme.{u}}

Lean source · statement

lemma map_op_congr {A B : Z.Opens} (i j : B ⟶ A) (s : Γ(Z, A)) :
    Z.presheaf.map i.op s = Z.presheaf.map j.op s

lemma

app_map_top

L50 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_pow_eq_of_section_fromNormalization_kummer.SecRoot.app_map_top

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.exists_pow_eq_of_section_fromNormalization_kummer
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace SecRoot
section thin
variable {Z : Scheme.{u}}

Lean source · statement

lemma app_map_top {Z' : Scheme.{u}} (q : Z' ⟶ Z) (W : Z.Opens) (x : Γ(Z, ⊤)) :
    q.app W (Z.presheaf.map (homOfLE le_top).op x) =
      Z'.presheaf.map (homOfLE le_top).op (q.appTop x)

lemma

comp_app_apply

L58 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_pow_eq_of_section_fromNormalization_kummer.SecRoot.comp_app_apply

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.exists_pow_eq_of_section_fromNormalization_kummer
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace SecRoot
section thin
variable {Z : Scheme.{u}}

Lean source · statement

lemma comp_app_apply {X Y : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) (U : Z.Opens) (x : Γ(Z, U)) :
    (f ≫ g).app U x = f.app (g ⁻¹ᵁ U) (g.app U x)

lemma

root_pow

L63 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_pow_eq_of_section_fromNormalization_kummer.SecRoot.root_pow

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.exists_pow_eq_of_section_fromNormalization_kummer
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace SecRoot

Lean source · statement

lemma root_pow {K : Type*} [CommRing K] (k : ℕ) (g : K) :
    AdjoinRoot.root (Polynomial.X ^ k - Polynomial.C g) ^ k =
      algebraMap K (AdjoinRoot (Polynomial.X ^ k - Polynomial.C g)) g

theorem

exists_pow_eq

L70 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_pow_eq_of_section_fromNormalization_kummer.SecRoot.exists_pow_eq

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.exists_pow_eq_of_section_fromNormalization_kummer
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace SecRoot

Lean source · statement

theorem exists_pow_eq {X : Scheme.{u}} [IsIntegral X] (k : ℕ) (g : X.functionField)
    {X' : Scheme.{u}} (φ : X' ⟶ X) [QuasiCompact φ] [QuasiSeparated φ]
    (s : X ⟶ φ.normalization) (hs : s ≫ φ.fromNormalization = 𝟙 X)
    (V : X.Opens) (hV : IsAffineOpen V) (hηV : genericPoint X ∈ V)
    (θ : AdjoinRoot (Polynomial.X ^ k - Polynomial.C g : Polynomial X.functionField) →+* Γ(X', φ
      ⁻¹ᵁ V))
    (hθ : ∀ c : Γ(X, V), φ.app V c =
      θ (algebraMap X.functionField _ (X.presheaf.germ V (genericPoint X) hηV c))) :
    ∃ f : X.functionField, f ^ k = g

theorem

exists_pow_eq_of_section_fromNormalization_kummer

L164 ↗

AlgebraicGeometry.exists_pow_eq_of_section_fromNormalization_kummer

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.exists_pow_eq_of_section_fromNormalization_kummer
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
open SecRoot in

Lean source · statement

theorem _root_.AlgebraicGeometry.exists_pow_eq_of_section_fromNormalization_kummer
    {X : Scheme.{u}} [IsIntegral X] (k : ℕ) (g : X.functionField) (_hg : g ≠ 0)
    (s : X ⟶ (Spec.map (CommRingCat.ofHom (algebraMap X.functionField
        (AdjoinRoot (Polynomial.X ^ k - Polynomial.C g : Polynomial X.functionField)))) ≫
      X.fromSpecStalk (genericPoint X)).normalization)
    (hs : s ≫ (Spec.map (CommRingCat.ofHom (algebraMap X.functionField
        (AdjoinRoot (Polynomial.X ^ k - Polynomial.C g : Polynomial X.functionField)))) ≫
      X.fromSpecStalk (genericPoint X)).fromNormalization = 𝟙 X) :
    ∃ f : X.functionField, f ^ k = g

Module documentation

exists pow eq of section from Normalization kummer

Declarations

map_op_congr

app_map_top

comp_app_apply

root_pow

exists_pow_eq

exists_pow_eq_of_section_fromNormalization_kummer