NYLL
Module

TwoChartCechLaurentChart.lean

Nyll.AlgebraicCurves.Cohomology.Cech.TwoChartCechLaurentChart
39 declarations indexed from sourceView source ↗

Module documentation

Two Chart Cech Laurent Chart

Imports5
Imported by8

Declarations

theorem

derivative_coeff

L31 ↗
LaurentSeries.derivative_coeff
Source context 4 commands

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

noncomputable section
universe u v
namespace LaurentSeries
variable (R : Type*) [CommRing R]
Lean source · statement
theorem derivative_coeff (x : LaurentSeries R) (n : ℤ) :
    (derivative R x).coeff n = (n + 1) • x.coeff (n + 1)
theorem

derivative_single_one_mul

L35 ↗
LaurentSeries.derivative_single_one_mul
Source context 4 commands

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

noncomputable section
universe u v
namespace LaurentSeries
variable (R : Type*) [CommRing R]
Lean source · statement
theorem derivative_single_one_mul (n : ℤ) (x : LaurentSeries R) :
    derivative R (HahnSeries.single n (1 : R) * x) =
      HahnSeries.single (n - 1) (n : R) * x + HahnSeries.single n (1 : R) * derivative R x
theorem

coeff_ofPowerSeries_of_neg

L45 ↗
LaurentSeries.coeff_ofPowerSeries_of_neg
Source context 4 commands

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

noncomputable section
universe u v
namespace LaurentSeries
variable (R : Type*) [CommRing R]
Lean source · statement
theorem coeff_ofPowerSeries_of_neg (p : PowerSeries R) {m : ℤ} (hm : m < 0) :
    (HahnSeries.ofPowerSeries ℤ R p).coeff m = 0
theorem

derivative_ofPowerSeries

L53 ↗
LaurentSeries.derivative_ofPowerSeries
Source context 4 commands

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

noncomputable section
universe u v
namespace LaurentSeries
variable (R : Type*) [CommRing R]
Lean source · statement
theorem derivative_ofPowerSeries (p : PowerSeries R) :
    derivative R (HahnSeries.ofPowerSeries ℤ R p) =
      HahnSeries.ofPowerSeries ℤ R (PowerSeries.derivative p)
theorem

derivative_mul_def

L69 ↗
LaurentSeries.derivative_mul_def
Source context 4 commands

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

noncomputable section
universe u v
namespace LaurentSeries
variable (R : Type*) [CommRing R]
Lean source · statement
theorem derivative_mul_def (x y : LaurentSeries R) :
    derivative R (x * y) = x * derivative R y + derivative R x * y
def

residue

L100 ↗
LaurentSeries.residue
Documentation

The residue of a Laurent series, given by its coefficient of exponent -1.

Source context 4 commands

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

noncomputable section
universe u v
namespace LaurentSeries
variable (R : Type*) [CommRing R]
Lean source · statement
def residue : LaurentSeries R →ₗ[R] R
theorem

residue_apply

L102 ↗
LaurentSeries.residue_apply
Source context 4 commands

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

noncomputable section
universe u v
namespace LaurentSeries
variable (R : Type*) [CommRing R]
Lean source · statement
theorem residue_apply (x : LaurentSeries R) : residue R x = x.coeff (-1)
theorem

residue_ofPowerSeries

L104 ↗
LaurentSeries.residue_ofPowerSeries
Source context 4 commands

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

noncomputable section
universe u v
namespace LaurentSeries
variable (R : Type*) [CommRing R]
Lean source · statement
theorem residue_ofPowerSeries (p : PowerSeries R) : residue R (HahnSeries.ofPowerSeries ℤ R p) =
  0
theorem

residue_ofPowerSeries_mul_derivative_ofPowerSeries

L108 ↗
LaurentSeries.residue_ofPowerSeries_mul_derivative_ofPowerSeries
Source context 4 commands

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

noncomputable section
universe u v
namespace LaurentSeries
variable (R : Type*) [CommRing R]
Lean source · statement
theorem residue_ofPowerSeries_mul_derivative_ofPowerSeries (p q : PowerSeries R) :
    residue R (HahnSeries.ofPowerSeries ℤ R p * derivative R (HahnSeries.ofPowerSeries ℤ R q)) =
      0
theorem

