Module

CommRing_Pic_exists_boundaryHom_conductorSquare_exact.lean

Nyll.AlgebraicCurves.Geometry.Picard.CommRing_Pic_exists_boundaryHom_conductorSquare_exact

28 declarations indexed from sourceView source ↗

Module documentation

Comm Ring Pic exists boundary Hom conductor Square exact

Imports22

Mathlib.RingTheory.PicardGroup
Mathlib.Algebra.Algebra.Basic
Mathlib.Algebra.Algebra.Operations
Mathlib.Algebra.Group.Hom.Basic
Mathlib.Algebra.Group.Subgroup.Ker
Mathlib.Algebra.Group.Units.Basic
Mathlib.Algebra.Group.Units.Defs
Mathlib.Algebra.Group.Units.Hom
Mathlib.Algebra.GroupWithZero.Units.Basic
Mathlib.Algebra.Module.Submodule.Defs
Mathlib.Algebra.Module.Submodule.Equiv
Mathlib.LinearAlgebra.Span.Defs
Mathlib.LinearAlgebra.Quotient.Defs
Mathlib.LinearAlgebra.TensorProduct.Defs
Mathlib.LinearAlgebra.TensorProduct.Quotient
Mathlib.LinearAlgebra.TensorProduct.Tower
Mathlib.RingTheory.Ideal.Maps
Mathlib.RingTheory.Ideal.Quotient.Defs
Mathlib.RingTheory.Ideal.Quotient.Operations
Mathlib.RingTheory.TensorProduct.Basic
Mathlib.Tactic.Ext
Mathlib.Tactic.Ring.RingNF

Imported by1

Nyll.AlgebraicCurves.Geometry.Picard.All

def

glueSubmodule

L57 ↗

AlgebraicCurves.Geometry.Picard.Proofs.CommRing_Pic_exists_boundaryHom_conductorSquare_exact.ConductorSquare.glueSubmodule

Documentation

The submodule of elements whose residue, multiplied by the gluing parameter, comes from the base ring.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace CommRing_Pic_exists_boundaryHom_conductorSquare_exact
open TensorProduct
universe u v
namespace ConductorSquare
variable {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B]

Lean source · full declaration

def glueSubmodule (𝔠 : Ideal B) (u : B ⧸ 𝔠) : Submodule A B where
  carrier := {x | ∃ a : A, u * Ideal.Quotient.mk 𝔠 x = Ideal.Quotient.mk 𝔠 (algebraMap A B a)}
  zero_mem' := ⟨0, by simp⟩
  add_mem' := by
    rintro x y ⟨a, ha⟩ ⟨a', ha'⟩
    exact ⟨a + a', by rw [map_add, mul_add, ha, ha', map_add, map_add]⟩
  smul_mem' := by
    rintro r x ⟨a, ha⟩
    refine ⟨r * a, ?_⟩
    rw [Algebra.smul_def, map_mul, mul_left_comm, ha, ← map_mul, ← map_mul]

theorem

mem_glueSubmodule

L70 ↗

AlgebraicCurves.Geometry.Picard.Proofs.CommRing_Pic_exists_boundaryHom_conductorSquare_exact.ConductorSquare.mem_glueSubmodule

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace CommRing_Pic_exists_boundaryHom_conductorSquare_exact
open TensorProduct
universe u v
namespace ConductorSquare
variable {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B]
variable (𝔠 : Ideal B)

Lean source · statement

theorem mem_glueSubmodule {u : B ⧸ 𝔠} {x : B} :
    x ∈ glueSubmodule (A := A) 𝔠 u ↔
      ∃ a : A, u * Ideal.Quotient.mk 𝔠 x = Ideal.Quotient.mk 𝔠 (algebraMap A B a)

theorem

mem_glueSubmodule_of_mem

L75 ↗

AlgebraicCurves.Geometry.Picard.Proofs.CommRing_Pic_exists_boundaryHom_conductorSquare_exact.ConductorSquare.mem_glueSubmodule_of_mem

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace CommRing_Pic_exists_boundaryHom_conductorSquare_exact
open TensorProduct
universe u v
namespace ConductorSquare
variable {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B]
variable (𝔠 : Ideal B)

Lean source · statement

