Module

SmoothLocus.lean

Nyll.SchemeTheory.Pi1.Morphisms.SmoothLocus

10 declarations indexed from sourceView source ↗

Module documentation

Smooth and locally standard smooth

Imports4

Mathlib.Algebra.Module.LocalizedModule.Basic
Mathlib.RingTheory.EssentialFiniteness
Mathlib.RingTheory.Localization.Away.AdjoinRoot
Mathlib.RingTheory.Smooth.Locus

Imported by1

Nyll.SchemeTheory.Pi1.Morphisms.All

lemma

subsingleton

L43 ↗

IsLocalizedModule.subsingleton

Source context 5 commands

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

@[expose] public section
universe w t u v
section Upstream
section
variable {R M M' : Type*} [CommRing R]
    (S : Submonoid R) [AddCommGroup M] [Module R M] [AddCommGroup M'] [Module R M'] (f : M →ₗ[R] M')

Lean source · statement

lemma IsLocalizedModule.subsingleton [IsLocalizedModule S f] (h : 0 ∈ S) :
    Subsingleton M'

lemma

map_injective_iff_localizedModule_map_injective

L57 ↗

IsLocalizedModule.map_injective_iff_localizedModule_map_injective

Source context 7 commands

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

@[expose] public section
universe w t u v
section Upstream
section
variable {R M M' : Type*} [CommRing R]
    (S : Submonoid R) [AddCommGroup M] [Module R M] [AddCommGroup M'] [Module R M'] (f : M →ₗ[R] M')
section
variable {R M N M' N' : Type*} [CommSemiring R] (S : Submonoid R)
  [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N]
  [AddCommMonoid M'] [Module R M'] [AddCommMonoid N'] [Module R N']
  (g₁ : M →ₗ[R] M') (g₂ : N →ₗ[R] N')

Lean source · statement

lemma IsLocalizedModule.map_injective_iff_localizedModule_map_injective
    [IsLocalizedModule S g₁] [IsLocalizedModule S g₂] (l : M →ₗ[R] N) :
    Function.Injective (IsLocalizedModule.map S g₁ g₂ l) ↔
      Function.Injective (LocalizedModule.map S l)

lemma

map_surjective_iff_localizedModule_map_surjective

L69 ↗

IsLocalizedModule.map_surjective_iff_localizedModule_map_surjective

Source context 7 commands

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

@[expose] public section
universe w t u v
section Upstream
section
variable {R M M' : Type*} [CommRing R]
    (S : Submonoid R) [AddCommGroup M] [Module R M] [AddCommGroup M'] [Module R M'] (f : M →ₗ[R] M')
section
variable {R M N M' N' : Type*} [CommSemiring R] (S : Submonoid R)
  [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N]
  [AddCommMonoid M'] [Module R M'] [AddCommMonoid N'] [Module R N']
  (g₁ : M →ₗ[R] M') (g₂ : N →ₗ[R] N')

Lean source · statement

lemma IsLocalizedModule.map_surjective_iff_localizedModule_map_surjective
    [IsLocalizedModule S g₁] [IsLocalizedModule S g₂] (l : M →ₗ[R] N) :
    Function.Surjective (IsLocalizedModule.map S g₁ g₂ l) ↔
      Function.Surjective (LocalizedModule.map S l)

lemma

map_bijective_iff_localizedModule_map_bijective

L81 ↗

IsLocalizedModule.map_bijective_iff_localizedModule_map_bijective

Source context 7 commands

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

@[expose] public section
universe w t u v
section Upstream
section
variable {R M M' : Type*} [CommRing R]
    (S : Submonoid R) [AddCommGroup M] [Module R M] [AddCommGroup M'] [Module R M'] (f : M →ₗ[R] M')
section
variable {R M N M' N' : Type*} [CommSemiring R] (S : Submonoid R)
  [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N]
  [AddCommMonoid M'] [Module R M'] [AddCommMonoid N'] [Module R N']
  (g₁ : M →ₗ[R] M') (g₂ : N →ₗ[R] N')

Lean source · statement

lemma IsLocalizedModule.map_bijective_iff_localizedModule_map_bijective
    [IsLocalizedModule S g₁] [IsLocalizedModule S g₂] (l : M →ₗ[R] N) :
    Function.Bijective (IsLocalizedModule.map S g₁ g₂ l) ↔
      Function.Bijective (LocalizedModule.map S l)

lemma

exists_basis_of_isLocalizedModule_powers

L128 ↗

Module.FinitePresentation.exists_basis_of_isLocalizedModule_powers

Source context 6 commands

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

@[expose] public section
universe w t u v
namespace Module
section
variable {R M : Type*} [CommRing R] [AddCommGroup M] [Module R M]
    (S : Submonoid R)
    {M' : Type*} [AddCommGroup M'] [Module R M'] (f : M →ₗ[R] M')
    [IsLocalizedModule S f]
    (Rₛ : Type*) [CommRing Rₛ] [Algebra R Rₛ]
    [Module Rₛ M'] [IsScalarTower R Rₛ M']
    [IsLocalization S Rₛ]
    (Mₜ : R → Type*) [∀ t, AddCommGroup (Mₜ t)] [∀ t, Module R (Mₜ t)]
    (fₜ : ∀ t, M →ₗ[R] Mₜ t)
    [∀ t, IsLocalizedModule (.powers t) (fₜ t)]
    (Rₜ : R → Type*) [∀ t, CommRing (Rₜ t)] [∀ t, Algebra R (Rₜ t)]
    [∀ t, IsLocalization.Away t (Rₜ t)]
    [∀ t, Module (Rₜ t) (Mₜ t)]
    [∀ t, IsScalarTower R (Rₜ t) (Mₜ t)]
    [FinitePresentation R M] {I : Type*} [Finite I]
    (b : Basis I Rₛ M')
include b

Lean source · full declaration

lemma FinitePresentation.exists_basis_of_isLocalizedModule_powers :
    ∃ (t : R) (ht : t ∈ S) (b' : Basis I (Rₜ t) (Mₜ t)),
      ∀ (i : I), (IsLocalizedModule.lift (.powers t) (fₜ t) f
        (fun x ↦ IsLocalizedModule.map_units f
          ⟨x.1, IsConcreteLE.le_iff.mp (Submonoid.powers_le.mpr ht) x.2⟩) (b' i) = b i) := by
  obtain ⟨t, ht, b', hb'⟩ := Module.FinitePresentation.exists_basis_localizedModule_powers S f Rₛ b
  use t, ht
  let eM : LocalizedModule (.powers t) M ≃ₗ[R] Mₜ t := IsLocalizedModule.iso (.powers t) (fₜ t)
  let eb'' : Mₜ t ≃ₗ[R] I →₀ Rₜ t :=
    eM.symm ≪≫ₗ b'.repr.restrictScalars R ≪≫ₗ
      IsLocalizedModule.linearEquiv (.powers t)
        (Finsupp.mapRange.linearMap (Algebra.linearMap R _))
        (Finsupp.mapRange.linearMap (Algebra.linearMap R _))
  let eb : Mₜ t ≃ₗ[Rₜ t] I →₀ Rₜ t :=
    .ofLinearMap (.extendScalarsOfIsLocalizationEquiv (.powers t) (Rₜ t) eb'')
      (.extendScalarsOfIsLocalizationEquiv (.powers t) (Rₜ t) eb''.symm)
      (by ext; simp) (by ext; simp)
  refine ⟨Basis.ofRepr eb, fun i ↦ ?_⟩
  simp only [LinearMap.extendScalarsOfIsLocalizationEquiv_apply, LinearEquiv.trans_symm,
    LinearEquiv.symm_symm, Basis.coe_ofRepr, LinearEquiv.symm_ofLinearMap,
    LinearEquiv.coe_ofLinearMap,
    LinearMap.extendScalarsOfIsLocalization_apply', LinearEquiv.coe_coe, LinearEquiv.trans_apply,
    LinearEquiv.restrictScalars_symm_apply, Basis.repr_symm_apply, eb, eb'']
  have : Finsupp.single i 1 =
    (Finsupp.mapRange.linearMap (Algebra.linearMap R (Rₜ t))) (Finsupp.basisSingleOne i) := by simp
  rw [this]
  rw [IsLocalizedModule.linearEquiv_symm_apply]
  simp only [Finsupp.coe_basisSingleOne, Finsupp.mapRange.linearMap_apply, Finsupp.mapRange_single,
    Algebra.linearMap_apply, map_one, Finsupp.linearCombination_single, one_smul,
    eM]
  rw [IsLocalizedModule.lift_iso, hb']

lemma

exists_of_surjective

L166 ↗

Module.exists_of_surjective

Source context 5 commands

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

@[expose] public section
universe w t u v
namespace Module
variable {R M N : Type*} [CommRing R] [AddCommGroup M] [AddCommGroup N]
  [Module R M] [Module R N]
open LinearMap in

Lean source · statement

lemma exists_of_surjective [Module.Finite R N] (f : M →ₗ[R] N)
    (p : Ideal R) [p.IsPrime] (hf : Function.Surjective (LocalizedModule.map p.primeCompl f)) :
    ∃ g ∉ p, Function.Surjective (LocalizedModule.map (Submonoid.powers g) f)

lemma

exists_of_surjective'

L197 ↗

Module.exists_of_surjective'

Source context 4 commands

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

@[expose] public section
universe w t u v
namespace Module
variable {R M N : Type*} [CommRing R] [AddCommGroup M] [AddCommGroup N]
  [Module R M] [Module R N]

Lean source · statement

lemma exists_of_surjective' [Module.Finite R N] (f : M →ₗ[R] N)
    (p : Ideal R) [p.IsPrime] {Mₚ Nₚ : Type*}
    [AddCommGroup Mₚ] [AddCommGroup Nₚ] [Module R Mₚ] [Module R Nₚ]
    (fM : M →ₗ[R] Mₚ) (fN : N →ₗ[R] Nₚ)
    [IsLocalizedModule p.primeCompl fM]
    [IsLocalizedModule p.primeCompl fN]
    (hf : Function.Surjective (IsLocalizedModule.map p.primeCompl fM fN f)) :
    ∃ g ∉ p, Function.Surjective (LocalizedModule.map (Submonoid.powers g) f)

lemma

exists_of_bijective'

L208 ↗

Module.exists_of_bijective'

Source context 4 commands

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

@[expose] public section
universe w t u v
namespace Module
variable {R M N : Type*} [CommRing R] [AddCommGroup M] [AddCommGroup N]
  [Module R M] [Module R N]

Lean source · statement

lemma exists_of_bijective' [Module.Finite R M] [Module.FinitePresentation R N] (f : M →ₗ[R] N)
    (p : Ideal R) [p.IsPrime] {Rₚ Mₚ Nₚ : Type*}
    [CommRing Rₚ] [Algebra R Rₚ] [IsLocalization.AtPrime Rₚ p]
    [AddCommGroup Mₚ] [AddCommGroup Nₚ] [Module R Mₚ] [Module R Nₚ]
    (fM : M →ₗ[R] Mₚ) (fN : N →ₗ[R] Nₚ)
    [IsLocalizedModule p.primeCompl fM]
    [IsLocalizedModule p.primeCompl fN]
    {Mₜ Nₜ : R → Type*}
    [∀ r, AddCommGroup (Mₜ r)] [∀ r, Module R (Mₜ r)]
    [∀ r, AddCommGroup (Nₜ r)] [∀ r, Module R (Nₜ r)]
    (fₜ : ∀ r, M →ₗ[R] Mₜ r) [∀ r, IsLocalizedModule (Submonoid.powers r) (fₜ r)]
    (gₜ : ∀ r, N →ₗ[R] Nₜ r) [∀ r, IsLocalizedModule (Submonoid.powers r) (gₜ r)]
    (hf : Function.Bijective (IsLocalizedModule.map p.primeCompl fM fN f)) :
    ∃ (g : R), g ∉ p ∧
      Function.Bijective (IsLocalizedModule.map (Submonoid.powers g) (fₜ g) (gₜ g) f)

lemma

exists_of_bijective

L227 ↗

Module.exists_of_bijective

Source context 4 commands

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

@[expose] public section
universe w t u v
namespace Module
variable {R M N : Type*} [CommRing R] [AddCommGroup M] [AddCommGroup N]
  [Module R M] [Module R N]

Lean source · statement

lemma exists_of_bijective [Module.Finite R M] [Module.FinitePresentation R N] (f : M →ₗ[R] N)
    (p : Ideal R) [p.IsPrime] {Rₚ Mₚ Nₚ : Type*}
    [CommRing Rₚ] [Algebra R Rₚ] [IsLocalization.AtPrime Rₚ p]
    [AddCommGroup Mₚ] [AddCommGroup Nₚ] [Module R Mₚ] [Module R Nₚ]
    (fM : M →ₗ[R] Mₚ) (fN : N →ₗ[R] Nₚ)
    [IsLocalizedModule p.primeCompl fM]
    [IsLocalizedModule p.primeCompl fN]
    (hf : Function.Bijective (IsLocalizedModule.map p.primeCompl fM fN f)) :
    ∃ (g : R), g ∉ p ∧ Function.Bijective (LocalizedModule.map (Submonoid.powers g) f)

lemma

isSmoothAt_of_smooth

L250 ↗

Algebra.isSmoothAt_of_smooth

Source context 7 commands

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

@[expose] public section
universe w t u v
namespace Algebra
variable {R S : Type u} [CommRing R] [CommRing S]
section
variable [Algebra R S]
variable (R) in

Lean source · statement

lemma isSmoothAt_of_smooth [Smooth R S] (p : Ideal S) [p.IsPrime] :
    IsSmoothAt R p

Module documentation

Smooth and locally standard smooth

Declarations