residue_single_neg_one_mul_derivative_single_one

L113 ↗
LaurentSeries.residue_single_neg_one_mul_derivative_single_one
Source context 4 commands

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

noncomputable section
universe u v
namespace LaurentSeries
variable (R : Type*) [CommRing R]
Lean source · statement
theorem residue_single_neg_one_mul_derivative_single_one :
    residue R (HahnSeries.single (-1) (1 : R) * derivative R (HahnSeries.single 1 (1 : R))) = 1
theorem

map_derivative

L120 ↗
LaurentSeries.map_derivative
Source context 4 commands

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

noncomputable section
universe u v
namespace LaurentSeries
variable (R : Type*) [CommRing R]
Lean source · statement
theorem map_derivative {S : Type*} [CommRing S] (τ : R →+* S) (x : LaurentSeries R) :
    (derivative R x).map τ = derivative S (x.map τ)
theorem

residue_map

L125 ↗
LaurentSeries.residue_map
Source context 4 commands

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

noncomputable section
universe u v
namespace LaurentSeries
variable (R : Type*) [CommRing R]
Lean source · statement
theorem residue_map {S : Type*} [CommRing S] (τ : R →+* S) (x : LaurentSeries R) :
    residue S (x.map τ) = τ (residue R x)
structure

LaurentChart

L136 ↗
TwoChartCech.Cover.LaurentChart
Documentation

A Laurent-series expansion of the overlap ring compatible with the base-ring algebra map.

Source context 4 commands

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

noncomputable section
universe u v
namespace TwoChartCech.Cover
variable {R : Type u} [CommRing R]
Lean source · full declaration
structure LaurentChart (𝒰 : Cover.{u, v} R) where
  /-- The ring homomorphism expanding elements of the overlap ring as Laurent series. -/
  expand : 𝒰.A01 →+* LaurentSeries R
  /-- Base-ring scalars expand as constant Laurent series. -/
  expand_algebraMap : ∀ r : R, expand (algebraMap R 𝒰.A01 r) = HahnSeries.C r
abbrev

expandModule

L147 ↗
TwoChartCech.Cover.LaurentChart.expandModule
Documentation

The action of the overlap ring on Laurent series through the expansion homomorphism.

Source context 6 commands

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

noncomputable section
universe u v
namespace TwoChartCech.Cover
variable {R : Type u} [CommRing R]
namespace LaurentChart
variable {𝒰 : Cover.{u, v} R} (Λ : 𝒰.LaurentChart)
Lean source · statement
abbrev expandModule : Module 𝒰.A01 (LaurentSeries R)
theorem

expand_smul

L149 ↗
TwoChartCech.Cover.LaurentChart.expand_smul
Source context 6 commands

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

noncomputable section
universe u v
namespace TwoChartCech.Cover
variable {R : Type u} [CommRing R]
namespace LaurentChart
variable {𝒰 : Cover.{u, v} R} (Λ : 𝒰.LaurentChart)
Lean source · statement
theorem expand_smul (r : R) (a : 𝒰.A01) : Λ.expand (r • a) = r • Λ.expand a
theorem

isScalarTower_expandModule

L152 ↗
TwoChartCech.Cover.LaurentChart.isScalarTower_expandModule
Source context 6 commands

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

noncomputable section
universe u v
namespace TwoChartCech.Cover
variable {R : Type u} [CommRing R]
namespace LaurentChart
variable {𝒰 : Cover.{u, v} R} (Λ : 𝒰.LaurentChart)
Lean source · full declaration
theorem isScalarTower_expandModule :
    letI := Λ.expandModule
    IsScalarTower R 𝒰.A01 (LaurentSeries R) :=
  letI := Λ.expandModule
  ⟨fun r a x => by
    change Λ.expand (r • a) * x = r • (Λ.expand a * x)
    rw [expand_smul, ← HahnSeries.C_mul_eq_smul, ← HahnSeries.C_mul_eq_smul, mul_assoc]⟩
def

expandLinear

L161 ↗
TwoChartCech.Cover.LaurentChart.expandLinear
Documentation

The expansion homomorphism viewed as an R-linear map.

Source context 6 commands

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