theorem mem_glueSubmodule_of_mem {u : B ⧸ 𝔠} {x : B} (hx : x ∈ 𝔠) :
    x ∈ glueSubmodule (A := A) 𝔠 u

theorem

glueSubmodule_mul_le

L79 ↗

AlgebraicCurves.Geometry.Picard.Proofs.CommRing_Pic_exists_boundaryHom_conductorSquare_exact.ConductorSquare.glueSubmodule_mul_le

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace CommRing_Pic_exists_boundaryHom_conductorSquare_exact
open TensorProduct
universe u v
namespace ConductorSquare
variable {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B]
variable (𝔠 : Ideal B)

Lean source · statement

theorem glueSubmodule_mul_le (u v : B ⧸ 𝔠) :
    glueSubmodule (A := A) 𝔠 u * glueSubmodule 𝔠 v ≤ glueSubmodule 𝔠 (u * v)

theorem

exists_eq_of_mk_eq

L92 ↗

AlgebraicCurves.Geometry.Picard.Proofs.CommRing_Pic_exists_boundaryHom_conductorSquare_exact.ConductorSquare.exists_eq_of_mk_eq

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace CommRing_Pic_exists_boundaryHom_conductorSquare_exact
open TensorProduct
universe u v
namespace ConductorSquare
variable {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B]
variable (𝔠 : Ideal B)
section conductor
variable {𝔠}
variable (h𝔠 : ∀ b ∈ 𝔠, b ∈ Set.range (algebraMap A B))
include h𝔠

Lean source · statement

theorem exists_eq_of_mk_eq {x : B} {a : A}
    (h : Ideal.Quotient.mk 𝔠 x = Ideal.Quotient.mk 𝔠 (algebraMap A B a)) :
    ∃ a' : A, algebraMap A B a' = x

theorem

glueSubmodule_one

L99 ↗

AlgebraicCurves.Geometry.Picard.Proofs.CommRing_Pic_exists_boundaryHom_conductorSquare_exact.ConductorSquare.glueSubmodule_one

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace CommRing_Pic_exists_boundaryHom_conductorSquare_exact
open TensorProduct
universe u v
namespace ConductorSquare
variable {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B]
variable (𝔠 : Ideal B)
section conductor
variable {𝔠}
variable (h𝔠 : ∀ b ∈ 𝔠, b ∈ Set.range (algebraMap A B))
include h𝔠

Lean source · statement

theorem glueSubmodule_one : glueSubmodule (A := A) 𝔠 1 = 1

theorem

le_glueSubmodule_mul

L113 ↗

AlgebraicCurves.Geometry.Picard.Proofs.CommRing_Pic_exists_boundaryHom_conductorSquare_exact.ConductorSquare.le_glueSubmodule_mul

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace CommRing_Pic_exists_boundaryHom_conductorSquare_exact
open TensorProduct
universe u v
namespace ConductorSquare
variable {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B]
variable (𝔠 : Ideal B)
section conductor
variable {𝔠}
variable (h𝔠 : ∀ b ∈ 𝔠, b ∈ Set.range (algebraMap A B))
include h𝔠
variable [FaithfulSMul A B]
omit [FaithfulSMul A B] in
omit h𝔠 in

Lean source · statement

theorem le_glueSubmodule_mul (u : (B ⧸ 𝔠)ˣ) :
    (𝔠.restrictScalars A : Submodule A B) ≤
      glueSubmodule (A := A) 𝔠 (u : B ⧸ 𝔠) * glueSubmodule 𝔠 (↑u⁻¹ : B ⧸ 𝔠)

theorem

glueSubmodule_mul_inv

L135 ↗

AlgebraicCurves.Geometry.Picard.Proofs.CommRing_Pic_exists_boundaryHom_conductorSquare_exact.ConductorSquare.glueSubmodule_mul_inv

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace CommRing_Pic_exists_boundaryHom_conductorSquare_exact
open TensorProduct
universe u v
namespace ConductorSquare
variable {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B]
variable (𝔠 : Ideal B)
section conductor
variable {𝔠}
variable (h𝔠 : ∀ b ∈ 𝔠, b ∈ Set.range (algebraMap A B))
include h𝔠
variable [FaithfulSMul A B]
omit [FaithfulSMul A B] in

Lean source · statement

