Module

Scheme_Hom_isInvertible_ker_of_comp_eq_id.lean

Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_Hom_isInvertible_ker_of_comp_eq_id

9 declarations indexed from sourceView source ↗

Module documentation

Invertibility of the ideal of a section of a smooth curve and its affine retraction calculations.

Imports12

Batteries.Tactic.Init
Mathlib.RingTheory.Unramified.Finite
Mathlib.RingTheory.RingHom.StandardSmooth
Mathlib.RingTheory.Polynomial.Quotient
Mathlib.RingTheory.MvPolynomial.Localization
Mathlib.RingTheory.Flat.TorsionFree
Mathlib.Tactic.TermCongr
Mathlib.Tactic.Ring
Mathlib.Tactic.Set
Nyll.AlgebraicCurves.RelativeDivisors.Cartier
Mathlib.AlgebraicGeometry.Morphisms.Smooth
Mathlib.AlgebraicGeometry.Morphisms.Separated

Imported by52

theorem

exists_map_eq_one_mul_eq_zero

L43 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_Hom_isInvertible_ker_of_comp_eq_id.RetractionKernel.exists_map_eq_one_mul_eq_zero

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_Hom_isInvertible_ker_of_comp_eq_id
universe u
section Engine
open TensorProduct nonZeroDivisors MvPolynomial
namespace RetractionKernel

Lean source · statement

theorem exists_map_eq_one_mul_eq_zero {A E : Type*} [CommRing A] [CommRing E] [Algebra A E]
    [Algebra.FormallyUnramified A E] [Algebra.EssFiniteType A E] (σ : E →ₐ[A] A) :
    ∃ e₀ : E, σ e₀ = 1 ∧ ∀ y, σ y = 0 → y * e₀ = 0

theorem

exists_ker_map_eq_span

L59 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_Hom_isInvertible_ker_of_comp_eq_id.RetractionKernel.exists_ker_map_eq_span

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_Hom_isInvertible_ker_of_comp_eq_id
universe u
section Engine
open TensorProduct nonZeroDivisors MvPolynomial
namespace RetractionKernel

Lean source · statement

theorem exists_ker_map_eq_span {A E : Type*} [CommRing A] [CommRing E] [Algebra A E]
    (σ : E →ₐ[A] A) (h : E) (hh : σ h = 0)
    [Algebra.FormallyUnramified A (E ⧸ Ideal.span {h})]
    [Algebra.EssFiniteType A (E ⧸ Ideal.span {h})]
    (P : Ideal E) [P.IsPrime] (hP : RingHom.ker σ ≤ P) :
    ∃ u ∉ P, ∀ (L : Type*) [CommRing L] [Algebra E L] [IsLocalization.Away u L],
      (RingHom.ker σ).map (algebraMap E L) = Ideal.span {algebraMap E L h}

theorem

algebraMap_mem_nonZeroDivisors

L100 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_Hom_isInvertible_ker_of_comp_eq_id.RetractionKernel.algebraMap_mem_nonZeroDivisors

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_Hom_isInvertible_ker_of_comp_eq_id
universe u
section Engine
open TensorProduct nonZeroDivisors MvPolynomial
namespace RetractionKernel

Lean source · statement

theorem algebraMap_mem_nonZeroDivisors {E : Type*} [CommRing E] (M : Submonoid E)
    (L : Type*) [CommRing L] [Algebra E L] [IsLocalization M L] {h : E} (hh : h ∈ E⁰) :
    algebraMap E L h ∈ L⁰

theorem

algebraMap_X_sub_C_mem_nonZeroDivisors

L112 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_Hom_isInvertible_ker_of_comp_eq_id.RetractionKernel.algebraMap_X_sub_C_mem_nonZeroDivisors

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_Hom_isInvertible_ker_of_comp_eq_id
universe u
section Engine
open TensorProduct nonZeroDivisors MvPolynomial
namespace RetractionKernel

Lean source · statement

