NYLL
Module

exists_root_fromNormalization_kummer_existsUnique_lift.lean

Nyll.AlgebraicCurves.Geometry.Schemes.exists_root_fromNormalization_kummer_existsUnique_lift
60 declarations indexed from sourceView source ↗

Module documentation

Kummer roots and unique lifts from normalization

Imports1
Imported by7

Declarations

theorem

genericPoint_mem

L37 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_root_fromNormalization_kummer_existsUnique_lift.KummerLift.genericPoint_mem
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_root_fromNormalization_kummer_existsUnique_lift
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
open _root_.TopologicalSpace
open _root_.Opposite
namespace KummerLift
variable {X : Scheme.{u}} [IsIntegral X]
Lean source · statement
theorem genericPoint_mem (V : X.Opens) [hV : Nonempty V] : genericPoint X ∈ V
theorem

preimage_eq_top

L40 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_root_fromNormalization_kummer_existsUnique_lift.KummerLift.preimage_eq_top
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_root_fromNormalization_kummer_existsUnique_lift
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
open _root_.TopologicalSpace
open _root_.Opposite
namespace KummerLift
variable {X : Scheme.{u}} [IsIntegral X]
Lean source · statement
theorem preimage_eq_top {A : CommRingCat.{u}} (φ : X.functionField ⟶ A) (V : X.Opens) [hV :
  Nonempty V] :
    (Spec.map φ ≫ X.fromSpecStalk (genericPoint X)) ⁻¹ᵁ V = ⊤
theorem

app_eq

L52 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_root_fromNormalization_kummer_existsUnique_lift.KummerLift.app_eq
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_root_fromNormalization_kummer_existsUnique_lift
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
open _root_.TopologicalSpace
open _root_.Opposite
namespace KummerLift
variable {X : Scheme.{u}} [IsIntegral X]
Lean source · statement
theorem app_eq {A : CommRingCat.{u}} (φ : X.functionField ⟶ A) (V : X.Opens) [hV : Nonempty V] :
    (Spec.map φ ≫ X.fromSpecStalk (genericPoint X)).app V =
      X.presheaf.germ V (genericPoint X) (genericPoint_mem V) ≫ φ ≫ (Scheme.ΓSpecIso A).inv ≫
        (Spec A).presheaf.map (homOfLE (le_top :
          (Spec.map φ ≫ X.fromSpecStalk (genericPoint X)) ⁻¹ᵁ V ≤ ⊤)).op
abbrev

KA

L74 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_root_fromNormalization_kummer_existsUnique_lift.KummerLift.KA
Documentation

The algebra obtained by adjoining a root of the Kummer polynomial over the function field.

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_root_fromNormalization_kummer_existsUnique_lift
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
open _root_.TopologicalSpace
open _root_.Opposite
namespace KummerLift
variable {X : Scheme.{u}} [IsIntegral X]
section KummerAlgebra
variable (k : ℕ) (g : X.functionField)
Lean source · statement
abbrev KA : Type u
abbrev

φK

L77 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_root_fromNormalization_kummer_existsUnique_lift.KummerLift.φK
Documentation

The inclusion of the function field into the Kummer root algebra as a ring morphism.

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_root_fromNormalization_kummer_existsUnique_lift
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
open _root_.TopologicalSpace
open _root_.Opposite
namespace KummerLift
variable {X : Scheme.{u}} [IsIntegral X]
section KummerAlgebra
variable (k : ℕ) (g : X.functionField)
Lean source · statement
abbrev φK : X.functionField ⟶ CommRingCat.of (KA k g)
abbrev

fK

L81 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_root_fromNormalization_kummer_existsUnique_lift.KummerLift.fK
Documentation

The morphism from the spectrum of the Kummer root algebra through the generic point.

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_root_fromNormalization_kummer_existsUnique_lift
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
open _root_.TopologicalSpace
open _root_.Opposite
namespace KummerLift
variable {X : Scheme.{u}} [IsIntegral X]
section KummerAlgebra
variable (k : ℕ) (g : X.functionField)
Lean source · statement
abbrev fK : Spec (CommRingCat.of (KA k g)) ⟶ X
def

secIso

L87 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_root_fromNormalization_kummer_existsUnique_lift.KummerLift.secIso
Documentation

The identification of sections over a nonempty inverse-image open with the Kummer root algebra.

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_root_fromNormalization_kummer_existsUnique_lift
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
open _root_.TopologicalSpace
open _root_.Opposite
namespace KummerLift
variable {X : Scheme.{u}} [IsIntegral X]
section KummerAlgebra
variable (k : ℕ) (g : X.functionField)
Lean source · statement
def secIso (V : X.Opens) [Nonempty V] :
    Γ(Spec (CommRingCat.of (KA k g)), (fK k g) ⁻¹ᵁ V) ≅ CommRingCat.of (KA k g)
theorem

secIso_inv

L92 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_root_fromNormalization_kummer_existsUnique_lift.KummerLift.secIso_inv
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_root_fromNormalization_kummer_existsUnique_lift
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
open _root_.TopologicalSpace
open _root_.Opposite
namespace KummerLift
variable {X : Scheme.{u}} [IsIntegral X]
section KummerAlgebra
variable (k : ℕ) (g : X.functionField)
Lean source · statement
theorem secIso_inv (V : X.Opens) [Nonempty V] :
    (secIso k g V).inv = (Scheme.ΓSpecIso (CommRingCat.of (KA k g))).inv ≫
      (Spec (CommRingCat.of (KA k g))).presheaf.map (homOfLE (le_top : (fK k g) ⁻¹ᵁ V ≤ ⊤)).op
theorem

secIso_hom

L98 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_root_fromNormalization_kummer_existsUnique_lift.KummerLift.secIso_hom
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_root_fromNormalization_kummer_existsUnique_lift
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
open _root_.TopologicalSpace
open _root_.Opposite
namespace KummerLift
variable {X : Scheme.{u}} [IsIntegral X]
section KummerAlgebra
variable (k : ℕ) (g : X.functionField)
Lean source · statement
theorem secIso_hom (V : X.Opens) [Nonempty V] :
    (secIso k g V).hom = (Spec (CommRingCat.of (KA k g))).presheaf.map
        (homOfLE (le_of_eq (preimage_eq_top (φK k g) V).symm) : ⊤ ⟶ (fK k g) ⁻¹ᵁ V).op ≫
      (Scheme.ΓSpecIso (CommRingCat.of (KA k g))).hom
theorem

secIso_hom_app

L105 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_root_fromNormalization_kummer_existsUnique_lift.KummerLift.secIso_hom_app
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_root_fromNormalization_kummer_existsUnique_lift
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
open _root_.TopologicalSpace
open _root_.Opposite
namespace KummerLift
variable {X : Scheme.{u}} [IsIntegral X]
section KummerAlgebra
variable (k : ℕ) (g : X.functionField)
Lean source · statement
theorem secIso_hom_app (V : X.Opens) [Nonempty V] (r : Γ(X, V)) :
    (secIso k g V).hom (((fK k g).app V) r) = algebraMap X.functionField (KA k g)
      (X.germToFunctionField V r)