theorem glueSubmodule_mul_inv (u : (B ⧸ 𝔠)ˣ) :
    glueSubmodule (A := A) 𝔠 (u : B ⧸ 𝔠) * glueSubmodule 𝔠 (↑u⁻¹ : B ⧸ 𝔠) = 1

def

glueUnits

L160 ↗

AlgebraicCurves.Geometry.Picard.Proofs.CommRing_Pic_exists_boundaryHom_conductorSquare_exact.ConductorSquare.glueUnits

Documentation

The multiplicative map sending a residue-ring unit to the corresponding invertible gluing submodule.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace CommRing_Pic_exists_boundaryHom_conductorSquare_exact
open TensorProduct
universe u v
namespace ConductorSquare
variable {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B]
variable (𝔠 : Ideal B)
section conductor
variable {𝔠}
variable (h𝔠 : ∀ b ∈ 𝔠, b ∈ Set.range (algebraMap A B))
include h𝔠
variable [FaithfulSMul A B]

Lean source · full declaration

def glueUnits : (B ⧸ 𝔠)ˣ →* (Submodule A B)ˣ where
  toFun u :=
    { val := glueSubmodule 𝔠 (u : B ⧸ 𝔠)
      inv := glueSubmodule 𝔠 (↑u⁻¹ : B ⧸ 𝔠)
      val_inv := glueSubmodule_mul_inv h𝔠 u
      inv_val := by rw [mul_comm]; exact glueSubmodule_mul_inv h𝔠 u }
  map_one' := Units.ext (by simp only [Units.val_one]; exact glueSubmodule_one h𝔠)
  map_mul' u v := by
    apply Units.ext
    simp only [Units.val_mul]
    apply le_antisymm
    · have h1 : glueSubmodule (A := A) 𝔠 (↑v⁻¹ : B ⧸ 𝔠) * glueSubmodule 𝔠 (v : B ⧸ 𝔠) = 1 := by
        rw [mul_comm]; exact glueSubmodule_mul_inv h𝔠 v
      calc glueSubmodule (A := A) 𝔠 ((u : B ⧸ 𝔠) * v)
          = glueSubmodule 𝔠 ((u : B ⧸ 𝔠) * v) *
              (glueSubmodule 𝔠 (↑v⁻¹ : B ⧸ 𝔠) * glueSubmodule 𝔠 (v : B ⧸ 𝔠)) := by
            rw [h1, mul_one]
        _ = glueSubmodule 𝔠 ((u : B ⧸ 𝔠) * v) * glueSubmodule 𝔠 (↑v⁻¹ : B ⧸ 𝔠) *
              glueSubmodule 𝔠 (v : B ⧸ 𝔠) := by rw [mul_assoc]
        _ ≤ glueSubmodule 𝔠 ((u : B ⧸ 𝔠) * v * ↑v⁻¹) * glueSubmodule 𝔠 (v : B ⧸ 𝔠) :=
            Submodule.mul_le.mpr fun m hm n hn =>
              Submodule.mul_mem_mul (glueSubmodule_mul_le 𝔠 _ _ hm) hn
        _ = glueSubmodule 𝔠 (u : B ⧸ 𝔠) * glueSubmodule 𝔠 (v : B ⧸ 𝔠) := by
            rw [Units.mul_inv_cancel_right]
    · exact glueSubmodule_mul_le 𝔠 _ _

theorem

val_glueUnits

L186 ↗

AlgebraicCurves.Geometry.Picard.Proofs.CommRing_Pic_exists_boundaryHom_conductorSquare_exact.ConductorSquare.val_glueUnits

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace CommRing_Pic_exists_boundaryHom_conductorSquare_exact
open TensorProduct
universe u v
namespace ConductorSquare
variable {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B]
variable (𝔠 : Ideal B)
section conductor
variable {𝔠}
variable (h𝔠 : ∀ b ∈ 𝔠, b ∈ Set.range (algebraMap A B))
include h𝔠
variable [FaithfulSMul A B]
omit [FaithfulSMul A B] in

Lean source · statement

theorem val_glueUnits (u : (B ⧸ 𝔠)ˣ) :
    (glueUnits h𝔠 u : Submodule A B) = glueSubmodule 𝔠 (u : B ⧸ 𝔠)

def

boundary

L190 ↗

