NYLL
Module

Module_free_coker_and_ker_baseChange_of_ker_le_range_residueField.lean

Nyll.AlgebraicCurves.Foundations.Algebra.Module_free_coker_and_ker_baseChange_of_ker_le_range_residueField
7 declarations indexed from sourceView source ↗

Module documentation

Module free coker and ker base Change of ker le range residue Field

Imports10
  • Mathlib.Algebra.Exact.Basic
  • Mathlib.Algebra.Module.Projective
  • Mathlib.LinearAlgebra.Quotient.Basic
  • Mathlib.LinearAlgebra.TensorProduct.RightExactness
  • Mathlib.LinearAlgebra.TensorProduct.Tower
  • Mathlib.RingTheory.Flat.Basic
  • Mathlib.RingTheory.LocalRing.Module
  • Mathlib.Tactic.Abel
  • Mathlib.RingTheory.Finiteness.Basic
  • Mathlib.Tactic.Ext
Imported by2

Declarations

theorem

lTensor_split

L46 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Module_free_coker_and_ker_baseChange_of_ker_le_range_residueField.BC0Free.lTensor_split
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_free_coker_and_ker_baseChange_of_ker_le_range_residueField
universe u v
open TensorProduct
namespace BC0Free
variable {R : Type u} [CommRing R]
section Split
variable {K M B : Type v} [AddCommGroup K] [Module R K] [AddCommGroup M] [Module R M]
  [AddCommGroup B] [Module R B]
Lean source · statement
theorem lTensor_split (i : K →ₗ[R] M) (r : M →ₗ[R] K) (p : M →ₗ[R] B) (s : B →ₗ[R] M)
    (hri : r ∘ₗ i = LinearMap.id) (_hps : p ∘ₗ s = LinearMap.id) (hpi : p ∘ₗ i = 0)
    (hsum : i ∘ₗ r + s ∘ₗ p = LinearMap.id)
    (A : Type u) [AddCommGroup A] [Module R A] :
    Function.Injective (i.lTensor A) ∧ LinearMap.range (i.lTensor A) = LinearMap.ker (p.lTensor A)
def

dbar

L87 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Module_free_coker_and_ker_baseChange_of_ker_le_range_residueField.BC0Free.dbar
Documentation

The map induced on the cokernel of the preceding differential.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_free_coker_and_ker_baseChange_of_ker_le_range_residueField
universe u v
open TensorProduct
namespace BC0Free
variable {R : Type u} [CommRing R]
section Main
variable [IsLocalRing R]
  {C0 C1 C2 : Type v} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
  [AddCommGroup C2] [Module R C2] [Module.Finite R C1] [Module.Free R C1] [Module.Finite R C2]
    [Module.Free R C2]
local notation "κ" => IsLocalRing.ResidueField R
Lean source · statement
def dbar (d0 : C0 →ₗ[R] C1) (d1 : C1 →ₗ[R] C2) (hdd : d1 ∘ₗ d0 = 0) :
    (C1 ⧸ LinearMap.range d0) →ₗ[R] C2
theorem

dbar_comp_mkQ

L94 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Module_free_coker_and_ker_baseChange_of_ker_le_range_residueField.BC0Free.dbar_comp_mkQ
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_free_coker_and_ker_baseChange_of_ker_le_range_residueField
universe u v
open TensorProduct
namespace BC0Free
variable {R : Type u} [CommRing R]
section Main
variable [IsLocalRing R]
  {C0 C1 C2 : Type v} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
  [AddCommGroup C2] [Module R C2] [Module.Finite R C1] [Module.Free R C1] [Module.Finite R C2]
    [Module.Free R C2]
local notation "κ" => IsLocalRing.ResidueField R
omit [IsLocalRing R] [Module.Finite R C1] [Module.Free R C1] [Module.Finite R C2] [Module.Free R
  C2] in
Lean source · statement
theorem dbar_comp_mkQ (d0 : C0 →ₗ[R] C1) (d1 : C1 →ₗ[R] C2) (hdd : d1 ∘ₗ d0 = 0) :
    dbar d0 d1 hdd ∘ₗ (LinearMap.range d0).mkQ = d1
theorem

lTensor_dbar_injective

L98 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Module_free_coker_and_ker_baseChange_of_ker_le_range_residueField.BC0Free.lTensor_dbar_injective
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_free_coker_and_ker_baseChange_of_ker_le_range_residueField
universe u v
open TensorProduct
namespace BC0Free
variable {R : Type u} [CommRing R]
section Main
variable [IsLocalRing R]
  {C0 C1 C2 : Type v} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
  [AddCommGroup C2] [Module R C2] [Module.Finite R C1] [Module.Free R C1] [Module.Finite R C2]
    [Module.Free R C2]