theorem

secIso_hom_res

L119 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_root_fromNormalization_kummer_existsUnique_lift.KummerLift.secIso_hom_res
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_root_fromNormalization_kummer_existsUnique_lift
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
open _root_.TopologicalSpace
open _root_.Opposite
namespace KummerLift
variable {X : Scheme.{u}} [IsIntegral X]
section KummerAlgebra
variable (k : ℕ) (g : X.functionField)
Lean source · statement
theorem secIso_hom_res {V V' : X.Opens} [Nonempty V] [Nonempty V'] (i : (fK k g) ⁻¹ᵁ V' ⟶ (fK k g)
  ⁻¹ᵁ V)
    (z : Γ(Spec (CommRingCat.of (KA k g)), (fK k g) ⁻¹ᵁ V)) :
    (secIso k g V').hom ((Spec (CommRingCat.of (KA k g))).presheaf.map i.op z) = (secIso k g V).hom
      z
def

secAlgEquiv

L137 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_root_fromNormalization_kummer_existsUnique_lift.KummerLift.secAlgEquiv
Documentation

The algebra equivalence identifying sections over the inverse-image open with the Kummer root algebra.

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_root_fromNormalization_kummer_existsUnique_lift
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
open _root_.TopologicalSpace
open _root_.Opposite
namespace KummerLift
variable {X : Scheme.{u}} [IsIntegral X]
section KummerAlgebra
variable (k : ℕ) (g : X.functionField)
Lean source · full declaration
def secAlgEquiv (V : X.Opens) [Nonempty V] :
    letI := ((fK k g).app V).hom.toAlgebra
    Γ(Spec (CommRingCat.of (KA k g)), (fK k g) ⁻¹ᵁ V) ≃ₐ[Γ(X, V)] KA k g :=
  letI := ((fK k g).app V).hom.toAlgebra
  AlgEquiv.ofRingEquiv (f := (secIso k g V).commRingCatIsoToRingEquiv) (fun r => by
    change (secIso k g V).hom (((fK k g).app V) r) = _
    rw [secIso_hom_app, IsScalarTower.algebraMap_apply Γ(X, V) X.functionField (KA k g)]
    rfl)
theorem

secAlgEquiv_apply

L146 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_root_fromNormalization_kummer_existsUnique_lift.KummerLift.secAlgEquiv_apply
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_root_fromNormalization_kummer_existsUnique_lift
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
open _root_.TopologicalSpace
open _root_.Opposite
namespace KummerLift
variable {X : Scheme.{u}} [IsIntegral X]
section KummerAlgebra
variable (k : ℕ) (g : X.functionField)
Lean source · full declaration
theorem secAlgEquiv_apply (V : X.Opens) [Nonempty V] (z : Γ(Spec (CommRingCat.of (KA k g)), (fK k
  g) ⁻¹ᵁ V)) :
    letI := ((fK k g).app V).hom.toAlgebra
    secAlgEquiv k g V z = (secIso k g V).hom z := rfl
theorem

algebraMap_germ

L153 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_root_fromNormalization_kummer_existsUnique_lift.KummerLift.algebraMap_germ
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_root_fromNormalization_kummer_existsUnique_lift
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
open _root_.TopologicalSpace
open _root_.Opposite
namespace KummerLift
variable {X : Scheme.{u}} [IsIntegral X]
Lean source · statement
theorem algebraMap_germ (U : X.Opens) (x : X) (hx : x ∈ U) (s : Γ(X, U)) :
    algebraMap (X.presheaf.stalk x) X.functionField (X.presheaf.germ U x hx s) =
      @Scheme.germToFunctionField X _ U ⟨⟨x, hx⟩⟩ s
def

HasValue

L161 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_root_fromNormalization_kummer_existsUnique_lift.KummerLift.HasValue
Documentation

A section has the specified rational value at every germ on its open domain.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_root_fromNormalization_kummer_existsUnique_lift
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
open _root_.TopologicalSpace
open _root_.Opposite
namespace KummerLift
variable {X : Scheme.{u}} [IsIntegral X]
Lean source · statement
def HasValue (U : X.Opens) (s : Γ(X, U)) (t : X.functionField) : Prop
theorem

hasValue_iff_of_mem

L165 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_root_fromNormalization_kummer_existsUnique_lift.KummerLift.hasValue_iff_of_mem
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_root_fromNormalization_kummer_existsUnique_lift
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
open _root_.TopologicalSpace
open _root_.Opposite
namespace KummerLift
variable {X : Scheme.{u}} [IsIntegral X]
Lean source · statement
theorem hasValue_iff_of_mem (U : X.Opens) (s : Γ(X, U)) (t : X.functionField) (x : X) (hx : x ∈ U) :
    HasValue U s t ↔ @Scheme.germToFunctionField X _ U ⟨⟨x, hx⟩⟩ s = t
theorem

germToFunctionField_eq

L173 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_root_fromNormalization_kummer_existsUnique_lift.KummerLift.HasValue.germToFunctionField_eq
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_root_fromNormalization_kummer_existsUnique_lift
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
open _root_.TopologicalSpace
open _root_.Opposite
namespace KummerLift
variable {X : Scheme.{u}} [IsIntegral X]
Lean source · statement
theorem HasValue.germToFunctionField_eq {U : X.Opens} {s : Γ(X, U)} {t : X.functionField} (h :
  HasValue U s t)
    [hU : Nonempty U] : X.germToFunctionField U s = t
theorem

res

L179 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_root_fromNormalization_kummer_existsUnique_lift.KummerLift.HasValue.res
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_root_fromNormalization_kummer_existsUnique_lift
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
open _root_.TopologicalSpace
open _root_.Opposite
namespace KummerLift
variable {X : Scheme.{u}} [IsIntegral X]
Lean source · statement
theorem HasValue.res {U V : X.Opens} {s : Γ(X, U)} {t : X.functionField} (h : HasValue U s t) (i :
  V ⟶ U) :
    HasValue V (X.presheaf.map i.op s) t
theorem

mul

L186 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_root_fromNormalization_kummer_existsUnique_lift.KummerLift.HasValue.mul
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_root_fromNormalization_kummer_existsUnique_lift
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
open _root_.TopologicalSpace
open _root_.Opposite
namespace KummerLift
variable {X : Scheme.{u}} [IsIntegral X]
Lean source · statement
theorem HasValue.mul {U : X.Opens} {s s' : Γ(X, U)} {t t' : X.functionField} (h : HasValue U s t)
    (h' : HasValue U s' t') : HasValue U (s * s') (t * t')
theorem

pow

L191 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_root_fromNormalization_kummer_existsUnique_lift.KummerLift.HasValue.pow
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_root_fromNormalization_kummer_existsUnique_lift
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
open _root_.TopologicalSpace
open _root_.Opposite
namespace KummerLift
variable {X : Scheme.{u}} [IsIntegral X]
Lean source · statement
theorem HasValue.pow {U : X.Opens} {s : Γ(X, U)} {t : X.functionField} (h : HasValue U s t) (n : ℕ)
  :
    HasValue U (s ^ n) (t ^ n)
theorem

eq

L197 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_root_fromNormalization_kummer_existsUnique_lift.KummerLift.HasValue.eq
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_root_fromNormalization_kummer_existsUnique_lift
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
open _root_.TopologicalSpace
open _root_.Opposite
namespace KummerLift
variable {X : Scheme.{u}} [IsIntegral X]
Lean source · statement
theorem HasValue.eq {U : X.Opens} {s s' : Γ(X, U)} {t : X.functionField} (h : HasValue U s t)
    (h' : HasValue U s' t) : s = s'
theorem

isUnit

L205 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_root_fromNormalization_kummer_existsUnique_lift.KummerLift.HasValue.isUnit
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_root_fromNormalization_kummer_existsUnique_lift
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
open _root_.TopologicalSpace
open _root_.Opposite
namespace KummerLift
variable {X : Scheme.{u}} [IsIntegral X]
Lean source · statement
theorem HasValue.isUnit {U : X.Opens} {s : Γ(X, U)} {t : X.functionField} (h : HasValue U s t) (ht
  : t ≠ 0)
    (hinv : ∀ (x : X), x ∈ U → t⁻¹ ∈ (algebraMap (X.presheaf.stalk x) X.functionField).range) :
      IsUnit s
theorem

exists_hasValue

L218 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_root_fromNormalization_kummer_existsUnique_lift.KummerLift.exists_hasValue
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_root_fromNormalization_kummer_existsUnique_lift
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
open _root_.TopologicalSpace
open _root_.Opposite
namespace KummerLift
variable {X : Scheme.{u}} [IsIntegral X]
Lean source · statement
theorem exists_hasValue (U : X.Opens) (t : X.functionField)
    (ht : ∀ (x : X), x ∈ U → t ∈ (algebraMap (X.presheaf.stalk x) X.functionField).range) :
    ∃ s : Γ(X, U), HasValue U s t
theorem

root_pow

L246 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_root_fromNormalization_kummer_existsUnique_lift.KummerLift.root_pow
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_root_fromNormalization_kummer_existsUnique_lift
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
open _root_.TopologicalSpace
open _root_.Opposite
namespace KummerLift
variable {X : Scheme.{u}} [IsIntegral X]
section Yside
variable (k : ℕ) (g : X.functionField)
Lean source · statement
theorem root_pow : (AdjoinRoot.root (Polynomial.X ^ k - Polynomial.C g : Polynomial
  X.functionField)) ^ k =
    algebraMap X.functionField (KA k g) g
def

yval

L256 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_root_fromNormalization_kummer_existsUnique_lift.KummerLift.yval
Documentation

The homomorphism realizing sections of the normalization as elements of the Kummer root algebra.

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_root_fromNormalization_kummer_existsUnique_lift
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
open _root_.TopologicalSpace
open _root_.Opposite
namespace KummerLift
variable {X : Scheme.{u}} [IsIntegral X]
section Yside
variable (k : ℕ) (g : X.functionField)
Lean source · statement
def yval (V : X.Opens) [Nonempty V] (hV : IsAffineOpen V) :
    Γ((fK k g).normalization, (fK k g).fromNormalization ⁻¹ᵁ V) →+* KA k g
theorem

yval_apply

L263 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_root_fromNormalization_kummer_existsUnique_lift.KummerLift.yval_apply
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_root_fromNormalization_kummer_existsUnique_lift
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
open _root_.TopologicalSpace
open _root_.Opposite
namespace KummerLift
variable {X : Scheme.{u}} [IsIntegral X]
section Yside
variable (k : ℕ) (g : X.functionField)
Lean source · full declaration
theorem yval_apply (V : X.Opens) [Nonempty V] (hV : IsAffineOpen V)
    (s : Γ((fK k g).normalization, (fK k g).fromNormalization ⁻¹ᵁ V)) :
    letI := ((fK k g).app V).hom.toAlgebra
    yval k g V hV s = (secIso k g V).hom (((fK k g).normalizationObjIso hV).hom s).val := rfl
theorem

yval_injective

L268 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_root_fromNormalization_kummer_existsUnique_lift.KummerLift.yval_injective
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_root_fromNormalization_kummer_existsUnique_lift
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
open _root_.TopologicalSpace
open _root_.Opposite
namespace KummerLift
variable {X : Scheme.{u}} [IsIntegral X]
section Yside
variable (k : ℕ) (g : X.functionField)
Lean source · statement
theorem yval_injective (V : X.Opens) [Nonempty V] (hV : IsAffineOpen V) : Function.Injective (yval
  k g V hV)
theorem

preimage_toNormalization

L277 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_root_fromNormalization_kummer_existsUnique_lift.KummerLift.preimage_toNormalization
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_root_fromNormalization_kummer_existsUnique_lift
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
open _root_.TopologicalSpace
open _root_.Opposite
namespace KummerLift
variable {X : Scheme.{u}} [IsIntegral X]
section Yside
variable (k : ℕ) (g : X.functionField)
Lean source · statement
theorem preimage_toNormalization (V : X.Opens) :
    (fK k g).toNormalization ⁻¹ᵁ ((fK k g).fromNormalization ⁻¹ᵁ V) = (fK k g) ⁻¹ᵁ V
theorem

yval_eq_appLE

L281 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_root_fromNormalization_kummer_existsUnique_lift.KummerLift.yval_eq_appLE
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_root_fromNormalization_kummer_existsUnique_lift
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
open _root_.TopologicalSpace
open _root_.Opposite
namespace KummerLift
variable {X : Scheme.{u}} [IsIntegral X]
section Yside
variable (k : ℕ) (g : X.functionField)
Lean source · statement
theorem yval_eq_appLE (V : X.Opens) [Nonempty V] (hV : IsAffineOpen V)
    (s : Γ((fK k g).normalization, (fK k g).fromNormalization ⁻¹ᵁ V)) :
    yval k g V hV s = (secIso k g V).hom ((fK k g).toNormalization.appLE ((fK k
      g).fromNormalization ⁻¹ᵁ V)
      ((fK k g) ⁻¹ᵁ V) (preimage_toNormalization k g V).ge s)
theorem

yval_res

L290 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_root_fromNormalization_kummer_existsUnique_lift.KummerLift.yval_res
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_root_fromNormalization_kummer_existsUnique_lift
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
open _root_.TopologicalSpace
open _root_.Opposite
namespace KummerLift
variable {X : Scheme.{u}} [IsIntegral X]
section Yside
variable (k : ℕ) (g : X.functionField)
Lean source · statement
theorem yval_res {V V' : X.Opens} [Nonempty V] [Nonempty V'] (hV : IsAffineOpen V) (hV' :
  IsAffineOpen V')
    (i : (fK k g).fromNormalization ⁻¹ᵁ V' ⟶ (fK k g).fromNormalization ⁻¹ᵁ V)
    (s : Γ((fK k g).normalization, (fK k g).fromNormalization ⁻¹ᵁ V)) :
    yval k g V' hV' (((fK k g).normalization).presheaf.map i.op s) = yval k g V hV s
theorem

yval_app

L303 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_root_fromNormalization_kummer_existsUnique_lift.KummerLift.yval_app
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_root_fromNormalization_kummer_existsUnique_lift
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
open _root_.TopologicalSpace
open _root_.Opposite
namespace KummerLift
variable {X : Scheme.{u}} [IsIntegral X]
section Yside
variable (k : ℕ) (g : X.functionField)
Lean source · statement
theorem yval_app (V : X.Opens) [Nonempty V] (hV : IsAffineOpen V) (r : Γ(X, V)) :
    yval k g V hV ((fK k g).fromNormalization.app V r) = algebraMap X.functionField (KA k g)
      (X.germToFunctionField V r)
theorem

exists_yval_eq_root

L318 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_root_fromNormalization_kummer_existsUnique_lift.KummerLift.exists_yval_eq_root
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_root_fromNormalization_kummer_existsUnique_lift
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
open _root_.TopologicalSpace
open _root_.Opposite
namespace KummerLift
variable {X : Scheme.{u}} [IsIntegral X]
section Yside
variable (k : ℕ) (g : X.functionField)
Lean source · statement
theorem exists_yval_eq_root (hk : k ≠ 0) (V : X.Opens) [Nonempty V] (hV : IsAffineOpen V) (h :
  X.functionField)
    (uV : Γ(X, V)) (huV : X.germToFunctionField V uV = g / h ^ k) :
    ∃ T : Γ((fK k g).normalization, (fK k g).fromNormalization ⁻¹ᵁ V),
      yval k g V hV T = algebraMap X.functionField (KA k g) h⁻¹ * AdjoinRoot.root _
theorem

map_map

L347 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_root_fromNormalization_kummer_existsUnique_lift.KummerLift.map_map
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_root_fromNormalization_kummer_existsUnique_lift
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
open _root_.TopologicalSpace
open _root_.Opposite
namespace KummerLift
variable {X : Scheme.{u}} [IsIntegral X]
section YGlue
variable (k : ℕ) (g : X.functionField)
Lean source · statement
theorem map_map {Z : Scheme.{u}} {A B C : Z.Opens} (i : B ⟶ A) (j : C ⟶ B) (l : C ⟶ A) (s : Γ(Z,
  A)) :
    Z.presheaf.map j.op (Z.presheaf.map i.op s) = Z.presheaf.map l.op s
def

GoodIdx

L354 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_root_fromNormalization_kummer_existsUnique_lift.KummerLift.GoodIdx
Documentation

The nonempty affine opens contained in a fixed open, used to compare sections locally.

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_root_fromNormalization_kummer_existsUnique_lift
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
open _root_.TopologicalSpace
open _root_.Opposite
namespace KummerLift
variable {X : Scheme.{u}} [IsIntegral X]
section YGlue
variable (k : ℕ) (g : X.functionField)
Lean source · statement
def GoodIdx (W₀ : X.Opens) : Type u
theorem

preimage_le_iSup

L356 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_root_fromNormalization_kummer_existsUnique_lift.KummerLift.preimage_le_iSup
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_root_fromNormalization_kummer_existsUnique_lift
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
open _root_.TopologicalSpace
open _root_.Opposite
namespace KummerLift
variable {X : Scheme.{u}} [IsIntegral X]
section YGlue
variable (k : ℕ) (g : X.functionField)
Lean source · statement
theorem preimage_le_iSup (W₀ : X.Opens) :
    (fK k g).fromNormalization ⁻¹ᵁ W₀ ≤ ⨆ i : GoodIdx W₀, (fK k g).fromNormalization ⁻¹ᵁ i.1
def

HasYVal

L365 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_root_fromNormalization_kummer_existsUnique_lift.KummerLift.HasYVal
Documentation

A section of the normalization has the specified value on every nonempty affine subopen.

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_root_fromNormalization_kummer_existsUnique_lift
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
open _root_.TopologicalSpace
open _root_.Opposite
namespace KummerLift
variable {X : Scheme.{u}} [IsIntegral X]
section YGlue
variable (k : ℕ) (g : X.functionField)
Lean source · statement
def HasYVal (W₀ : X.Opens) (s : Γ((fK k g).normalization, (fK k g).fromNormalization ⁻¹ᵁ W₀)) (t :
  KA k g) : Prop
theorem

hasYVal_of_yval_eq

L373 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_root_fromNormalization_kummer_existsUnique_lift.KummerLift.hasYVal_of_yval_eq
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_root_fromNormalization_kummer_existsUnique_lift
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
open _root_.TopologicalSpace
open _root_.Opposite
namespace KummerLift
variable {X : Scheme.{u}} [IsIntegral X]
section YGlue
variable (k : ℕ) (g : X.functionField)
variable {k g}
Lean source · statement
theorem hasYVal_of_yval_eq {V₀ : X.Opens} [Nonempty V₀] (hV₀ : IsAffineOpen V₀)
    {T : Γ((fK k g).normalization, (fK k g).fromNormalization ⁻¹ᵁ V₀)} {t : KA k g} (hT : yval k g
      V₀ hV₀ T = t) :
    HasYVal k g V₀ T t
theorem

res

L381 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_root_fromNormalization_kummer_existsUnique_lift.KummerLift.HasYVal.res
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_root_fromNormalization_kummer_existsUnique_lift
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
open _root_.TopologicalSpace
open _root_.Opposite
namespace KummerLift
variable {X : Scheme.{u}} [IsIntegral X]
section YGlue
variable (k : ℕ) (g : X.functionField)
variable {k g}
Lean source · statement
theorem HasYVal.res {W₀ W₁ : X.Opens} {s : Γ((fK k g).normalization, (fK k g).fromNormalization ⁻¹ᵁ
  W₀)} {t : KA k g}
    (h : HasYVal k g W₀ s t) (hW : W₁ ≤ W₀) :
    HasYVal k g W₁ (((fK k g).normalization).presheaf.map (homOfLE ((fK k
      g).fromNormalization.preimage_mono hW)).op s) t
theorem

mul

L390 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_root_fromNormalization_kummer_existsUnique_lift.KummerLift.HasYVal.mul
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_root_fromNormalization_kummer_existsUnique_lift
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
open _root_.TopologicalSpace
open _root_.Opposite
namespace KummerLift
variable {X : Scheme.{u}} [IsIntegral X]
section YGlue
variable (k : ℕ) (g : X.functionField)
variable {k g}
Lean source · statement
theorem HasYVal.mul {W₀ : X.Opens} {s s' : Γ((fK k g).normalization, (fK k g).fromNormalization ⁻¹ᵁ
  W₀)} {t t' : KA k g}
    (h : HasYVal k g W₀ s t) (h' : HasYVal k g W₀ s' t') : HasYVal k g W₀ (s * s') (t * t')
theorem

pow

L396 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_root_fromNormalization_kummer_existsUnique_lift.KummerLift.HasYVal.pow
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_root_fromNormalization_kummer_existsUnique_lift
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
open _root_.TopologicalSpace
open _root_.Opposite
namespace KummerLift
variable {X : Scheme.{u}} [IsIntegral X]
section YGlue
variable (k : ℕ) (g : X.functionField)
variable {k g}
Lean source · statement
theorem HasYVal.pow {W₀ : X.Opens} {s : Γ((fK k g).normalization, (fK k g).fromNormalization ⁻¹ᵁ
  W₀)} {t : KA k g}
    (h : HasYVal k g W₀ s t) (n : ℕ) : HasYVal k g W₀ (s ^ n) (t ^ n)
theorem

eq

L402 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_root_fromNormalization_kummer_existsUnique_lift.KummerLift.HasYVal.eq
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_root_fromNormalization_kummer_existsUnique_lift
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
open _root_.TopologicalSpace
open _root_.Opposite
namespace KummerLift
variable {X : Scheme.{u}} [IsIntegral X]
section YGlue
variable (k : ℕ) (g : X.functionField)
variable {k g}
Lean source · statement
theorem HasYVal.eq {W₀ : X.Opens} {s s' : Γ((fK k g).normalization, (fK k g).fromNormalization ⁻¹ᵁ
  W₀)} {t : KA k g}
    (h : HasYVal k g W₀ s t) (h' : HasYVal k g W₀ s' t) : s = s'
theorem

hasYVal_app

L413 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_root_fromNormalization_kummer_existsUnique_lift.KummerLift.hasYVal_app
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_root_fromNormalization_kummer_existsUnique_lift
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
open _root_.TopologicalSpace
open _root_.Opposite
namespace KummerLift
variable {X : Scheme.{u}} [IsIntegral X]
section YGlue
variable (k : ℕ) (g : X.functionField)
variable {k g}
Lean source · statement
theorem hasYVal_app {W₀ : X.Opens} {u : Γ(X, W₀)} {t : X.functionField} (hu : HasValue W₀ u t) :
    HasYVal k g W₀ ((fK k g).fromNormalization.app W₀ u) (algebraMap X.functionField (KA k g) t)
theorem

exists_hasYVal_root

L425 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_root_fromNormalization_kummer_existsUnique_lift.KummerLift.exists_hasYVal_root
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_root_fromNormalization_kummer_existsUnique_lift
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
open _root_.TopologicalSpace
open _root_.Opposite
namespace KummerLift
variable {X : Scheme.{u}} [IsIntegral X]
section YGlue
variable (k : ℕ) (g : X.functionField)
variable {k g}
Lean source · statement
theorem exists_hasYVal_root (hk : k ≠ 0) (W₀ : X.Opens) (h : X.functionField) (u : Γ(X, W₀))
    (hu : HasValue W₀ u (g / h ^ k)) :
    ∃ T : Γ((fK k g).normalization, (fK k g).fromNormalization ⁻¹ᵁ W₀),
      HasYVal k g W₀ T (algebraMap X.functionField (KA k g) h⁻¹ * AdjoinRoot.root _)
theorem

root_div_pow

L462 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_root_fromNormalization_kummer_existsUnique_lift.KummerLift.root_div_pow
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_root_fromNormalization_kummer_existsUnique_lift
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
open _root_.TopologicalSpace
open _root_.Opposite
namespace KummerLift
variable {X : Scheme.{u}} [IsIntegral X]
section Data
variable (k : ℕ) (g : X.functionField)
Lean source · statement
theorem root_div_pow (h : X.functionField) :
    (algebraMap X.functionField (KA k g) h⁻¹ * AdjoinRoot.root _) ^ k = algebraMap X.functionField
      (KA k g) (g / h ^ k)
theorem

mem_range_div

L469 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_root_fromNormalization_kummer_existsUnique_lift.KummerLift.mem_range_div
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_root_fromNormalization_kummer_existsUnique_lift
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
open _root_.TopologicalSpace
open _root_.Opposite
namespace KummerLift
variable {X : Scheme.{u}} [IsIntegral X]
section Data
variable (k : ℕ) (g : X.functionField)
variable {k g}
Lean source · statement
theorem mem_range_div (hnorm : ∀ x : X, IsIntegrallyClosed (X.presheaf.stalk x)) (hk0 : k ≠ 0) (hg
  : g ≠ 0)
    {ha hb : X.functionField} (x : X)
    (h1 : g / ha ^ k ∈ (algebraMap (X.presheaf.stalk x) X.functionField).range)
    (h2 : hb ^ k / g ∈ (algebraMap (X.presheaf.stalk x) X.functionField).range) :
    hb / ha ∈ (algebraMap (X.presheaf.stalk x) X.functionField).range
theorem

exists_data

L485 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_root_fromNormalization_kummer_existsUnique_lift.KummerLift.exists_data
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_root_fromNormalization_kummer_existsUnique_lift
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
open _root_.TopologicalSpace
open _root_.Opposite
namespace KummerLift
variable {X : Scheme.{u}} [IsIntegral X]
section Data
variable (k : ℕ) (g : X.functionField)
variable {k g}
Lean source · statement
theorem exists_data (hnorm : ∀ x : X, IsIntegrallyClosed (X.presheaf.stalk x)) (hk0 : k ≠ 0) (hg :
  g ≠ 0)
    (r : ℕ) (U : Fin r → X.Opens) (h : Fin r → X.functionField) (hh : ∀ a, h a ≠ 0)
    (hdiv : ∀ a (x : X), x ∈ U a →
      g / h a ^ k ∈ (algebraMap (X.presheaf.stalk x) X.functionField).range ∧
      h a ^ k / g ∈ (algebraMap (X.presheaf.stalk x) X.functionField).range) :
    ∃ (u : ∀ a, Γ(X, U a)) (T : ∀ a, Γ((fK k g).normalization, (fK k g).fromNormalization ⁻¹ᵁ (U
      a))),
      (∀ a, HasValue (U a) (u a) (g / h a ^ k)) ∧
      (∀ a, IsUnit (u a)) ∧
      (∀ a, HasYVal k g (U a) (T a) (algebraMap X.functionField (KA k g) (h a)⁻¹ * AdjoinRoot.root
        _)) ∧
      (∀ a, T a ^ k = (fK k g).fromNormalization.app (U a) (u a)) ∧
      (∀ a b, ∃ w : Γ(X, U a ⊓ U b), HasValue (U a ⊓ U b) w (h b / h a) ∧
        X.presheaf.map (homOfLE inf_le_left).op (u a) = w ^ k * X.presheaf.map (homOfLE
          inf_le_right).op (u b) ∧
        ((fK k g).normalization).presheaf.map (homOfLE ((fK k g).fromNormalization.preimage_mono
          inf_le_left)).op (T a) =
          (fK k g).fromNormalization.app (U a ⊓ U b) w *
          ((fK k g).normalization).presheaf.map (homOfLE ((fK k g).fromNormalization.preimage_mono
            inf_le_right)).op (T b))
theorem

map_injective_of_eq

L547 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_root_fromNormalization_kummer_existsUnique_lift.KummerLift.map_injective_of_eq
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_root_fromNormalization_kummer_existsUnique_lift
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
open _root_.TopologicalSpace
open _root_.Opposite
namespace KummerLift
variable {X : Scheme.{u}} [IsIntegral X]
section Lift
variable (k : ℕ) (g : X.functionField)
omit [IsIntegral X] in
Lean source · statement
theorem map_injective_of_eq {Z : Scheme.{u}} {A B : Z.Opens} (e : A = B) (i : A ⟶ B) :
    Function.Injective (Z.presheaf.map i.op)
theorem

app_map

L553 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_root_fromNormalization_kummer_existsUnique_lift.KummerLift.app_map
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_root_fromNormalization_kummer_existsUnique_lift
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
open _root_.TopologicalSpace
open _root_.Opposite
namespace KummerLift
variable {X : Scheme.{u}} [IsIntegral X]
section Lift
variable (k : ℕ) (g : X.functionField)
omit [IsIntegral X] in
Lean source · statement
theorem app_map {Z Z' : Scheme.{u}} (q : Z' ⟶ Z) {A B : Z.Opens} (i : B ⟶ A) (j : q ⁻¹ᵁ B ⟶ q ⁻¹ᵁ A)
    (x : Γ(Z, A)) : q.app B (Z.presheaf.map i.op x) = Z'.presheaf.map j.op (q.app A x)
def

RootHyp

L562 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_root_fromNormalization_kummer_existsUnique_lift.KummerLift.RootHyp
Documentation

The equation saying that the chosen global section is a root of the pulled-back section.

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_root_fromNormalization_kummer_existsUnique_lift
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
open _root_.TopologicalSpace
open _root_.Opposite
namespace KummerLift
variable {X : Scheme.{u}} [IsIntegral X]
section Lift
variable (k : ℕ) (g : X.functionField)
Lean source · statement
def RootHyp (W : X.Opens) (uW : Γ(X, W)) (Z : Scheme.{u}) (z : Z ⟶ X) (τ : Γ(Z, ⊤)) : Prop
def

LiftProp

L569 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_root_fromNormalization_kummer_existsUnique_lift.KummerLift.LiftProp
Documentation

A lift to the normalization lies over the given morphism and pulls the distinguished section to the chosen root.

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_root_fromNormalization_kummer_existsUnique_lift
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
open _root_.TopologicalSpace
open _root_.Opposite
namespace KummerLift
variable {X : Scheme.{u}} [IsIntegral X]
section Lift
variable (k : ℕ) (g : X.functionField)
Lean source · statement
def LiftProp (W : X.Opens) (TW : Γ((fK k g).normalization, (fK k g).fromNormalization ⁻¹ᵁ W))
    (Z : Scheme.{u}) (z : Z ⟶ X) (τ : Γ(Z, ⊤)) (s : Z ⟶ (fK k g).normalization) : Prop
def

HasLift

L578 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_root_fromNormalization_kummer_existsUnique_lift.KummerLift.HasLift
Documentation

The universal property asserting existence and uniqueness of a lift carrying the distinguished section to each root.

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_root_fromNormalization_kummer_existsUnique_lift
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
open _root_.TopologicalSpace
open _root_.Opposite
namespace KummerLift
variable {X : Scheme.{u}} [IsIntegral X]
section Lift
variable (k : ℕ) (g : X.functionField)
Lean source · statement
def HasLift (W : X.Opens) (uW : Γ(X, W)) (TW : Γ((fK k g).normalization, (fK k g).fromNormalization
  ⁻¹ᵁ W)) : Prop
theorem

rootHyp_comp

L586 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_root_fromNormalization_kummer_existsUnique_lift.KummerLift.rootHyp_comp
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_root_fromNormalization_kummer_existsUnique_lift
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
open _root_.TopologicalSpace
open _root_.Opposite
namespace KummerLift
variable {X : Scheme.{u}} [IsIntegral X]
section Lift
variable (k : ℕ) (g : X.functionField)
variable {k g}
omit [IsIntegral X] in
Lean source · statement
theorem rootHyp_comp {W : X.Opens} {uW : Γ(X, W)} {Z Z' : Scheme.{u}} (q : Z' ⟶ Z) {z : Z ⟶ X} {τ :
  Γ(Z, ⊤)}
    (h : RootHyp k W uW Z z τ) : RootHyp k W uW Z' (q ≫ z) (q.appTop τ)
theorem

liftProp_comp

L597 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_root_fromNormalization_kummer_existsUnique_lift.KummerLift.liftProp_comp
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_root_fromNormalization_kummer_existsUnique_lift
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
open _root_.TopologicalSpace
open _root_.Opposite
namespace KummerLift
variable {X : Scheme.{u}} [IsIntegral X]
section Lift
variable (k : ℕ) (g : X.functionField)
variable {k g}
Lean source · statement
theorem liftProp_comp {W : X.Opens} {TW : Γ((fK k g).normalization, (fK k g).fromNormalization ⁻¹ᵁ
  W)}
    {Z Z' : Scheme.{u}} (q : Z' ⟶ Z) {z : Z ⟶ X} {τ : Γ(Z, ⊤)} {s : Z ⟶ (fK k g).normalization}
    (h : LiftProp k g W TW Z z τ s) : LiftProp k g W TW Z' (q ≫ z) (q.appTop τ) (q ≫ s)
theorem

rootHyp_res

L607 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_root_fromNormalization_kummer_existsUnique_lift.KummerLift.rootHyp_res
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_root_fromNormalization_kummer_existsUnique_lift
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
open _root_.TopologicalSpace
open _root_.Opposite
namespace KummerLift
variable {X : Scheme.{u}} [IsIntegral X]
section Lift
variable (k : ℕ) (g : X.functionField)
variable {k g}
omit [IsIntegral X] in
Lean source · statement
theorem rootHyp_res {W W' : X.Opens} (hle : W' ≤ W) {uW : Γ(X, W)} {Z : Scheme.{u}} {z : Z ⟶ X} {τ
  : Γ(Z, ⊤)}
    (h : RootHyp k W uW Z z τ) : RootHyp k W' (X.presheaf.map (homOfLE hle).op uW) Z z τ
theorem

app_res_iff

L614 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_root_fromNormalization_kummer_existsUnique_lift.KummerLift.app_res_iff
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_root_fromNormalization_kummer_existsUnique_lift
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
open _root_.TopologicalSpace
open _root_.Opposite
namespace KummerLift
variable {X : Scheme.{u}} [IsIntegral X]
section Lift
variable (k : ℕ) (g : X.functionField)
variable {k g}
Lean source · statement
theorem app_res_iff {W W' : X.Opens} (hle : W' ≤ W) {TW : Γ((fK k g).normalization, (fK k
  g).fromNormalization ⁻¹ᵁ W)}
    {Z : Scheme.{u}} {z : Z ⟶ X} (hz : z ⁻¹ᵁ W' = ⊤) {τ : Γ(Z, ⊤)} {s : Z ⟶ (fK k g).normalization}
    (hs : s ≫ (fK k g).fromNormalization = z) :
    s.app ((fK k g).fromNormalization ⁻¹ᵁ W) TW = Z.presheaf.map (homOfLE le_top).op τ ↔
      s.app ((fK k g).fromNormalization ⁻¹ᵁ W')
        (((fK k g).normalization).presheaf.map (homOfLE ((fK k g).fromNormalization.preimage_mono
          hle)).op TW) =
        Z.presheaf.map (homOfLE le_top).op τ
theorem

isOpenCover_preimage

L637 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_root_fromNormalization_kummer_existsUnique_lift.KummerLift.isOpenCover_preimage
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_root_fromNormalization_kummer_existsUnique_lift
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
open _root_.TopologicalSpace
open _root_.Opposite
namespace KummerLift
variable {X : Scheme.{u}} [IsIntegral X]
section Lift
variable (k : ℕ) (g : X.functionField)
variable {k g}
omit [IsIntegral X] in
Lean source · full declaration
theorem isOpenCover_preimage (W₀ : X.Opens) {Z : Scheme.{u}} (z : Z ⟶ X) (hz : z ⁻¹ᵁ W₀ = ⊤) :
    IsOpenCover (fun i : GoodIdx W₀ => z ⁻¹ᵁ i.1) := by
  apply IsOpenCover.mk
  apply top_le_iff.mp
  rw [← hz]
  intro y hy
  have hy' : z y ∈ (W₀ : Set X) := hy
  obtain ⟨_, ⟨V, hVaff, rfl⟩, hyV, hVle⟩ := X.isBasis_affineOpens.exists_subset_of_mem_open hy'
    W₀.isOpen
  exact Opens.mem_iSup.mpr ⟨⟨V, hVaff, ⟨⟨_, hyV⟩⟩, hVle⟩, hyV⟩
theorem

lift_unique

L648 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_root_fromNormalization_kummer_existsUnique_lift.KummerLift.lift_unique
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_root_fromNormalization_kummer_existsUnique_lift
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
open _root_.TopologicalSpace
open _root_.Opposite
namespace KummerLift
variable {X : Scheme.{u}} [IsIntegral X]
section Lift
variable (k : ℕ) (g : X.functionField)
variable {k g}
Lean source · statement
theorem lift_unique {W₀ : X.Opens} {u₀ : Γ(X, W₀)}
    {T₀ : Γ((fK k g).normalization, (fK k g).fromNormalization ⁻¹ᵁ W₀)}
    (hloc : ∀ i : GoodIdx W₀, HasLift k g i.1 (X.presheaf.map (homOfLE i.2.2.2).op u₀)
      (((fK k g).normalization).presheaf.map (homOfLE ((fK k g).fromNormalization.preimage_mono
        i.2.2.2)).op T₀))
    {Z : Scheme.{u}} {z : Z ⟶ X} (hz : z ⁻¹ᵁ W₀ = ⊤) {τ : Γ(Z, ⊤)} (hτ : RootHyp k W₀ u₀ Z z τ)
    {s₁ s₂ : Z ⟶ (fK k g).normalization} (h₁ : LiftProp k g W₀ T₀ Z z τ s₁) (h₂ : LiftProp k g W₀
      T₀ Z z τ s₂) :
    s₁ = s₂
theorem

hasLift_of_forall

L672 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_root_fromNormalization_kummer_existsUnique_lift.KummerLift.hasLift_of_forall
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_root_fromNormalization_kummer_existsUnique_lift
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
open _root_.TopologicalSpace
open _root_.Opposite
namespace KummerLift
variable {X : Scheme.{u}} [IsIntegral X]
section Lift
variable (k : ℕ) (g : X.functionField)
variable {k g}
Lean source · statement
theorem hasLift_of_forall {W₀ : X.Opens} {u₀ : Γ(X, W₀)}
    {T₀ : Γ((fK k g).normalization, (fK k g).fromNormalization ⁻¹ᵁ W₀)}
    (hloc : ∀ i : GoodIdx W₀, HasLift k g i.1 (X.presheaf.map (homOfLE i.2.2.2).op u₀)
      (((fK k g).normalization).presheaf.map (homOfLE ((fK k g).fromNormalization.preimage_mono
        i.2.2.2)).op T₀)) :
    HasLift k g W₀ u₀ T₀
theorem

toNormalization_app_eq

L737 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_root_fromNormalization_kummer_existsUnique_lift.KummerLift.toNormalization_app_eq
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_root_fromNormalization_kummer_existsUnique_lift
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
open _root_.TopologicalSpace
open _root_.Opposite
namespace KummerLift
variable {X : Scheme.{u}} [IsIntegral X]
section Bridge
variable (k : ℕ) (g : X.functionField)
Lean source · statement
theorem toNormalization_app_eq (V : X.Opens) [Nonempty V] (hV : IsAffineOpen V)
    (T : Γ((fK k g).normalization, (fK k g).fromNormalization ⁻¹ᵁ V)) (ρ : KA k g) (hT : yval k g V
      hV T = ρ) :
    (fK k g).toNormalization.app ((fK k g).fromNormalization ⁻¹ᵁ V) T =
      (Spec (CommRingCat.of (KA k g))).presheaf.map (homOfLE le_top).op
        ((Scheme.ΓSpecIso (CommRingCat.of (KA k g))).inv ρ)
theorem

exists_root_fromNormalization_kummer_existsUnique_lift

L761 ↗
AlgebraicGeometry.exists_root_fromNormalization_kummer_existsUnique_lift
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_root_fromNormalization_kummer_existsUnique_lift
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Polynomial
open _root_.TopologicalSpace
open _root_.Opposite
open KummerLift in
Lean source · full declaration
theorem _root_.AlgebraicGeometry.exists_root_fromNormalization_kummer_existsUnique_lift
    {R : Type u} [CommRing R]
    {X : Scheme.{u}} [IsIntegral X] (f : X ⟶ Spec (CommRingCat.of R))
    (hnorm : ∀ x : X, IsIntegrallyClosed (X.presheaf.stalk x))
    (k : ℕ) (hk : IsUnit ((k : ℕ) : R))
    (g : X.functionField) (hg : g ≠ 0)
    (r : ℕ) (U : Fin r → X.Opens) (hU : (⨆ a, U a) = ⊤) (h : Fin r → X.functionField) (hh : ∀ a, h
      a ≠ 0)
    (hdiv : ∀ a (x : X), x ∈ U a →
      g / h a ^ k ∈ (algebraMap (X.presheaf.stalk x) X.functionField).range ∧
      h a ^ k / g ∈ (algebraMap (X.presheaf.stalk x) X.functionField).range) :
    let π := (Spec.map (CommRingCat.ofHom (algebraMap X.functionField (AdjoinRoot (Polynomial.X ^ k
      - Polynomial.C g : Polynomial X.functionField)))) ≫
      X.fromSpecStalk (genericPoint X)).fromNormalization
    let Y := (Spec.map (CommRingCat.ofHom (algebraMap X.functionField (AdjoinRoot (Polynomial.X ^ k
      - Polynomial.C g : Polynomial X.functionField)))) ≫
      X.fromSpecStalk (genericPoint X)).normalization
    ∃ (u : ∀ a, Γ(X, U a)) (T : ∀ a, Γ(Y, π ⁻¹ᵁ (U a))),
      (∀ a (x : X) (hx : x ∈ U a),
        algebraMap (X.presheaf.stalk x) X.functionField (X.presheaf.germ (U a) x hx (u a)) = g / h
          a ^ k) ∧
      (∀ a, IsUnit (u a)) ∧
      (∀ a, T a ^ k = π.app (U a) (u a)) ∧
      (∀ a b, ∃ w : Γ(X, U a ⊓ U b),
        (∀ (x : X) (hx : x ∈ U a ⊓ U b),
          algebraMap (X.presheaf.stalk x) X.functionField (X.presheaf.germ (U a ⊓ U b) x hx w) = h
            b / h a) ∧
        X.presheaf.map (homOfLE inf_le_left).op (u a) = w ^ k * X.presheaf.map (homOfLE
          inf_le_right).op (u b) ∧
        Y.presheaf.map (homOfLE (π.preimage_mono inf_le_left)).op (T a) =
          π.app (U a ⊓ U b) w * Y.presheaf.map (homOfLE (π.preimage_mono inf_le_right)).op (T b)) ∧
      (∀ a (Z : Scheme.{u}) (z : Z ⟶ X), z ⁻¹ᵁ (U a) = ⊤ →
        ∀ τ : Γ(Z, ⊤), Z.presheaf.map (homOfLE le_top).op τ ^ k = z.app (U a) (u a) →
          ∃! s : Z ⟶ Y, s ≫ π = z ∧ s.app (π ⁻¹ᵁ (U a)) (T a) = Z.presheaf.map (homOfLE le_top).op
            τ) := by
  intro π Y
  change ∃ (u : ∀ a, Γ(X, U a)) (T : ∀ a, Γ((fK k g).normalization, (fK k g).fromNormalization ⁻¹ᵁ
    (U a))),
      (∀ a (x : X) (hx : x ∈ U a),
        algebraMap (X.presheaf.stalk x) X.functionField (X.presheaf.germ (U a) x hx (u a)) = g / h
          a ^ k) ∧
      (∀ a, IsUnit (u a)) ∧
      (∀ a, T a ^ k = (fK k g).fromNormalization.app (U a) (u a)) ∧
      (∀ a b, ∃ w : Γ(X, U a ⊓ U b),
        (∀ (x : X) (hx : x ∈ U a ⊓ U b),
          algebraMap (X.presheaf.stalk x) X.functionField (X.presheaf.germ (U a ⊓ U b) x hx w) = h
            b / h a) ∧
        X.presheaf.map (homOfLE inf_le_left).op (u a) = w ^ k * X.presheaf.map (homOfLE
          inf_le_right).op (u b) ∧
        ((fK k g).normalization).presheaf.map (homOfLE ((fK k g).fromNormalization.preimage_mono
          inf_le_left)).op (T a) =
          (fK k g).fromNormalization.app (U a ⊓ U b) w *
          ((fK k g).normalization).presheaf.map (homOfLE ((fK k g).fromNormalization.preimage_mono
            inf_le_right)).op (T b)) ∧
      (∀ a (Z : Scheme.{u}) (z : Z ⟶ X), z ⁻¹ᵁ (U a) = ⊤ →
        ∀ τ : Γ(Z, ⊤), Z.presheaf.map (homOfLE le_top).op τ ^ k = z.app (U a) (u a) →
          ∃! s : Z ⟶ (fK k g).normalization, s ≫ (fK k g).fromNormalization = z ∧
            s.app ((fK k g).fromNormalization ⁻¹ᵁ (U a)) (T a) = Z.presheaf.map (homOfLE le_top).op
              τ)
  have hkX : ∀ V : X.Opens, IsUnit ((k : ℕ) : Γ(X, V)) := fun V => by
    have := hk.map ((Scheme.ΓSpecIso (CommRingCat.of R)).inv ≫ f.appLE ⊤ V le_top).hom
    rwa [map_natCast] at this
  have hk0 : k ≠ 0 := by
    rintro rfl
    have h1 := hkX (⨆ a, U a)
    rw [hU, Nat.cast_zero, isUnit_zero_iff] at h1
    exact zero_ne_one h1
  obtain ⟨u, T, hrest⟩ := exists_data (k := k) (g := g) hnorm hk0 hg r U h hh hdiv
  refine ⟨u, T, fun a x hx => hrest.1 a x hx, hrest.2.1, hrest.2.2.2.1, fun a b => ?_, fun a => ?_⟩
  · exact (hrest.2.2.2.2 a b).elim fun w hw => ⟨w, hw.1, hw.2.1, hw.2.2⟩
  · have hu : HasValue (U a) (u a) (g / h a ^ k) := hrest.1 a
    have huunit : IsUnit (u a) := hrest.2.1 a
    have hT : HasYVal k g (U a) (T a) (algebraMap X.functionField (KA k g) (h a)⁻¹ *
      AdjoinRoot.root _) :=
      hrest.2.2.1 a
    have hL : HasLift k g (U a) (u a) (T a) := by
      apply hasLift_of_forall
      intro i
      have := i.2.2.1
      have hchar := toNormalization_app_eq k g i.1 i.2.1 _ _ (hT i.1 i.2.1 i.2.2.1 i.2.2.2)
      have hmain := AlgebraicGeometry.existsUnique_lift_fromNormalization_kummer_of_isAffineOpen
        hnorm k g i.1 i.2.1
        i.2.2.1 (hkX i.1) (X.presheaf.map (homOfLE i.2.2.2).op (u a)) (huunit.map _) (h a) (hh a)
        (hu.res (homOfLE i.2.2.2)) _ hchar
      intro Z z hz τ hτ
      exact hmain Z z hz τ hτ
    intro Z z hz τ hτ
    exact hL Z z hz τ hτ

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