NYLL
Module

Module_Flat_projective_ker_baseChange_of_isLocalizationAway_of_ker_baseChange_le_range.lean

Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.Module_Flat_projective_ker_baseChange_of_isLocalizationAway_of_ker_baseChange_le_range
10 declarations indexed from sourceView source ↗

Module documentation

Module Flat projective ker base Change of is Localization Away of ker base Change le range

Imports15
Imported by2

Declarations

theorem

ker_le_range_transport

L52 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_projective_ker_baseChange_of_isLocalizationAway_of_ker_baseChange_le_range.B2SOL.ker_le_range_transport
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_projective_ker_baseChange_of_isLocalizationAway_of_ker_baseChange_le_range
universe u uR uT uM
open TensorProduct
namespace B2SOL
section Transport
variable {A : Type*} [Semiring A]
  {M₀ M₁ M₂ N₀ N₁ N₂ : Type*}
  [AddCommMonoid M₀] [AddCommMonoid M₁] [AddCommMonoid M₂]
  [AddCommMonoid N₀] [AddCommMonoid N₁] [AddCommMonoid N₂]
  [Module A M₀] [Module A M₁] [Module A M₂] [Module A N₀] [Module A N₁] [Module A N₂]
Lean source · statement
theorem ker_le_range_transport (e₀ : M₀ ≃ₗ[A] N₀) (e₁ : M₁ ≃ₗ[A] N₁) (e₂ : M₂ ≃ₗ[A] N₂)
    (u : M₀ →ₗ[A] M₁) (v : M₁ →ₗ[A] M₂) (u' : N₀ →ₗ[A] N₁) (v' : N₁ →ₗ[A] N₂)
    (h₀ : ∀ x, e₁ (u x) = u' (e₀ x)) (h₁ : ∀ y, e₂ (v y) = v' (e₁ y))
    (hex : LinearMap.ker v ≤ LinearMap.range u) :
    LinearMap.ker v' ≤ LinearMap.range u'
theorem

cancelBaseChange_baseChange_baseChange

L73 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_projective_ker_baseChange_of_isLocalizationAway_of_ker_baseChange_le_range.B2SOL.cancelBaseChange_baseChange_baseChange
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_projective_ker_baseChange_of_isLocalizationAway_of_ker_baseChange_le_range
universe u uR uT uM
open TensorProduct
namespace B2SOL
section Cancel
variable (R : Type*) (S : Type*) (B : Type*) [CommRing R] [CommRing S] [CommRing B]
  [Algebra R S] [Algebra R B] [Algebra S B] [IsScalarTower R S B]
  {M N : Type*} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N]
Lean source · statement
theorem cancelBaseChange_baseChange_baseChange (f : M →ₗ[R] N) (x : B ⊗[S] (S ⊗[R] M)) :
    AlgebraTensorModule.cancelBaseChange R S B B N (((f.baseChange S).baseChange B) x) =
      (f.baseChange B) (AlgebraTensorModule.cancelBaseChange R S B B M x)
theorem

baseChange_subtype_injective

L91 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_projective_ker_baseChange_of_isLocalizationAway_of_ker_baseChange_le_range.B2SOL.baseChange_subtype_injective
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_projective_ker_baseChange_of_isLocalizationAway_of_ker_baseChange_le_range
universe u uR uT uM
open TensorProduct
namespace B2SOL
section FlatKer
variable {R : Type uR} [CommRing R] (T : Type uT) [CommRing T] [Algebra R T] [Module.Flat R T]
  {M N : Type uM} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N]
Lean source · statement
theorem baseChange_subtype_injective (f : M →ₗ[R] N) :
    Function.Injective ((LinearMap.ker f).subtype.baseChange T)
theorem

exists_baseChange_subtype_eq

L98 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_projective_ker_baseChange_of_isLocalizationAway_of_ker_baseChange_le_range.B2SOL.exists_baseChange_subtype_eq
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_projective_ker_baseChange_of_isLocalizationAway_of_ker_baseChange_le_range
universe u uR uT uM
open TensorProduct
namespace B2SOL
section FlatKer
variable {R : Type uR} [CommRing R] (T : Type uT) [CommRing T] [Algebra R T] [Module.Flat R T]
  {M N : Type uM} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N]
Lean source · statement
theorem exists_baseChange_subtype_eq (f : M →ₗ[R] N) (y : T ⊗[R] M)
    (hy : f.baseChange T y = 0) :
    ∃ x : T ⊗[R] LinearMap.ker f, (LinearMap.ker f).subtype.baseChange T x = y
theorem

kerBaseChangeHom_bijective

L104 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_projective_ker_baseChange_of_isLocalizationAway_of_ker_baseChange_le_range.B2SOL.kerBaseChangeHom_bijective
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_projective_ker_baseChange_of_isLocalizationAway_of_ker_baseChange_le_range
universe u uR uT uM
open TensorProduct
namespace B2SOL
section FlatKer
variable {R : Type uR} [CommRing R] (T : Type uT) [CommRing T] [Algebra R T] [Module.Flat R T]
  {M N : Type uM} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N]
Lean source · statement
theorem kerBaseChangeHom_bijective (f : M →ₗ[R] N) :
    Function.Bijective (TwoChartCech.kerBaseChangeHom f T)