AlgebraicCurves.Geometry.Picard.Proofs.CommRing_Pic_exists_boundaryHom_conductorSquare_exact.ConductorSquare.boundary

Documentation

The boundary homomorphism from residue-ring units to the Picard group of the base ring.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace CommRing_Pic_exists_boundaryHom_conductorSquare_exact
open TensorProduct
universe u v
namespace ConductorSquare
variable {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B]
variable (𝔠 : Ideal B)
section conductor
variable {𝔠}
variable (h𝔠 : ∀ b ∈ 𝔠, b ∈ Set.range (algebraMap A B))
include h𝔠
variable [FaithfulSMul A B]

Lean source · statement

def boundary : (B ⧸ 𝔠)ˣ →* CommRing.Pic A

theorem

boundary_apply

L193 ↗

AlgebraicCurves.Geometry.Picard.Proofs.CommRing_Pic_exists_boundaryHom_conductorSquare_exact.ConductorSquare.boundary_apply

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace CommRing_Pic_exists_boundaryHom_conductorSquare_exact
open TensorProduct
universe u v
namespace ConductorSquare
variable {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B]
variable (𝔠 : Ideal B)
section conductor
variable {𝔠}
variable (h𝔠 : ∀ b ∈ 𝔠, b ∈ Set.range (algebraMap A B))
include h𝔠
variable [FaithfulSMul A B]

Lean source · statement

theorem boundary_apply (u : (B ⧸ 𝔠)ˣ) :
    boundary h𝔠 u = Submodule.unitsToPic A B (glueUnits h𝔠 u)

def

boundaryEquiv

L197 ↗

AlgebraicCurves.Geometry.Picard.Proofs.CommRing_Pic_exists_boundaryHom_conductorSquare_exact.ConductorSquare.boundaryEquiv

Documentation

The linear equivalence realizing the boundary Picard class as the gluing submodule.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace CommRing_Pic_exists_boundaryHom_conductorSquare_exact
open TensorProduct
universe u v
namespace ConductorSquare
variable {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B]
variable (𝔠 : Ideal B)
section conductor
variable {𝔠}
variable (h𝔠 : ∀ b ∈ 𝔠, b ∈ Set.range (algebraMap A B))
include h𝔠
variable [FaithfulSMul A B]

Lean source · statement

def boundaryEquiv (u : (B ⧸ 𝔠)ˣ) :
    (boundary h𝔠 u : CommRing.Pic A) ≃ₗ[A] ↥(glueSubmodule (A := A) 𝔠 (u : B ⧸ 𝔠))

theorem

glueSubmodule_eq_span_of_eq

L204 ↗

AlgebraicCurves.Geometry.Picard.Proofs.CommRing_Pic_exists_boundaryHom_conductorSquare_exact.ConductorSquare.glueSubmodule_eq_span_of_eq

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace CommRing_Pic_exists_boundaryHom_conductorSquare_exact
open TensorProduct
universe u v
namespace ConductorSquare
variable {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B]
variable (𝔠 : Ideal B)
section conductor
variable {𝔠}
variable (h𝔠 : ∀ b ∈ 𝔠, b ∈ Set.range (algebraMap A B))
include h𝔠
variable [FaithfulSMul A B]
local notation "𝔠A" => Ideal.comap (algebraMap A B) 𝔠
omit [FaithfulSMul A B] in

Lean source · statement

theorem glueSubmodule_eq_span_of_eq (u : B ⧸ 𝔠) (s : Bˣ) (a : (A ⧸ 𝔠A)ˣ)
    (hu : u = Ideal.quotientMap 𝔠 (algebraMap A B) le_rfl (a : A ⧸ 𝔠A) *
      Ideal.Quotient.mk 𝔠 (s : B)) :
    glueSubmodule (A := A) 𝔠 u = Submodule.span A {((s⁻¹ : Bˣ) : B)}

theorem

boundary_eq_one_iff

L233 ↗

AlgebraicCurves.Geometry.Picard.Proofs.CommRing_Pic_exists_boundaryHom_conductorSquare_exact.ConductorSquare.boundary_eq_one_iff

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace CommRing_Pic_exists_boundaryHom_conductorSquare_exact
open TensorProduct
universe u v
namespace ConductorSquare
variable {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B]
variable (𝔠 : Ideal B)
section conductor
variable {𝔠}
variable (h𝔠 : ∀ b ∈ 𝔠, b ∈ Set.range (algebraMap A B))
include h𝔠
variable [FaithfulSMul A B]
local notation "𝔠A" => Ideal.comap (algebraMap A B) 𝔠

