NYLL
Module

CurveModel_ker_comap_eq_prod_ker_pow_ramificationIndex.lean

Nyll.AlgebraicCurves.Models.CurveModel_ker_comap_eq_prod_ker_pow_ramificationIndex
26 declarations indexed from sourceView source ↗

Module documentation

Curve Model ker comap eq prod ker pow ramification Index

Imports5
Imported by3

Declarations

theorem

eq_unit_mul_pow_ord

L43 ↗
AlgebraicCurves.Models.Proofs.CurveModel_ker_comap_eq_prod_ker_pow_ramificationIndex.HG1b.eq_unit_mul_pow_ord
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_ker_comap_eq_prod_ker_pow_ramificationIndex
section SolBody
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
open _root_.Topology
universe u v
section H4
namespace HG1b
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
Lean source · statement
theorem eq_unit_mul_pow_ord (w : Place K F') {ϖ : w.toValuationSubring} (hϖ : Irreducible ϖ)
    {a : w.toValuationSubring} (ha : a ≠ 0) :
    ∃ u : w.toValuationSubringˣ, ∃ n : ℕ, a = u * ϖ ^ n ∧ w.ord (a : F') = n
theorem

mem_maximalIdeal_pow_of_le_ord

L55 ↗
AlgebraicCurves.Models.Proofs.CurveModel_ker_comap_eq_prod_ker_pow_ramificationIndex.HG1b.mem_maximalIdeal_pow_of_le_ord
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_ker_comap_eq_prod_ker_pow_ramificationIndex
section SolBody
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
open _root_.Topology
universe u v
section H4
namespace HG1b
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
Lean source · statement
theorem mem_maximalIdeal_pow_of_le_ord (w : Place K F') {a : w.toValuationSubring} (ha : a ≠ 0)
    {n : ℕ} (hn : (n : ℤ) ≤ w.ord (a : F')) :
    a ∈ IsLocalRing.maximalIdeal w.toValuationSubring ^ n
theorem

ord_pos_of_mem_maximalIdeal

L65 ↗
AlgebraicCurves.Models.Proofs.CurveModel_ker_comap_eq_prod_ker_pow_ramificationIndex.HG1b.ord_pos_of_mem_maximalIdeal
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_ker_comap_eq_prod_ker_pow_ramificationIndex
section SolBody
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
open _root_.Topology
universe u v
section H4
namespace HG1b
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
Lean source · statement
theorem ord_pos_of_mem_maximalIdeal (w : Place K F') {a : w.toValuationSubring} (ha : a ≠ 0)
    (hmem : a ∈ IsLocalRing.maximalIdeal w.toValuationSubring) : 0 < w.ord (a : F')
theorem

map_restrictInclusion_maximalIdeal

L79 ↗
HG1b.map_restrictInclusion_maximalIdeal
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_ker_comap_eq_prod_ker_pow_ramificationIndex
section SolBody
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
open _root_.Topology
universe u v
section H4
namespace HG1b
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
variable [Algebra.IsIntegral F F']
Lean source · statement
theorem _root_.HG1b.map_restrictInclusion_maximalIdeal (w : Place K F') :
    (IsLocalRing.maximalIdeal (w.restrict F).toValuationSubring).map (w.restrictInclusion F) =
      IsLocalRing.maximalIdeal w.toValuationSubring ^ w.ramificationIndex F
theorem

comap_eq_of_forall_ideal_preimage_eq

L155 ↗
AlgebraicCurves.Models.Proofs.CurveModel_ker_comap_eq_prod_ker_pow_ramificationIndex.AlgebraicGeometry.Scheme.IdealSheafData.comap_eq_of_forall_ideal_preimage_eq
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_ker_comap_eq_prod_ker_pow_ramificationIndex
section SolBody
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
open _root_.Topology
universe u v
open scoped _root_.AlgebraicGeometry _root_.AlgebraicGeometry.Scheme
  _root_.AlgebraicGeometry.Scheme.IdealSheafData in
Lean source · statement
theorem AlgebraicGeometry.Scheme.IdealSheafData.comap_eq_of_forall_ideal_preimage_eq
    {X Y : Scheme.{u}} (f : X ⟶ Y) [IsAffineHom f] (J : Y.IdealSheafData) (P : X.IdealSheafData)
    (h : ∀ U : Y.affineOpens,
      P.ideal ⟨f ⁻¹ᵁ U.1, U.2.preimage f⟩ = (J.ideal U).map (f.app U.1).hom) :
    J.comap f = P
theorem

map_restrictInclusion_maximalIdeal

L184 ↗
AlgebraicCurve.Place.map_restrictInclusion_maximalIdeal
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_ker_comap_eq_prod_ker_pow_ramificationIndex
section SolBody
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
open _root_.Topology
universe u v
namespace AlgebraicCurve.Place
open scoped _root_.AlgebraicCurve _root_.AlgebraicCurve.Place in
Lean source · statement
theorem _root_.AlgebraicCurve.Place.map_restrictInclusion_maximalIdeal
    {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F'] [Algebra F F']
    [IsScalarTower K F F'] [Algebra.IsIntegral F F'] (w : Place K F') :
    (IsLocalRing.maximalIdeal (w.restrict F).toValuationSubring).map (w.restrictInclusion F) =
      IsLocalRing.maximalIdeal w.toValuationSubring ^ w.ramificationIndex F
def

stalkToField

L207 ↗
AlgebraicCurves.Models.Proofs.CurveModel_ker_comap_eq_prod_ker_pow_ramificationIndex.HG1b.stalkToField
Documentation

The homomorphism from a stalk to the modeled function field.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_ker_comap_eq_prod_ker_pow_ramificationIndex
section StalkVal
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
universe u v
namespace HG1b
variable {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L]
Lean source · statement
def stalkToField (M : CurveModel K L) (z : M.C) : M.C.presheaf.stalk z →+* L
theorem

stalkToField_apply

L211 ↗
AlgebraicCurves.Models.Proofs.CurveModel_ker_comap_eq_prod_ker_pow_ramificationIndex.HG1b.stalkToField_apply
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_ker_comap_eq_prod_ker_pow_ramificationIndex
section StalkVal
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
universe u v
namespace HG1b
variable {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L]
Lean source · statement
theorem stalkToField_apply (M : CurveModel K L) (z : M.C) (s : M.C.presheaf.stalk z) :
    stalkToField M z s = M.ffEquiv.symm (algebraMap (M.C.presheaf.stalk z) M.C.functionField s)
theorem

stalkToField_injective

L215 ↗
AlgebraicCurves.Models.Proofs.CurveModel_ker_comap_eq_prod_ker_pow_ramificationIndex.HG1b.stalkToField_injective
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_ker_comap_eq_prod_ker_pow_ramificationIndex
section StalkVal
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
universe u v
namespace HG1b
variable {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L]
Lean source · statement
theorem stalkToField_injective (M : CurveModel K L) (z : M.C) : Function.Injective (stalkToField M
  z)
def

stalkEquivOfRange

L220 ↗
AlgebraicCurves.Models.Proofs.CurveModel_ker_comap_eq_prod_ker_pow_ramificationIndex.HG1b.stalkEquivOfRange
Documentation

The stalk equivalence with a valuation ring having the same image in the function field.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_ker_comap_eq_prod_ker_pow_ramificationIndex
section StalkVal
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
universe u v
namespace HG1b
variable {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L]
Lean source · statement
def stalkEquivOfRange (M : CurveModel K L) (z : M.C) (P : Place K L)
    (hr : (stalkToField M z).range = P.toValuationSubring.toSubring) :
    M.C.presheaf.stalk z ≃+* P.toValuationSubring
theorem

coe_stalkEquivOfRange

L233 ↗
AlgebraicCurves.Models.Proofs.CurveModel_ker_comap_eq_prod_ker_pow_ramificationIndex.HG1b.coe_stalkEquivOfRange
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_ker_comap_eq_prod_ker_pow_ramificationIndex
section StalkVal
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
universe u v
namespace HG1b
variable {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L]
Lean source · statement
theorem coe_stalkEquivOfRange (M : CurveModel K L) (z : M.C) (P : Place K L)
    (hr : (stalkToField M z).range = P.toValuationSubring.toSubring) (s : M.C.presheaf.stalk z) :
    ((stalkEquivOfRange M z P hr s : P.toValuationSubring) : L) = stalkToField M z s
theorem

map_stalkMap_maximalIdeal_eq_pow

L239 ↗
AlgebraicCurves.Models.Proofs.CurveModel_ker_comap_eq_prod_ker_pow_ramificationIndex.HG1b.map_stalkMap_maximalIdeal_eq_pow
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_ker_comap_eq_prod_ker_pow_ramificationIndex
section StalkVal
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
universe u v
Lean source · statement
theorem HG1b.map_stalkMap_maximalIdeal_eq_pow
    {k : Type u} [Field k] [IsAlgClosed k] {F F' : Type v} [Field F] [Field F'] [Algebra k F]
      [Algebra k F']
    [IsCurveOver k F] [IsCurveOver k F'] [Algebra.EssFiniteType k F] [Algebra.EssFiniteType k F']
    [Algebra F F'] [IsScalarTower k F F'] [Algebra.IsIntegral F F']
    (M : CurveModel k F) (M' : CurveModel k F')
    (π : M'.C ⟶ M.C) (hπ : π ≫ M.toBase = M'.toBase)
    [IsFinite π] [Flat π] [LocallyOfFinitePresentation π]
    (hplace : ∀ (y : {q : Spec (CommRingCat.of k) ⟶ M'.C // q ≫ M'.toBase = 𝟙 _})
        (x : {q : Spec (CommRingCat.of k) ⟶ M.C // q ≫ M.toBase = 𝟙 _}),
      y.1 ≫ π = x.1 → (M'.pointEquivPlace y).restrict F = M.pointEquivPlace x)
    (y : {q : Spec (CommRingCat.of k) ⟶ M'.C // q ≫ M'.toBase = 𝟙 _}) :
    (IsLocalRing.maximalIdeal (M.C.presheaf.stalk (π.base (pointEquivClosedPoint M'.toBase
      y).1))).map
        (π.stalkMap (pointEquivClosedPoint M'.toBase y).1).hom =
      IsLocalRing.maximalIdeal (M'.C.presheaf.stalk (pointEquivClosedPoint M'.toBase y).1) ^
        ((M'.pointEquivPlace y).ramificationIndex F)
theorem

map_germ_primeIdealOf

L306 ↗
AlgebraicCurves.Models.Proofs.CurveModel_ker_comap_eq_prod_ker_pow_ramificationIndex.HG1bPlumbing.map_germ_primeIdealOf
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_ker_comap_eq_prod_ker_pow_ramificationIndex
section Plumb
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Topology
universe u
namespace HG1bPlumbing
Lean source · statement
theorem map_germ_primeIdealOf {X : Scheme.{u}} {U : X.Opens} (hU : IsAffineOpen U) (z : U) :
    (hU.primeIdealOf z).asIdeal.map (X.presheaf.germ U z.1 z.2).hom =
      IsLocalRing.maximalIdeal (X.presheaf.stalk z.1)
theorem

map_germ_eq_top_of_not_le

L313 ↗
AlgebraicCurves.Models.Proofs.CurveModel_ker_comap_eq_prod_ker_pow_ramificationIndex.HG1bPlumbing.map_germ_eq_top_of_not_le
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_ker_comap_eq_prod_ker_pow_ramificationIndex
section Plumb
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Topology
universe u
namespace HG1bPlumbing
Lean source · statement
theorem map_germ_eq_top_of_not_le {X : Scheme.{u}} {U : X.Opens} (hU : IsAffineOpen U) (z : U)
    {I : Ideal Γ(X, U)} (hI : ¬ I ≤ (hU.primeIdealOf z).asIdeal) :
    I.map (X.presheaf.germ U z.1 z.2).hom = ⊤
theorem

comap_germ_maximalIdeal

L324 ↗
AlgebraicCurves.Models.Proofs.CurveModel_ker_comap_eq_prod_ker_pow_ramificationIndex.HG1bPlumbing.comap_germ_maximalIdeal
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_ker_comap_eq_prod_ker_pow_ramificationIndex
section Plumb
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Topology
universe u
namespace HG1bPlumbing
Lean source · statement
theorem comap_germ_maximalIdeal {X : Scheme.{u}} {U : X.Opens} (hU : IsAffineOpen U) (z : U) :
    (IsLocalRing.maximalIdeal (X.presheaf.stalk z.1)).comap (X.presheaf.germ U z.1 z.2).hom =
      (hU.primeIdealOf z).asIdeal
theorem

maximalIdeal_stalk_eq_bot_of_isField

L330 ↗
AlgebraicCurves.Models.Proofs.CurveModel_ker_comap_eq_prod_ker_pow_ramificationIndex.HG1bPlumbing.maximalIdeal_stalk_eq_bot_of_isField
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_ker_comap_eq_prod_ker_pow_ramificationIndex
section Plumb
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Topology
universe u
namespace HG1bPlumbing
Lean source · statement
theorem maximalIdeal_stalk_eq_bot_of_isField {X : Scheme.{u}} {U : X.Opens} (hU : IsAffineOpen U)
  (z : U)
    (hF : IsField Γ(X, U)) : IsLocalRing.maximalIdeal (X.presheaf.stalk z.1) = ⊥
theorem

ker_ideal_eq_top_of_not_mem

L343 ↗
AlgebraicCurves.Models.Proofs.CurveModel_ker_comap_eq_prod_ker_pow_ramificationIndex.HG1bPlumbing.ker_ideal_eq_top_of_not_mem
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_ker_comap_eq_prod_ker_pow_ramificationIndex
section Plumb
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Topology
universe u
namespace HG1bPlumbing
Lean source · statement
theorem ker_ideal_eq_top_of_not_mem {X : Scheme.{u}} {K : Type u} [Field K]
    (p : Spec (CommRingCat.of K) ⟶ X) [QuasiCompact p] (U : X.affineOpens)
    (h : p.base (IsLocalRing.closedPoint K) ∉ (U : X.Opens)) :
    p.ker.ideal U = ⊤
theorem

ker_eq_maximalIdeal_of_isLocalHom

L358 ↗
AlgebraicCurves.Models.Proofs.CurveModel_ker_comap_eq_prod_ker_pow_ramificationIndex.HG1bPlumbing.ker_eq_maximalIdeal_of_isLocalHom
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_ker_comap_eq_prod_ker_pow_ramificationIndex
section Plumb
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Topology
universe u
namespace HG1bPlumbing
Lean source · statement
theorem ker_eq_maximalIdeal_of_isLocalHom {R S : Type*} [CommRing R] [IsLocalRing R] [CommRing S]
  [IsLocalRing S]
    (hS : IsLocalRing.maximalIdeal S = ⊥) (φ : R →+* S) [IsLocalHom φ] :
    RingHom.ker φ = IsLocalRing.maximalIdeal R
theorem

isField_ΓSpec_top

L373 ↗
AlgebraicCurves.Models.Proofs.CurveModel_ker_comap_eq_prod_ker_pow_ramificationIndex.HG1bPlumbing.isField_ΓSpec_top
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_ker_comap_eq_prod_ker_pow_ramificationIndex
section Plumb
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Topology
universe u
namespace HG1bPlumbing
Lean source · statement
theorem isField_ΓSpec_top (K : Type u) [Field K] : IsField Γ(Spec (CommRingCat.of K), ⊤)
theorem

isField_ΓSpec

L377 ↗
AlgebraicCurves.Models.Proofs.CurveModel_ker_comap_eq_prod_ker_pow_ramificationIndex.HG1bPlumbing.isField_ΓSpec
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_ker_comap_eq_prod_ker_pow_ramificationIndex
section Plumb
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Topology
universe u
namespace HG1bPlumbing
Lean source · statement
theorem isField_ΓSpec (K : Type u) [Field K] (V : (Spec (CommRingCat.of K)).Opens)
    (hV : IsLocalRing.closedPoint K ∈ V) : IsField Γ(Spec (CommRingCat.of K), V)
theorem

maximalIdeal_stalk_Spec_field_eq_bot

L385 ↗
AlgebraicCurves.Models.Proofs.CurveModel_ker_comap_eq_prod_ker_pow_ramificationIndex.HG1bPlumbing.maximalIdeal_stalk_Spec_field_eq_bot
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_ker_comap_eq_prod_ker_pow_ramificationIndex
section Plumb
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Topology
universe u
namespace HG1bPlumbing
Lean source · full declaration
theorem maximalIdeal_stalk_Spec_field_eq_bot (K : Type u) [Field K] :
    IsLocalRing.maximalIdeal ((Spec (CommRingCat.of K)).presheaf.stalk
      (show ↥(Spec (CommRingCat.of K)) from IsLocalRing.closedPoint K)) = ⊥ :=
  maximalIdeal_stalk_eq_bot_of_isField (isAffineOpen_top _) ⟨IsLocalRing.closedPoint K, trivial⟩
    (isField_ΓSpec_top K)
theorem

ker_ideal_eq_primeIdealOf

L391 ↗
AlgebraicCurves.Models.Proofs.CurveModel_ker_comap_eq_prod_ker_pow_ramificationIndex.HG1bPlumbing.ker_ideal_eq_primeIdealOf
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_ker_comap_eq_prod_ker_pow_ramificationIndex
section Plumb
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Topology
universe u
namespace HG1bPlumbing
Lean source · statement
theorem ker_ideal_eq_primeIdealOf {X : Scheme.{u}} {K : Type u} [Field K]
    (p : Spec (CommRingCat.of K) ⟶ X) [QuasiCompact p] (U : X.affineOpens)
    (h : p.base (IsLocalRing.closedPoint K) ∈ (U : X.Opens)) :
    p.ker.ideal U = (U.2.primeIdealOf ⟨_, h⟩).asIdeal
theorem

ideal_eq_of_forall_isClosed_map_germ_eq

L415 ↗
AlgebraicCurves.Models.Proofs.CurveModel_ker_comap_eq_prod_ker_pow_ramificationIndex.HG1bPlumbing.ideal_eq_of_forall_isClosed_map_germ_eq
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_ker_comap_eq_prod_ker_pow_ramificationIndex
section Plumb
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Topology
universe u
namespace HG1bPlumbing
Lean source · statement
theorem ideal_eq_of_forall_isClosed_map_germ_eq {X : Scheme.{u}} [JacobsonSpace X] {U : X.Opens}
    (hU : IsAffineOpen U) {I J : Ideal Γ(X, U)}
    (h : ∀ z : U, IsClosed ({z.1} : Set X) →
      I.map (X.presheaf.germ U z.1 z.2).hom = J.map (X.presheaf.germ U z.1 z.2).hom) : I = J
theorem

map_app_ideal_ker_eq_prod_pow

L459 ↗
AlgebraicCurves.Models.Proofs.CurveModel_ker_comap_eq_prod_ker_pow_ramificationIndex.HG1b.map_app_ideal_ker_eq_prod_pow
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_ker_comap_eq_prod_ker_pow_ramificationIndex
section H2proof
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
open _root_.Topology
universe u v
Lean source · statement
theorem HG1b.map_app_ideal_ker_eq_prod_pow
    {k : Type u} [Field k] [IsAlgClosed k] {F F' : Type v} [Field F] [Field F'] [Algebra k F]
      [Algebra k F']
    [IsCurveOver k F] [IsCurveOver k F'] [Algebra.EssFiniteType k F] [Algebra.EssFiniteType k F']
    [Algebra F F'] [IsScalarTower k F F'] [Algebra.IsIntegral F F']
    (M : CurveModel k F) (M' : CurveModel k F')
    (π : M'.C ⟶ M.C) (hπ : π ≫ M.toBase = M'.toBase)
    [IsFinite π] [Flat π] [LocallyOfFinitePresentation π]
    (hplace : ∀ (y : {q : Spec (CommRingCat.of k) ⟶ M'.C // q ≫ M'.toBase = 𝟙 _})
        (x : {q : Spec (CommRingCat.of k) ⟶ M.C // q ≫ M.toBase = 𝟙 _}),
      y.1 ≫ π = x.1 → (M'.pointEquivPlace y).restrict F = M.pointEquivPlace x)
    (x : {q : Spec (CommRingCat.of k) ⟶ M.C // q ≫ M.toBase = 𝟙 _}) (U : M.C.affineOpens) :
    ((x.1.ker).ideal U).map (π.app U.1).hom =
      ∏ w ∈ (M.pointEquivPlace x).fiber F',
        (((M'.pointEquivPlace.symm w).1.ker).ideal ⟨π ⁻¹ᵁ U.1, U.2.preimage π⟩) ^
          (w.ramificationIndex F)
theorem

ideal_finset_prod_pow

L614 ↗
AlgebraicCurves.Models.Proofs.CurveModel_ker_comap_eq_prod_ker_pow_ramificationIndex.AlgebraicGeometry.Scheme.IdealSheafData.ideal_finset_prod_pow
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_ker_comap_eq_prod_ker_pow_ramificationIndex
section Head
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
universe u v
open scoped _root_.AlgebraicGeometry _root_.AlgebraicGeometry.Scheme
  _root_.AlgebraicGeometry.Scheme.IdealSheafData in
Lean source · statement
theorem AlgebraicGeometry.Scheme.IdealSheafData.ideal_finset_prod_pow {X : Scheme.{u}} {ι : Type*}
    (s : Finset ι) (I : ι → X.IdealSheafData) (n : ι → ℕ) (V : X.affineOpens) :
    (∏ i ∈ s, I i ^ n i).ideal V = ∏ i ∈ s, (I i).ideal V ^ n i
theorem

ker_comap_eq_prod_ker_pow_ramificationIndex

L627 ↗
AlgebraicCurve.CurveModel.ker_comap_eq_prod_ker_pow_ramificationIndex
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_ker_comap_eq_prod_ker_pow_ramificationIndex
section Head
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
universe u v
open
  CurveModel_ker_comap_eq_prod_ker_pow_ramificationIndex.AlgebraicGeometry.Scheme.IdealSheafData in
Lean source · statement
theorem _root_.AlgebraicCurve.CurveModel.ker_comap_eq_prod_ker_pow_ramificationIndex
    {k : Type u} [Field k] [IsAlgClosed k] {F F' : Type v} [Field F] [Field F'] [Algebra k F]
      [Algebra k F']
    [IsCurveOver k F] [IsCurveOver k F'] [Algebra.EssFiniteType k F] [Algebra.EssFiniteType k F']
    [Algebra F F'] [IsScalarTower k F F'] [Algebra.IsIntegral F F']
    (M : CurveModel k F) (M' : CurveModel k F')
    (π : M'.C ⟶ M.C) (hπ : π ≫ M.toBase = M'.toBase)
    [IsFinite π] [Flat π] [LocallyOfFinitePresentation π]
    (hplace : ∀ (y : {q : Spec (CommRingCat.of k) ⟶ M'.C // q ≫ M'.toBase = 𝟙 _})
        (x : {q : Spec (CommRingCat.of k) ⟶ M.C // q ≫ M.toBase = 𝟙 _}),
      y.1 ≫ π = x.1 → (M'.pointEquivPlace y).restrict F = M.pointEquivPlace x)
    (x : {q : Spec (CommRingCat.of k) ⟶ M.C // q ≫ M.toBase = 𝟙 _}) :
    (x.1.ker).comap π =
      ∏ w ∈ (M.pointEquivPlace x).fiber F', ((M'.pointEquivPlace.symm w).1.ker) ^
        (w.ramificationIndex F)

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