noncomputable section
universe u v
namespace TwoChartCech.Cover
variable {R : Type u} [CommRing R]
namespace LaurentChart
variable {𝒰 : Cover.{u, v} R} (Λ : 𝒰.LaurentChart)
Lean source · full declaration
def expandLinear : 𝒰.A01 →ₗ[R] LaurentSeries R where
  toFun := Λ.expand
  map_add' := map_add _
  map_smul' := Λ.expand_smul
theorem

expandLinear_apply

L166 ↗
TwoChartCech.Cover.LaurentChart.expandLinear_apply
Source context 6 commands

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

noncomputable section
universe u v
namespace TwoChartCech.Cover
variable {R : Type u} [CommRing R]
namespace LaurentChart
variable {𝒰 : Cover.{u, v} R} (Λ : 𝒰.LaurentChart)
Lean source · statement
theorem expandLinear_apply (a : 𝒰.A01) : Λ.expandLinear a = Λ.expand a
def

expandDerivation

L169 ↗
TwoChartCech.Cover.LaurentChart.expandDerivation
Documentation

Differentiate the Laurent expansion to obtain a derivation of the overlap ring.

Source context 6 commands

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

noncomputable section
universe u v
namespace TwoChartCech.Cover
variable {R : Type u} [CommRing R]
namespace LaurentChart
variable {𝒰 : Cover.{u, v} R} (Λ : 𝒰.LaurentChart)
Lean source · full declaration
def expandDerivation :
    letI := Λ.expandModule
    Derivation R 𝒰.A01 (LaurentSeries R) :=
  letI := Λ.expandModule
  Derivation.mk' (LaurentSeries.derivative R ∘ₗ Λ.expandLinear) fun f g => by
    change LaurentSeries.derivative R (Λ.expand (f * g)) =
      Λ.expand f * LaurentSeries.derivative R (Λ.expand g) + Λ.expand g *
        LaurentSeries.derivative R (Λ.expand f)
    rw [map_mul, LaurentSeries.derivative_mul_def, mul_comm (LaurentSeries.derivative R
      (Λ.expand f))]
theorem

expandDerivation_apply

L180 ↗
TwoChartCech.Cover.LaurentChart.expandDerivation_apply
Source context 6 commands

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

noncomputable section
universe u v
namespace TwoChartCech.Cover
variable {R : Type u} [CommRing R]
namespace LaurentChart
variable {𝒰 : Cover.{u, v} R} (Λ : 𝒰.LaurentChart)
Lean source · full declaration
theorem expandDerivation_apply (f : 𝒰.A01) :
    letI := Λ.expandModule
    Λ.expandDerivation f = LaurentSeries.derivative R (Λ.expand f) := rfl
def

expandKaehler

L185 ↗
TwoChartCech.Cover.LaurentChart.expandKaehler
Documentation

The linear map on Kaehler differentials induced by differentiating Laurent expansions.

Source context 6 commands

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

noncomputable section
universe u v
namespace TwoChartCech.Cover
variable {R : Type u} [CommRing R]
namespace LaurentChart
variable {𝒰 : Cover.{u, v} R} (Λ : 𝒰.LaurentChart)
Lean source · full declaration
def expandKaehler :
    letI := Λ.expandModule
    Ω[𝒰.A01⁄R] →ₗ[𝒰.A01] LaurentSeries R :=
  letI := Λ.expandModule
  haveI := Λ.isScalarTower_expandModule
  Λ.expandDerivation.liftKaehlerDifferential
theorem

expandKaehler_smul_D

L192 ↗
TwoChartCech.Cover.LaurentChart.expandKaehler_smul_D
Source context 6 commands

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

noncomputable section
universe u v
namespace TwoChartCech.Cover
variable {R : Type u} [CommRing R]
namespace LaurentChart
variable {𝒰 : Cover.{u, v} R} (Λ : 𝒰.LaurentChart)
Lean source · full declaration
theorem expandKaehler_smul_D (f g : 𝒰.A01) :
    letI := Λ.expandModule
    Λ.expandKaehler (f • KaehlerDifferential.D R 𝒰.A01 g) = Λ.expand f *
      LaurentSeries.derivative R (Λ.expand g) := by
  let := Λ.expandModule
  have := Λ.isScalarTower_expandModule
  change Λ.expandDerivation.liftKaehlerDifferential (f • KaehlerDifferential.D R 𝒰.A01 g) = _
  rw [LinearMap.map_smul, Derivation.liftKaehlerDifferential_comp_D]
  rfl