Lean source · statement

theorem boundary_eq_one_iff (u : (B ⧸ 𝔠)ˣ) :
    boundary h𝔠 u = 1 ↔
      ∃ (t : Bˣ) (a : (A ⧸ 𝔠A)ˣ),
        (u : B ⧸ 𝔠) = Ideal.quotientMap 𝔠 (algebraMap A B) le_rfl (a : A ⧸ 𝔠A) *
          Ideal.Quotient.mk 𝔠 (t : B)

theorem

exists_unit_eq

L269 ↗

AlgebraicCurves.Geometry.Picard.Proofs.CommRing_Pic_exists_boundaryHom_conductorSquare_exact.ConductorSquare.exists_unit_eq

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace CommRing_Pic_exists_boundaryHom_conductorSquare_exact
open TensorProduct
universe u v
namespace ConductorSquare
variable {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B]
variable (𝔠 : Ideal B)
section conductor
variable {𝔠}
variable (h𝔠 : ∀ b ∈ 𝔠, b ∈ Set.range (algebraMap A B))
include h𝔠
variable [FaithfulSMul A B]
local notation "𝔠A" => Ideal.comap (algebraMap A B) 𝔠
omit [FaithfulSMul A B] in

Lean source · statement

theorem exists_unit_eq (hinj : Function.Injective (algebraMap A B)) (t : Bˣ) (a : (A ⧸ 𝔠A)ˣ)
    (h : Ideal.Quotient.mk 𝔠 (t : B) =
      Ideal.quotientMap 𝔠 (algebraMap A B) le_rfl (a : A ⧸ 𝔠A)) :
    ∃ s : Aˣ, algebraMap A B s = t

theorem

mapAlgebra_boundary

L293 ↗

AlgebraicCurves.Geometry.Picard.Proofs.CommRing_Pic_exists_boundaryHom_conductorSquare_exact.ConductorSquare.mapAlgebra_boundary

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace CommRing_Pic_exists_boundaryHom_conductorSquare_exact
open TensorProduct
universe u v
namespace ConductorSquare
variable {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B]
variable (𝔠 : Ideal B)
section conductor
variable {𝔠}
variable (h𝔠 : ∀ b ∈ 𝔠, b ∈ Set.range (algebraMap A B))
include h𝔠
variable [FaithfulSMul A B]
local notation "𝔠A" => Ideal.comap (algebraMap A B) 𝔠

Lean source · statement

theorem mapAlgebra_boundary (u : (B ⧸ 𝔠)ˣ) :
    CommRing.Pic.mapAlgebra A B (boundary h𝔠 u) = 1

theorem

exists_of_coe_glueSubmodule

L299 ↗

AlgebraicCurves.Geometry.Picard.Proofs.CommRing_Pic_exists_boundaryHom_conductorSquare_exact.ConductorSquare.exists_of_coe_glueSubmodule

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace CommRing_Pic_exists_boundaryHom_conductorSquare_exact
open TensorProduct
universe u v
namespace ConductorSquare
variable {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B]
variable (𝔠 : Ideal B)
section conductor
variable {𝔠}
variable (h𝔠 : ∀ b ∈ 𝔠, b ∈ Set.range (algebraMap A B))
include h𝔠
variable [FaithfulSMul A B]
local notation "𝔠A" => Ideal.comap (algebraMap A B) 𝔠
omit [FaithfulSMul A B] h𝔠 in

Lean source · statement

theorem exists_of_coe_glueSubmodule (u : B ⧸ 𝔠) (x : ↥(glueSubmodule (A := A) 𝔠 u)) :
    ∃ a : A, u * Ideal.Quotient.mk 𝔠 (x : B) = Ideal.Quotient.mk 𝔠 (algebraMap A B a)

def

glueValueFun

L304 ↗

AlgebraicCurves.Geometry.Picard.Proofs.CommRing_Pic_exists_boundaryHom_conductorSquare_exact.ConductorSquare.glueValueFun

Documentation

