NYLL
Module

TwoChartCech_Mumford_bijective_kerMapBaseChange.lean

Nyll.AlgebraicCurves.Cohomology.Cech.TwoChartCech_Mumford_bijective_kerMapBaseChange
8 declarations indexed from sourceView source ↗

Module documentation

Bijectivity of kernel base change in the finite-presentation construction for a Cech differential.

Imports6
Imported by5

Declarations

theorem

subtype_baseChange_injective

L46 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Mumford_bijective_kerMapBaseChange.TwoChartCech.Mumford.subtype_baseChange_injective
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Mumford_bijective_kerMapBaseChange
noncomputable section
open scoped TensorProduct
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace Mumford
open _root_.TwoChartCech.Mumford
open _root_.TwoChartCech.Mumford
open _root_.TwoChartCech
variable {R : Type u} [CommRing R]
variable {C0 C1 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable (d : C0 →ₗ[R] C1) [Module.Finite R (C1 ⧸ LinearMap.range d)]
variable (A : Type u) [CommRing A] [Algebra R A]
Lean source · statement
theorem subtype_baseChange_injective [Module.Flat R C1] :
    Function.Injective ((K0 d).subtype.baseChange A)
theorem

mem_range_subtype_baseChange

L52 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Mumford_bijective_kerMapBaseChange.TwoChartCech.Mumford.mem_range_subtype_baseChange
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Mumford_bijective_kerMapBaseChange
noncomputable section
open scoped TensorProduct
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace Mumford
open _root_.TwoChartCech.Mumford
open _root_.TwoChartCech.Mumford
open _root_.TwoChartCech
variable {R : Type u} [CommRing R]
variable {C0 C1 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable (d : C0 →ₗ[R] C1) [Module.Finite R (C1 ⧸ LinearMap.range d)]
variable (A : Type u) [CommRing A] [Algebra R A]
Lean source · statement
theorem mem_range_subtype_baseChange (w : A ⊗[R] (C0 × (Fin (rank d) → R))) :
    ((d.coprod (lift d)).baseChange A) w = 0 ↔ ∃ z, ((K0 d).subtype.baseChange A) z = w
theorem

prodRight_apply_eq_baseChange

L62 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Mumford_bijective_kerMapBaseChange.TwoChartCech.Mumford.prodRight_apply_eq_baseChange
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Mumford_bijective_kerMapBaseChange
noncomputable section
open scoped TensorProduct
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace Mumford
open _root_.TwoChartCech.Mumford
open _root_.TwoChartCech.Mumford
open _root_.TwoChartCech
variable {R : Type u} [CommRing R]
variable {C0 C1 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable (d : C0 →ₗ[R] C1) [Module.Finite R (C1 ⧸ LinearMap.range d)]
variable (A : Type u) [CommRing A] [Algebra R A]
Lean source · statement
theorem prodRight_apply_eq_baseChange {M N : Type u} [AddCommGroup M] [Module R M]
    [AddCommGroup N] [Module R N] (w : A ⊗[R] (M × N)) :
    (TensorProduct.prodRight R A A M N) w
      = (((LinearMap.fst R M N).baseChange A) w, ((LinearMap.snd R M N).baseChange A) w)
theorem

prodRight_subtype_baseChange

L70 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Mumford_bijective_kerMapBaseChange.TwoChartCech.Mumford.prodRight_subtype_baseChange
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Mumford_bijective_kerMapBaseChange
noncomputable section
open scoped TensorProduct
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace Mumford
open _root_.TwoChartCech.Mumford
open _root_.TwoChartCech.Mumford
open _root_.TwoChartCech
variable {R : Type u} [CommRing R]
variable {C0 C1 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable (d : C0 →ₗ[R] C1) [Module.Finite R (C1 ⧸ LinearMap.range d)]
variable (A : Type u) [CommRing A] [Algebra R A]
Lean source · statement
theorem prodRight_subtype_baseChange (z : A ⊗[R] K0 d) :
    (TensorProduct.prodRight R A A C0 (Fin (rank d) → R)) (((K0 d).subtype.baseChange A) z)
      = (((ι0 d).baseChange A) z, ((dK d).baseChange A) z)
theorem

coprod_baseChange_apply

L82 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Mumford_bijective_kerMapBaseChange.TwoChartCech.Mumford.coprod_baseChange_apply
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Mumford_bijective_kerMapBaseChange
noncomputable section
open scoped TensorProduct
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace Mumford
open _root_.TwoChartCech.Mumford
open _root_.TwoChartCech.Mumford
open _root_.TwoChartCech
variable {R : Type u} [CommRing R]
variable {C0 C1 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable (d : C0 →ₗ[R] C1) [Module.Finite R (C1 ⧸ LinearMap.range d)]
variable (A : Type u) [CommRing A] [Algebra R A]
Lean source · statement
theorem coprod_baseChange_apply (w : A ⊗[R] (C0 × (Fin (rank d) → R))) :
    ((d.coprod (lift d)).baseChange A) w
      = (d.baseChange A) ((TensorProduct.prodRight R A A C0 (Fin (rank d) → R)) w).1
        + ((lift d).baseChange A) ((TensorProduct.prodRight R A A C0 (Fin (rank d) → R)) w).2
theorem

kerMapBaseChange_injective

L90 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Mumford_bijective_kerMapBaseChange.TwoChartCech.Mumford.kerMapBaseChange_injective
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Mumford_bijective_kerMapBaseChange
noncomputable section
open scoped TensorProduct
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace Mumford
open _root_.TwoChartCech.Mumford
open _root_.TwoChartCech.Mumford
open _root_.TwoChartCech
variable {R : Type u} [CommRing R]
variable {C0 C1 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable (d : C0 →ₗ[R] C1) [Module.Finite R (C1 ⧸ LinearMap.range d)]
variable (A : Type u) [CommRing A] [Algebra R A]
Lean source · statement
theorem kerMapBaseChange_injective [Module.Flat R C1] :
    Function.Injective (kerMapBaseChange (dK d) d (ι0 d) (ι1 d) (comm d) A)
theorem

kerMapBaseChange_surjective

L102 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Mumford_bijective_kerMapBaseChange.TwoChartCech.Mumford.kerMapBaseChange_surjective
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Mumford_bijective_kerMapBaseChange
noncomputable section
open scoped TensorProduct
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace Mumford
open _root_.TwoChartCech.Mumford
open _root_.TwoChartCech.Mumford
open _root_.TwoChartCech
variable {R : Type u} [CommRing R]
variable {C0 C1 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable (d : C0 →ₗ[R] C1) [Module.Finite R (C1 ⧸ LinearMap.range d)]
variable (A : Type u) [CommRing A] [Algebra R A]
Lean source · statement
theorem kerMapBaseChange_surjective :
    Function.Surjective (kerMapBaseChange (dK d) d (ι0 d) (ι1 d) (comm d) A)
theorem

bijective_kerMapBaseChange

L128 ↗
TwoChartCech.Mumford.bijective_kerMapBaseChange
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Mumford_bijective_kerMapBaseChange
noncomputable section
open scoped TensorProduct
universe u
open _root_.AlgebraicCurves.Cohomology.Cech.Proofs in
open _root_.TwoChartCech.Mumford
  TwoChartCech_Mumford_bijective_kerMapBaseChange.TwoChartCech.Mumford in
Lean source · statement
theorem _root_.TwoChartCech.Mumford.bijective_kerMapBaseChange
    {R : Type u} [CommRing R]
    {C0 C1 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1] [Module.Flat
      R C1]
    (d : C0 →ₗ[R] C1) [Module.Finite R (C1 ⧸ LinearMap.range d)]
    (A : Type u) [CommRing A] [Algebra R A] :
    Function.Bijective
      (TwoChartCech.kerMapBaseChange (TwoChartCech.Mumford.dK d) d (TwoChartCech.Mumford.ι0 d)
        (TwoChartCech.Mumford.ι1 d) (TwoChartCech.Mumford.comm d) A)

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