NYLL
Module

CurveModel_exists_iso_of_twoAffineLineCover.lean

Nyll.AlgebraicCurves.Models.CurveModel_exists_iso_of_twoAffineLineCover
7 declarations indexed from sourceView source ↗

Module documentation

Curve Model exists iso of two Affine Line Cover

Imports3
Imported by1

Declarations

instance

factX

L40 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_iso_of_twoAffineLineCover.E86P1.factX
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_iso_of_twoAffineLineCover
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
open _root_.Polynomial
namespace E86P1
variable (κ : Type u) [Field κ]
local notation "RF" => RatFunc κ
local notation "XX" => (RatFunc.X : RatFunc κ)
Lean source · statement
instance factX : Fact ((RatFunc.X : RatFunc κ) ≠ 0)
theorem

exists_algEquiv_chartRing_X

L42 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_iso_of_twoAffineLineCover.E86P1.exists_algEquiv_chartRing_X
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_iso_of_twoAffineLineCover
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
open _root_.Polynomial
namespace E86P1
variable (κ : Type u) [Field κ]
local notation "RF" => RatFunc κ
local notation "XX" => (RatFunc.X : RatFunc κ)
Lean source · statement
theorem exists_algEquiv_chartRing_X :
    ∃ α : Polynomial κ ≃ₐ[κ] CurveModel.chartRing κ ({XX} : Set RF), (α Polynomial.X : RF) = XX
theorem

map_chartRing_le

L82 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_iso_of_twoAffineLineCover.E86P1.map_chartRing_le
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_iso_of_twoAffineLineCover
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
open _root_.Polynomial
namespace E86P1
variable (κ : Type u) [Field κ]
local notation "RF" => RatFunc κ
local notation "XX" => (RatFunc.X : RatFunc κ)
Lean source · statement
theorem map_chartRing_le {K : Type u} [Field K] {L L' : Type u} [Field L] [Field L'] [Algebra K L]
  [Algebra K L']
    (φ : L →ₐ[K] L') (S : Set L) :
    (CurveModel.chartRing K S).map φ ≤ CurveModel.chartRing K (φ '' S)
theorem

exists_algEquiv_ratFunc_inv

L98 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_iso_of_twoAffineLineCover.E86P1.exists_algEquiv_ratFunc_inv
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_iso_of_twoAffineLineCover
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
open _root_.Polynomial
namespace E86P1
variable (κ : Type u) [Field κ]
local notation "RF" => RatFunc κ
local notation "XX" => (RatFunc.X : RatFunc κ)
Lean source · statement
theorem exists_algEquiv_ratFunc_inv : ∃ σ : RF ≃ₐ[κ] RF, σ XX = XX⁻¹ ∧ σ XX⁻¹ = XX
theorem

exists_algEquiv_chartRing_Xinv

L128 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_iso_of_twoAffineLineCover.E86P1.exists_algEquiv_chartRing_Xinv
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_iso_of_twoAffineLineCover
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
open _root_.Polynomial
namespace E86P1
variable (κ : Type u) [Field κ]
local notation "RF" => RatFunc κ
local notation "XX" => (RatFunc.X : RatFunc κ)
Lean source · statement
theorem exists_algEquiv_chartRing_Xinv :
    ∃ α : Polynomial κ ≃ₐ[κ] CurveModel.chartRing κ ({XX⁻¹} : Set RF), (α Polynomial.X : RF) = XX⁻¹
theorem

exists_ringEquiv_overlap

L151 ↗
AlgebraicCurves.Models.Proofs.CurveModel_exists_iso_of_twoAffineLineCover.E86P1.exists_ringEquiv_overlap
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_iso_of_twoAffineLineCover
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
open _root_.Polynomial
namespace E86P1
variable (κ : Type u) [Field κ]
local notation "RF" => RatFunc κ
local notation "XX" => (RatFunc.X : RatFunc κ)
Lean source · statement
theorem exists_ringEquiv_overlap (α₀ : Polynomial κ ≃ₐ[κ] CurveModel.chartRing κ ({XX} : Set RF))
    (hα₀ : (α₀ Polynomial.X : RF) = XX)
    (α₁ : Polynomial κ ≃ₐ[κ] CurveModel.chartRing κ ({XX⁻¹} : Set RF)) (hα₁ : (α₁ Polynomial.X :
      RF) = XX⁻¹) :
    ∃ β : Localization.Away (X : Polynomial κ) ≃+* CurveModel.chartRing κ ({XX, XX⁻¹} : Set RF),
      (β.toRingHom.comp (algebraMap (Polynomial κ) (Localization.Away (X : Polynomial κ))) =
        (CurveModel.incl₀ κ XX).toRingHom.comp α₀.toRingHom) ∧
      (β.toRingHom.comp (Polynomial.aeval (R := κ)
          (IsLocalization.Away.invSelf (S := Localization.Away (X : Polynomial κ)) (X : Polynomial
            κ))).toRingHom =
        (CurveModel.inclInf κ XX).toRingHom.comp α₁.toRingHom)
theorem

exists_iso_of_twoAffineLineCover

L221 ↗
AlgebraicCurve.CurveModel.exists_iso_of_twoAffineLineCover
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_exists_iso_of_twoAffineLineCover
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
open _root_.Polynomial
Lean source · statement
theorem _root_.AlgebraicCurve.CurveModel.exists_iso_of_twoAffineLineCover
    (κ : Type u) [Field κ] [IsAlgClosed κ] {Z : Scheme.{u}} (z : Z ⟶ Spec (CommRingCat.of κ))
    (i₀ i₁ : Spec (CommRingCat.of (Polynomial κ)) ⟶ Z) [IsOpenImmersion i₀] [IsOpenImmersion i₁]
    (hi₀ : i₀ ≫ z = Spec.map (CommRingCat.ofHom (algebraMap κ (Polynomial κ))))
    (hi₁ : i₁ ≫ z = Spec.map (CommRingCat.ofHom (algebraMap κ (Polynomial κ))))
    (hcov : Set.range i₀.base ∪ Set.range i₁.base = Set.univ)
    (hglue : Spec.map (CommRingCat.ofHom (algebraMap (Polynomial κ) (Localization.Away (X :
      Polynomial κ)))) ≫ i₀ =
      Spec.map (CommRingCat.ofHom (Polynomial.aeval (R := κ)
        (IsLocalization.Away.invSelf (S := Localization.Away (X : Polynomial κ)) (X : Polynomial
          κ))).toRingHom) ≫ i₁)
    (hmeet : Set.range i₀.base ∩ Set.range i₁.base ⊆
      Set.range (Spec.map (CommRingCat.ofHom (algebraMap (Polynomial κ) (Localization.Away (X :
        Polynomial κ)))) ≫ i₀).base) :
    ∃ (M : CurveModel κ (RatFunc κ)) (e : M.C ≅ Z), e.hom ≫ z = M.toBase

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