The residue class in the base ring attached to an element of the gluing submodule.

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace CommRing_Pic_exists_boundaryHom_conductorSquare_exact
open TensorProduct
universe u v
namespace ConductorSquare
variable {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B]
variable (𝔠 : Ideal B)
section conductor
variable {𝔠}
variable (h𝔠 : ∀ b ∈ 𝔠, b ∈ Set.range (algebraMap A B))
include h𝔠
variable [FaithfulSMul A B]
local notation "𝔠A" => Ideal.comap (algebraMap A B) 𝔠
omit [FaithfulSMul A B] h𝔠 in

Lean source · statement

def glueValueFun (u : B ⧸ 𝔠) (x : ↥(glueSubmodule (A := A) 𝔠 u)) : A ⧸ 𝔠A

theorem

quotientMap_glueValueFun

L307 ↗

AlgebraicCurves.Geometry.Picard.Proofs.CommRing_Pic_exists_boundaryHom_conductorSquare_exact.ConductorSquare.quotientMap_glueValueFun

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace CommRing_Pic_exists_boundaryHom_conductorSquare_exact
open TensorProduct
universe u v
namespace ConductorSquare
variable {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B]
variable (𝔠 : Ideal B)
section conductor
variable {𝔠}
variable (h𝔠 : ∀ b ∈ 𝔠, b ∈ Set.range (algebraMap A B))
include h𝔠
variable [FaithfulSMul A B]
local notation "𝔠A" => Ideal.comap (algebraMap A B) 𝔠
omit [FaithfulSMul A B] h𝔠 in

Lean source · statement

theorem quotientMap_glueValueFun (u : B ⧸ 𝔠) (x : ↥(glueSubmodule (A := A) 𝔠 u)) :
    Ideal.quotientMap 𝔠 (algebraMap A B) le_rfl (glueValueFun u x) =
      u * Ideal.Quotient.mk 𝔠 (x : B)

def

glueValue

L314 ↗

AlgebraicCurves.Geometry.Picard.Proofs.CommRing_Pic_exists_boundaryHom_conductorSquare_exact.ConductorSquare.glueValue

Documentation

The linear residue map from the gluing submodule to the quotient of the base ring.

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace CommRing_Pic_exists_boundaryHom_conductorSquare_exact
open TensorProduct
universe u v
namespace ConductorSquare
variable {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B]
variable (𝔠 : Ideal B)
section conductor
variable {𝔠}
variable (h𝔠 : ∀ b ∈ 𝔠, b ∈ Set.range (algebraMap A B))
include h𝔠
variable [FaithfulSMul A B]
local notation "𝔠A" => Ideal.comap (algebraMap A B) 𝔠
omit [FaithfulSMul A B] h𝔠 in

Lean source · full declaration

def glueValue (u : (B ⧸ 𝔠)ˣ) :
    ↥(glueSubmodule (A := A) 𝔠 (u : B ⧸ 𝔠)) →ₗ[A] (A ⧸ 𝔠A) where
  toFun := glueValueFun (u : B ⧸ 𝔠)
  map_add' x y := by
    apply Ideal.quotientMap_injective (I := 𝔠) (f := algebraMap A B)
    rw [map_add, quotientMap_glueValueFun, quotientMap_glueValueFun, quotientMap_glueValueFun,
      Submodule.coe_add, map_add, mul_add]
  map_smul' r x := by
    apply Ideal.quotientMap_injective (I := 𝔠) (f := algebraMap A B)
    rw [RingHom.id_apply, quotientMap_glueValueFun, Algebra.smul_def, Ideal.Quotient.algebraMap_eq,
      map_mul, Ideal.quotientMap_mk, quotientMap_glueValueFun, Submodule.coe_smul, Algebra.smul_def,
      map_mul, mul_left_comm]

theorem

quotientMap_glueValue

L327 ↗

AlgebraicCurves.Geometry.Picard.Proofs.CommRing_Pic_exists_boundaryHom_conductorSquare_exact.ConductorSquare.quotientMap_glueValue

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace CommRing_Pic_exists_boundaryHom_conductorSquare_exact
open TensorProduct
universe u v
namespace ConductorSquare
variable {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B]
variable (𝔠 : Ideal B)
section conductor
variable {𝔠}
variable (h𝔠 : ∀ b ∈ 𝔠, b ∈ Set.range (algebraMap A B))
include h𝔠
variable [FaithfulSMul A B]
local notation "𝔠A" => Ideal.comap (algebraMap A B) 𝔠
omit [FaithfulSMul A B] h𝔠 in