def

kerEquiv

L116 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_projective_ker_baseChange_of_isLocalizationAway_of_ker_baseChange_le_range.B2SOL.kerEquiv
Documentation

The comparison equivalence between the base change of a kernel and the kernel after flat base change.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_projective_ker_baseChange_of_isLocalizationAway_of_ker_baseChange_le_range
universe u uR uT uM
open TensorProduct
namespace B2SOL
section FlatKer
variable {R : Type uR} [CommRing R] (T : Type uT) [CommRing T] [Algebra R T] [Module.Flat R T]
  {M N : Type uM} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N]
Lean source · statement
def kerEquiv (f : M →ₗ[R] N) :
    T ⊗[R] LinearMap.ker f ≃ₗ[T] LinearMap.ker (f.baseChange T)
theorem

kerEquiv_apply_coe

L120 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_projective_ker_baseChange_of_isLocalizationAway_of_ker_baseChange_le_range.B2SOL.kerEquiv_apply_coe
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_projective_ker_baseChange_of_isLocalizationAway_of_ker_baseChange_le_range
universe u uR uT uM
open TensorProduct
namespace B2SOL
section FlatKer
variable {R : Type uR} [CommRing R] (T : Type uT) [CommRing T] [Algebra R T] [Module.Flat R T]
  {M N : Type uM} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N]
Lean source · statement
theorem kerEquiv_apply_coe (f : M →ₗ[R] N) (x : T ⊗[R] LinearMap.ker f) :
    (kerEquiv T f x : T ⊗[R] M) = (LinearMap.ker f).subtype.baseChange T x
theorem

key

L132 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_projective_ker_baseChange_of_isLocalizationAway_of_ker_baseChange_le_range.B2SOL.key
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_projective_ker_baseChange_of_isLocalizationAway_of_ker_baseChange_le_range
universe u uR uT uM
open TensorProduct
namespace B2SOL
section Key
variable (R : Type uR) (S : Type uR) (B : Type uT) [CommRing R] [CommRing S] [CommRing B]
  [Algebra R S] [Algebra R B] [Algebra S B] [IsScalarTower R S B] [Module.Flat R S]
  {M N : Type uM} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N]
Lean source · statement
theorem key (f : M →ₗ[R] N) (w : B ⊗[S] (S ⊗[R] LinearMap.ker f)) :
    ((LinearMap.ker f).subtype.baseChange B)
        (AlgebraTensorModule.cancelBaseChange R S B B (LinearMap.ker f) w) =
      AlgebraTensorModule.cancelBaseChange R S B B M
        ↑(TwoChartCech.kerBaseChangeHom (f.baseChange S) B
          (LinearEquiv.baseChange S B _ _ (kerEquiv S f) w))
theorem

subsingleton_tensor

L149 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_projective_ker_baseChange_of_isLocalizationAway_of_ker_baseChange_le_range.B2SOL.subsingleton_tensor
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_projective_ker_baseChange_of_isLocalizationAway_of_ker_baseChange_le_range
universe u uR uT uM
open TensorProduct
namespace B2SOL
Lean source · statement
theorem subsingleton_tensor {R : Type*} [CommRing R] (T : Type*) [CommRing T] [Algebra R T]
    (M : Type*) [AddCommGroup M] [Module R M] [Subsingleton M] : Subsingleton (T ⊗[R] M)
theorem

projective_ker_baseChange_of_isLocalizationAway_of_ker_baseChange_le_range

L164 ↗
Module.Flat.projective_ker_baseChange_of_isLocalizationAway_of_ker_baseChange_le_range
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_projective_ker_baseChange_of_isLocalizationAway_of_ker_baseChange_le_range
universe u uR uT uM
open TensorProduct
attribute [local simp] B2SOL.kerEquiv_apply_coe
open B2SOL in
Lean source · statement
theorem
  _root_.Module.Flat.projective_ker_baseChange_of_isLocalizationAway_of_ker_baseChange_le_range
    {R : Type u} [CommRing R] [IsNoetherianRing R]
    (C : ℕ → Type u) [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)] [∀ i, Module.Flat R (C i)]
    (d : ∀ i, C i →ₗ[R] C (i + 1)) (hdd : ∀ i, d (i + 1) ∘ₗ d i = 0)
    (n : ℕ) (hbd : ∀ i, n ≤ i → Subsingleton (C i))
    (hfin0 : Module.Finite R (LinearMap.ker (d 0)))
    (g : R) (S : Type u) [CommRing S] [Algebra R S] [IsLocalization.Away g S]
    (hex : ∀ i : ℕ, LinearMap.ker ((d (i + 1)).baseChange S) ≤ LinearMap.range ((d i).baseChange S))
    (A : Type u) [CommRing A] [Algebra R A] (hA : IsUnit (algebraMap R A g)) :
    Module.Finite A (LinearMap.ker ((d 0).baseChange A)) ∧
      Module.Projective A (LinearMap.ker ((d 0).baseChange A)) ∧
      (∀ i : ℕ, LinearMap.ker ((d (i + 1)).baseChange A) ≤ LinearMap.range ((d i).baseChange A)) ∧
      Function.Bijective (TwoChartCech.kerBaseChangeHom (d 0) A)

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