theorem

expandKaehler_D

L202 ↗
TwoChartCech.Cover.LaurentChart.expandKaehler_D
Source context 6 commands

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

noncomputable section
universe u v
namespace TwoChartCech.Cover
variable {R : Type u} [CommRing R]
namespace LaurentChart
variable {𝒰 : Cover.{u, v} R} (Λ : 𝒰.LaurentChart)
Lean source · full declaration
theorem expandKaehler_D (g : 𝒰.A01) :
    letI := Λ.expandModule
    Λ.expandKaehler (KaehlerDifferential.D R 𝒰.A01 g) = LaurentSeries.derivative R (Λ.expand g)
      := by
  let := Λ.expandModule
  have := Λ.isScalarTower_expandModule
  exact Λ.expandDerivation.liftKaehlerDifferential_comp_D g
def

residue

L212 ↗
TwoChartCech.Cover.LaurentChart.residue
Documentation

The residue of a Kaehler differential, extracted from the coefficient of exponent -1 of its expansion.

Source context 6 commands

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

noncomputable section
universe u v
namespace TwoChartCech.Cover
variable {R : Type u} [CommRing R]
namespace LaurentChart
variable {𝒰 : Cover.{u, v} R} (Λ : 𝒰.LaurentChart)
Lean source · full declaration
def residue : Ω[𝒰.A01⁄R] →ₗ[R] R where
  toFun ω := letI := Λ.expandModule; LaurentSeries.residue R (Λ.expandKaehler ω)
  map_add' ω ω' := by
    let := Λ.expandModule
    change LaurentSeries.residue R (Λ.expandKaehler (ω + ω')) = _
    rw [map_add, map_add]
  map_smul' r ω := by
    let := Λ.expandModule
    have := Λ.isScalarTower_expandModule
    change LaurentSeries.residue R (Λ.expandKaehler (r • ω)) = r • LaurentSeries.residue R
      (Λ.expandKaehler ω)
    have h1 : Λ.expandKaehler (r • ω) = r • Λ.expandKaehler ω := by
      rw [← IsScalarTower.algebraMap_smul 𝒰.A01 r ω, LinearMap.map_smul]
      change Λ.expand (algebraMap R 𝒰.A01 r) * Λ.expandKaehler ω = _
      rw [expand_algebraMap, HahnSeries.C_mul_eq_smul]
    rw [h1, map_smul]
theorem

residue_apply

L229 ↗
TwoChartCech.Cover.LaurentChart.residue_apply
Source context 6 commands

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

noncomputable section
universe u v
namespace TwoChartCech.Cover
variable {R : Type u} [CommRing R]
namespace LaurentChart
variable {𝒰 : Cover.{u, v} R} (Λ : 𝒰.LaurentChart)
Lean source · full declaration
theorem residue_apply (ω : Ω[𝒰.A01⁄R]) :
    letI := Λ.expandModule
    Λ.residue ω = (Λ.expandKaehler ω).coeff (-1) := rfl
theorem

residue_smul_D

L233 ↗
TwoChartCech.Cover.LaurentChart.residue_smul_D
Source context 6 commands

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

noncomputable section
universe u v
namespace TwoChartCech.Cover
variable {R : Type u} [CommRing R]
namespace LaurentChart
variable {𝒰 : Cover.{u, v} R} (Λ : 𝒰.LaurentChart)
Lean source · statement
theorem residue_smul_D (f g : 𝒰.A01) :
    Λ.residue (f • KaehlerDifferential.D R 𝒰.A01 g) =
      (Λ.expand f * LaurentSeries.derivative R (Λ.expand g)).coeff (-1)
theorem

residue_D

L238 ↗
TwoChartCech.Cover.LaurentChart.residue_D
Source context 6 commands

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

noncomputable section
universe u v
namespace TwoChartCech.Cover
variable {R : Type u} [CommRing R]
namespace LaurentChart
variable {𝒰 : Cover.{u, v} R} (Λ : 𝒰.LaurentChart)
Lean source · statement
theorem residue_D (g : 𝒰.A01) :
    Λ.residue (KaehlerDifferential.D R 𝒰.A01 g) = (LaurentSeries.derivative R (Λ.expand
      g)).coeff (-1)
def

IsRegular

L244 ↗
TwoChartCech.Cover.LaurentChart.IsRegular
Documentation

Every element from B expands as a power series under the map ρ.

Source context 6 commands

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

noncomputable section
universe u v
namespace TwoChartCech.Cover
variable {R : Type u} [CommRing R]
namespace LaurentChart
variable {𝒰 : Cover.{u, v} R} (Λ : 𝒰.LaurentChart)
Lean source · statement
def IsRegular {B : Type*} [CommRing B] [Algebra R B] (ρ : B →ₐ[R] 𝒰.A01) : Prop
theorem

exists_eq_ofPowerSeries

L247 ↗
TwoChartCech.Cover.LaurentChart.IsRegular.exists_eq_ofPowerSeries
Source context 6 commands

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

noncomputable section
universe u v
namespace TwoChartCech.Cover
variable {R : Type u} [CommRing R]
namespace LaurentChart
variable {𝒰 : Cover.{u, v} R} (Λ : 𝒰.LaurentChart)
Lean source · statement
theorem IsRegular.exists_eq_ofPowerSeries {B : Type*} [CommRing B] [Algebra R B] {ρ : B →ₐ[R] 𝒰.A01}
    (h : Λ.IsRegular ρ) (b : B) : ∃ p : PowerSeries R, HahnSeries.ofPowerSeries ℤ R p = Λ.expand
      (ρ b)
def

HasParameter

L253 ↗
TwoChartCech.Cover.LaurentChart.HasParameter
Documentation

Some element from B expands as the Laurent monomial of exponent 1 with coefficient 1.

Source context 6 commands

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

noncomputable section
universe u v
namespace TwoChartCech.Cover
variable {R : Type u} [CommRing R]
namespace LaurentChart
variable {𝒰 : Cover.{u, v} R} (Λ : 𝒰.LaurentChart)
Lean source · statement
def HasParameter {B : Type*} [CommRing B] [Algebra R B] (ρ : B →ₐ[R] 𝒰.A01) : Prop
def

formalDisc

L260 ↗
TwoChartCech.Cover.formalDisc
Documentation

The two-chart cover with Laurent-series rings on the overlap and first chart, and a power-series ring on the second chart.

Source context 4 commands

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

noncomputable section
universe u v
namespace TwoChartCech.Cover
variable {R : Type u} [CommRing R]
Lean source · statement
def formalDisc (R : Type u) [CommRing R] : Cover.{u, u} R
def

formalDiscChart

L273 ↗
TwoChartCech.Cover.formalDiscChart
Documentation

The Laurent chart on formalDisc R with identity expansion on the overlap ring.

Source context 4 commands

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

noncomputable section
universe u v
namespace TwoChartCech.Cover
variable {R : Type u} [CommRing R]
Lean source · full declaration
def formalDiscChart (R : Type u) [CommRing R] : (formalDisc R).LaurentChart where
  expand := RingHom.id _
  expand_algebraMap _ := rfl
theorem

formalDiscChart_isRegular

L277 ↗
TwoChartCech.Cover.formalDiscChart_isRegular
Source context 4 commands

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

noncomputable section
universe u v
namespace TwoChartCech.Cover
variable {R : Type u} [CommRing R]
Lean source · statement
theorem formalDiscChart_isRegular (R : Type u) [CommRing R] : (formalDiscChart R).IsRegular
  (formalDisc R).ρ1
theorem

formalDiscChart_hasParameter

L281 ↗
TwoChartCech.Cover.formalDiscChart_hasParameter
Source context 4 commands

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

noncomputable section
universe u v
namespace TwoChartCech.Cover
variable {R : Type u} [CommRing R]
Lean source · statement
theorem formalDiscChart_hasParameter (R : Type u) [CommRing R] :
    (formalDiscChart R).HasParameter (formalDisc R).ρ1
theorem

formalDiscChart_residue_tinv_dt

L287 ↗
TwoChartCech.Cover.formalDiscChart_residue_tinv_dt
Source context 4 commands

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

noncomputable section
universe u v
namespace TwoChartCech.Cover
variable {R : Type u} [CommRing R]
Lean source · statement
theorem formalDiscChart_residue_tinv_dt (R : Type u) [CommRing R] (f g : (formalDisc R).A01)
    (hf : f = HahnSeries.single (-1) (1 : R)) (hg : g = HahnSeries.single 1 (1 : R)) :
    (formalDiscChart R).residue (f • KaehlerDifferential.D R (formalDisc R).A01 g) = 1
structure

IsCompletionAlong

L302 ↗
TwoChartCech.Cover.LaurentChart.IsCompletionAlong
Documentation

A regular Laurent expansion whose finite jets lift from B and whose vanishing jets detect powers of the kernel of e.

Source context 4 commands

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

noncomputable section
universe u v
namespace TwoChartCech.Cover.LaurentChart
variable {R : Type u} [CommRing R] {𝒰 : Cover.{u, v} R}
Lean source · full declaration
structure IsCompletionAlong (Λ : 𝒰.LaurentChart) {B : Type*} [CommRing B] [Algebra R B]
    (ρ : B →ₐ[R] 𝒰.A01) (e : B →ₐ[R] R) : Prop where
  /-- The Laurent expansion is regular along `ρ`. -/
  isRegular : Λ.IsRegular ρ
  /-- Every finite list of coefficients of a power series is realized by the expansion of an
  element of `B`. -/
  exists_coeff_eq : ∀ (n : ℕ) (p : PowerSeries R), ∃ b : B,
    ∀ k : ℕ, k < n → (Λ.expand (ρ b)).coeff (k : ℤ) = PowerSeries.coeff k p
  /-- Vanishing of the first `n` coefficients is equivalent to membership in the `n`th power of
  the kernel of `e`. -/
  forall_coeff_eq_zero_iff : ∀ (n : ℕ) (b : B),
    (∀ k : ℕ, k < n → (Λ.expand (ρ b)).coeff (k : ℤ) = 0) ↔ b ∈ RingHom.ker e.toRingHom ^ n
theorem

forall_coeff_eq_zero_iff_mem_ker_constantCoeff_pow

L317 ↗
PowerSeries.forall_coeff_eq_zero_iff_mem_ker_constantCoeff_pow
Source context 2 commands

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

noncomputable section
universe u v
Lean source · statement
theorem PowerSeries.forall_coeff_eq_zero_iff_mem_ker_constantCoeff_pow (R : Type*) [CommRing R]
  (n : ℕ)
    (a : PowerSeries R) :
    (∀ k : ℕ, k < n → PowerSeries.coeff k a = 0) ↔ a ∈ RingHom.ker (PowerSeries.constantCoeff (R
      := R)) ^ n
def

formalDiscPoint

L331 ↗
TwoChartCech.Cover.formalDiscPoint
Documentation

The algebra homomorphism from the power-series chart to R given by the constant coefficient.

Source context 3 commands

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

noncomputable section
universe u v
namespace TwoChartCech.Cover
Lean source · statement
def formalDiscPoint (R : Type u) [CommRing R] : (formalDisc R).A1 →ₐ[R] R
theorem

formalDiscChart_isCompletionAlong

L338 ↗
TwoChartCech.Cover.formalDiscChart_isCompletionAlong
Source context 3 commands

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

noncomputable section
universe u v
namespace TwoChartCech.Cover
Lean source · full declaration
theorem formalDiscChart_isCompletionAlong (R : Type u) [CommRing R] :
    (formalDiscChart R).IsCompletionAlong (formalDisc R).ρ1 (formalDiscPoint R) where
  isRegular := formalDiscChart_isRegular R
  exists_coeff_eq n p := ⟨p, fun k _ => HahnSeries.ofPowerSeries_apply_coeff p k⟩
  forall_coeff_eq_zero_iff n a := by
    refine Iff.trans ?_ (PowerSeries.forall_coeff_eq_zero_iff_mem_ker_constantCoeff_pow R n a)
    simp only [show ∀ b, (formalDiscChart R).expand ((formalDisc R).ρ1 b) =
      HahnSeries.ofPowerSeries ℤ R b from
      fun _ => rfl]
    constructor
    · intro h k hk
      exact (HahnSeries.ofPowerSeries_apply_coeff (Γ := ℤ) a k).symm.trans (h k hk)
    · intro h k hk
      exact (HahnSeries.ofPowerSeries_apply_coeff (Γ := ℤ) a k).trans (h k hk)

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