Lean source · statement

theorem quotientMap_glueValue (u : (B ⧸ 𝔠)ˣ) (x : ↥(glueSubmodule (A := A) 𝔠 (u : B ⧸ 𝔠))) :
    Ideal.quotientMap 𝔠 (algebraMap A B) le_rfl (glueValue (A := A) u x) =
      (u : B ⧸ 𝔠) * Ideal.Quotient.mk 𝔠 (x : B)

theorem

mem_smul_top_of_mem

L332 ↗

AlgebraicCurves.Geometry.Picard.Proofs.CommRing_Pic_exists_boundaryHom_conductorSquare_exact.ConductorSquare.mem_smul_top_of_mem

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace CommRing_Pic_exists_boundaryHom_conductorSquare_exact
open TensorProduct
universe u v
namespace ConductorSquare
variable {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B]
variable (𝔠 : Ideal B)
section conductor
variable {𝔠}
variable (h𝔠 : ∀ b ∈ 𝔠, b ∈ Set.range (algebraMap A B))
include h𝔠
variable [FaithfulSMul A B]
local notation "𝔠A" => Ideal.comap (algebraMap A B) 𝔠
omit [FaithfulSMul A B] in

Lean source · statement

theorem mem_smul_top_of_mem (u : (B ⧸ 𝔠)ˣ) (x : ↥(glueSubmodule (A := A) 𝔠 (u : B ⧸ 𝔠)))
    (hx : (x : B) ∈ 𝔠) :
    x ∈ (𝔠A) • (⊤ : Submodule A ↥(glueSubmodule (A := A) 𝔠 (u : B ⧸ 𝔠)))

theorem

bijective_liftBaseChange_glueValue

L358 ↗

AlgebraicCurves.Geometry.Picard.Proofs.CommRing_Pic_exists_boundaryHom_conductorSquare_exact.ConductorSquare.bijective_liftBaseChange_glueValue

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace CommRing_Pic_exists_boundaryHom_conductorSquare_exact
open TensorProduct
universe u v
namespace ConductorSquare
variable {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B]
variable (𝔠 : Ideal B)
section conductor
variable {𝔠}
variable (h𝔠 : ∀ b ∈ 𝔠, b ∈ Set.range (algebraMap A B))
include h𝔠
variable [FaithfulSMul A B]
local notation "𝔠A" => Ideal.comap (algebraMap A B) 𝔠
omit [FaithfulSMul A B] in

Lean source · statement

theorem bijective_liftBaseChange_glueValue (u : (B ⧸ 𝔠)ˣ) :
    Function.Bijective ((glueValue (A := A) u).liftBaseChange (A ⧸ 𝔠A))

theorem

mapAlgebra_quotient_boundary

L394 ↗

AlgebraicCurves.Geometry.Picard.Proofs.CommRing_Pic_exists_boundaryHom_conductorSquare_exact.ConductorSquare.mapAlgebra_quotient_boundary

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace CommRing_Pic_exists_boundaryHom_conductorSquare_exact
open TensorProduct
universe u v
namespace ConductorSquare
variable {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B]
variable (𝔠 : Ideal B)
section conductor
variable {𝔠}
variable (h𝔠 : ∀ b ∈ 𝔠, b ∈ Set.range (algebraMap A B))
include h𝔠
variable [FaithfulSMul A B]
local notation "𝔠A" => Ideal.comap (algebraMap A B) 𝔠

Lean source · statement

theorem mapAlgebra_quotient_boundary (u : (B ⧸ 𝔠)ˣ) :
    CommRing.Pic.mapAlgebra A (A ⧸ 𝔠A) (boundary h𝔠 u) = 1

theorem

exists_glueSubmodule_eq

L400 ↗

AlgebraicCurves.Geometry.Picard.Proofs.CommRing_Pic_exists_boundaryHom_conductorSquare_exact.ConductorSquare.exists_glueSubmodule_eq

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace CommRing_Pic_exists_boundaryHom_conductorSquare_exact
open TensorProduct
universe u v
namespace ConductorSquare
variable {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B]
variable (𝔠 : Ideal B)
section conductor
variable {𝔠}
variable (h𝔠 : ∀ b ∈ 𝔠, b ∈ Set.range (algebraMap A B))
include h𝔠
variable [FaithfulSMul A B]
local notation "𝔠A" => Ideal.comap (algebraMap A B) 𝔠
omit [FaithfulSMul A B] in