local notation "κ" => IsLocalRing.ResidueField R
omit [Module.Finite R C1] [Module.Free R C1] [Module.Finite R C2] [Module.Free R C2] in
Lean source · statement
theorem lTensor_dbar_injective (d0 : C0 →ₗ[R] C1) (d1 : C1 →ₗ[R] C2) (hdd : d1 ∘ₗ d0 = 0)
    (hH1 : LinearMap.ker (d1.baseChange (IsLocalRing.ResidueField R)) ≤
      LinearMap.range (d0.baseChange (IsLocalRing.ResidueField R))) :
    Function.Injective ((dbar d0 d1 hdd).lTensor κ)
theorem

free_coker

L119 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Module_free_coker_and_ker_baseChange_of_ker_le_range_residueField.BC0Free.free_coker
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_free_coker_and_ker_baseChange_of_ker_le_range_residueField
universe u v
open TensorProduct
namespace BC0Free
variable {R : Type u} [CommRing R]
section Main
variable [IsLocalRing R]
  {C0 C1 C2 : Type v} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
  [AddCommGroup C2] [Module R C2] [Module.Finite R C1] [Module.Free R C1] [Module.Finite R C2]
    [Module.Free R C2]
local notation "κ" => IsLocalRing.ResidueField R
omit [Module.Free R C1] in
Lean source · statement
theorem free_coker (d0 : C0 →ₗ[R] C1) (d1 : C1 →ₗ[R] C2) (hdd : d1 ∘ₗ d0 = 0)
    (hH1 : LinearMap.ker (d1.baseChange (IsLocalRing.ResidueField R)) ≤
      LinearMap.range (d0.baseChange (IsLocalRing.ResidueField R))) :
    Module.Free R (C1 ⧸ LinearMap.range d0)
theorem

ker_baseChange

L131 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Module_free_coker_and_ker_baseChange_of_ker_le_range_residueField.BC0Free.ker_baseChange
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_free_coker_and_ker_baseChange_of_ker_le_range_residueField
universe u v
open TensorProduct
namespace BC0Free
variable {R : Type u} [CommRing R]
section Main
variable [IsLocalRing R]
  {C0 C1 C2 : Type v} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
  [AddCommGroup C2] [Module R C2] [Module.Finite R C1] [Module.Free R C1] [Module.Finite R C2]
    [Module.Free R C2]
local notation "κ" => IsLocalRing.ResidueField R
Lean source · statement
theorem ker_baseChange (d0 : C0 →ₗ[R] C1) (d1 : C1 →ₗ[R] C2) (hdd : d1 ∘ₗ d0 = 0)
    (hH1 : LinearMap.ker (d1.baseChange (IsLocalRing.ResidueField R)) ≤
      LinearMap.range (d0.baseChange (IsLocalRing.ResidueField R)))
    (A : Type u) [CommRing A] [Algebra R A] :
    LinearMap.range ((LinearMap.ker d0).subtype.baseChange A) = LinearMap.ker (d0.baseChange A) ∧
      Function.Injective ((LinearMap.ker d0).subtype.baseChange A)
theorem

free_coker_and_ker_baseChange_of_ker_le_range_residueField

L218 ↗
Module.free_coker_and_ker_baseChange_of_ker_le_range_residueField
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_free_coker_and_ker_baseChange_of_ker_le_range_residueField
universe u v
open TensorProduct
Lean source · statement
theorem _root_.Module.free_coker_and_ker_baseChange_of_ker_le_range_residueField
    (R : Type u) [CommRing R] [IsLocalRing R]
    {C0 C1 C2 : Type v} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
    [AddCommGroup C2] [Module R C2] [Module.Finite R C1] [Module.Free R C1] [Module.Finite R C2]
      [Module.Free R C2]
    (d0 : C0 →ₗ[R] C1) (d1 : C1 →ₗ[R] C2) (hdd : d1 ∘ₗ d0 = 0)
    (hH1 : LinearMap.ker (d1.baseChange (IsLocalRing.ResidueField R)) ≤
      LinearMap.range (d0.baseChange (IsLocalRing.ResidueField R))) :
    Module.Free R (C1 ⧸ LinearMap.range d0) ∧
      ∀ (A : Type u) [CommRing A] [Algebra R A],
        LinearMap.range ((LinearMap.ker d0).subtype.baseChange A) = LinearMap.ker (d0.baseChange A)
          ∧
          Function.Injective ((LinearMap.ker d0).subtype.baseChange A)

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