theorem algebraMap_X_sub_C_mem_nonZeroDivisors {A E : Type*} [CommRing A] [CommRing E]
    [Algebra (MvPolynomial (Fin 1) A) E] [Module.Flat (MvPolynomial (Fin 1) A) E] (φ : A) :
    algebraMap (MvPolynomial (Fin 1) A) E (X 0 - C φ) ∈ E⁰

def

quotientXSubCAlgEquiv

L130 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_Hom_isInvertible_ker_of_comp_eq_id.RetractionKernel.quotientXSubCAlgEquiv

Documentation

The quotient of a one-variable polynomial algebra by X minus a constant, identified with its coefficient algebra.

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_Hom_isInvertible_ker_of_comp_eq_id
universe u
section Engine
open TensorProduct nonZeroDivisors MvPolynomial
namespace RetractionKernel

Lean source · statement

def quotientXSubCAlgEquiv (A : Type*) [CommRing A] (φ : A) :
    (MvPolynomial (Fin 1) A ⧸ Ideal.span {(X 0 - C φ : MvPolynomial (Fin 1) A)}) ≃ₐ[A] A

theorem

formallyUnramified_essFiniteType_quotient

L140 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_Hom_isInvertible_ker_of_comp_eq_id.RetractionKernel.formallyUnramified_essFiniteType_quotient

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_Hom_isInvertible_ker_of_comp_eq_id
universe u
section Engine
open TensorProduct nonZeroDivisors MvPolynomial
namespace RetractionKernel

Lean source · statement

theorem formallyUnramified_essFiniteType_quotient {A P E : Type*} [CommRing A] [CommRing P]
    [CommRing E] [Algebra A P] [Algebra A E] [Algebra P E] [IsScalarTower A P E]
    [Algebra.FormallyUnramified P E] [Algebra.FiniteType P E] [Algebra.FiniteType A P]
    (p₀ : P) (e : (P ⧸ Ideal.span {p₀}) ≃ₐ[A] A) :
    Algebra.FormallyUnramified A (E ⧸ Ideal.span {algebraMap P E p₀}) ∧
      Algebra.EssFiniteType A (E ⧸ Ideal.span {algebraMap P E p₀})

theorem

subsingleton_sections_bot

L189 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_Hom_isInvertible_ker_of_comp_eq_id.GraphLocalEquation.subsingleton_sections_bot

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_Hom_isInvertible_ker_of_comp_eq_id
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace nonZeroDivisors
noncomputable section
namespace GraphLocalEquation

Lean source · statement

theorem subsingleton_sections_bot (T : Scheme.{u}) {V : T.Opens} (hV : V = ⊥) :
    Subsingleton Γ(T, V)

theorem

section_local_equation

L196 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_Hom_isInvertible_ker_of_comp_eq_id.section_local_equation

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_Hom_isInvertible_ker_of_comp_eq_id
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace nonZeroDivisors
noncomputable section
open GraphLocalEquation in

Lean source · statement

theorem section_local_equation {X T : Scheme.{u}} (p : X ⟶ T) [IsSeparated p]
    [SmoothOfRelativeDimension 1 p] (σ₀ : T ⟶ X) (hσ₀ : σ₀ ≫ p = 𝟙 T) (x : ↥X) :
    ∃ (U : X.affineOpens) (u : Γ(X, U)), x ∈ X.basicOpen u ∧
      ∃ g ∈ nonZeroDivisors Γ(X, X.affineBasicOpen u),
        σ₀.ker.ideal (X.affineBasicOpen u) = Ideal.span {g}

theorem

isInvertible_ker_of_comp_eq_id

L379 ↗

AlgebraicGeometry.Scheme.Hom.isInvertible_ker_of_comp_eq_id

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_Hom_isInvertible_ker_of_comp_eq_id
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace nonZeroDivisors
noncomputable section

Lean source · statement

theorem _root_.AlgebraicGeometry.Scheme.Hom.isInvertible_ker_of_comp_eq_id {X T : Scheme.{u}} {p
    : X ⟶ T} [IsSeparated p] [SmoothOfRelativeDimension 1 p]
    (σ : T ⟶ X) (hσ : σ ≫ p = 𝟙 T) : σ.ker.IsInvertible

Module documentation

Declarations