Lean source · statement

theorem exists_glueSubmodule_eq (J : Submodule A B) (hJB : ⊤ * J = ⊤)
    (hfree : Nonempty ((A ⧸ 𝔠A) ⊗[A] ↥J ≃ₗ[A ⧸ 𝔠A] (A ⧸ 𝔠A))) :
    ∃ u : (B ⧸ 𝔠)ˣ, glueSubmodule (A := A) 𝔠 (u : B ⧸ 𝔠) = J

theorem

exists_boundary_eq

L476 ↗

AlgebraicCurves.Geometry.Picard.Proofs.CommRing_Pic_exists_boundaryHom_conductorSquare_exact.ConductorSquare.exists_boundary_eq

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace CommRing_Pic_exists_boundaryHom_conductorSquare_exact
open TensorProduct
universe u v
namespace ConductorSquare
variable {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B]
variable (𝔠 : Ideal B)
section conductor
variable {𝔠}
variable (h𝔠 : ∀ b ∈ 𝔠, b ∈ Set.range (algebraMap A B))
include h𝔠
variable [FaithfulSMul A B]
local notation "𝔠A" => Ideal.comap (algebraMap A B) 𝔠

Lean source · statement

theorem exists_boundary_eq (P : CommRing.Pic A) (hB : CommRing.Pic.mapAlgebra A B P = 1)
    (hA : CommRing.Pic.mapAlgebra A (A ⧸ 𝔠A) P = 1) : ∃ u, boundary h𝔠 u = P

theorem

exists_boundaryHom_conductorSquare_exact

L498 ↗

CommRing.Pic.exists_boundaryHom_conductorSquare_exact

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace CommRing_Pic_exists_boundaryHom_conductorSquare_exact
open TensorProduct
universe u v
attribute [local simp] ConductorSquare.val_glueUnits
open ConductorSquare in

Lean source · statement

theorem _root_.CommRing.Pic.exists_boundaryHom_conductorSquare_exact
    {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B] [FaithfulSMul A B]
    (𝔠 : Ideal B) (h𝔠 : ∀ b ∈ 𝔠, b ∈ Set.range (algebraMap A B)) :
    ∃ δ : (B ⧸ 𝔠)ˣ →* CommRing.Pic A,
      (∀ u : (B ⧸ 𝔠)ˣ, ∃ I : Submodule A B,
        (∀ x : B, x ∈ I ↔ ∃ a : A,
          (u : B ⧸ 𝔠) * Ideal.Quotient.mk 𝔠 x = Ideal.Quotient.mk 𝔠 (algebraMap A B a)) ∧
        Nonempty ((δ u : CommRing.Pic A) ≃ₗ[A] ↥I)) ∧
      (∀ u : (B ⧸ 𝔠)ˣ, δ u = 1 ↔
        ∃ (t : Bˣ) (a : (A ⧸ 𝔠.comap (algebraMap A B))ˣ),
          (u : B ⧸ 𝔠) =
            Ideal.quotientMap 𝔠 (algebraMap A B) le_rfl (a : A ⧸ 𝔠.comap (algebraMap A B)) *
              Ideal.Quotient.mk 𝔠 (t : B)) ∧
      (∀ P : CommRing.Pic A, (∃ u, δ u = P) ↔
        CommRing.Pic.mapAlgebra A B P = 1 ∧
          CommRing.Pic.mapAlgebra A (A ⧸ 𝔠.comap (algebraMap A B)) P = 1) ∧
      (∀ (t : Bˣ) (a : (A ⧸ 𝔠.comap (algebraMap A B))ˣ),
        Ideal.Quotient.mk 𝔠 (t : B) =
            Ideal.quotientMap 𝔠 (algebraMap A B) le_rfl (a : A ⧸ 𝔠.comap (algebraMap A B)) →
          ∃ s : Aˣ, algebraMap A B s = t)

Module documentation

Comm Ring Pic exists boundary Hom conductor Square exact

Declarations