Module

Module_quasiIso_baseChange_of_quasiIso_of_flat.lean

Nyll.AlgebraicCurves.Foundations.Algebra.Module_quasiIso_baseChange_of_quasiIso_of_flat

16 declarations indexed from sourceView source ↗

Module documentation

Module quasi Iso base Change of quasi Iso of flat

Imports5

Mathlib.LinearAlgebra.TensorProduct.Prod
Mathlib.RingTheory.Flat.Basic
Mathlib.Tactic.Abel
Mathlib.Tactic.Ext
Nyll.AlgebraicCurves.Foundations.Algebra.Module_Flat_ker_baseChange_eq_bot_and_ker_le_range_of_flat_of_exact

Imported by4

theorem

flat_prod

L33 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.ModuleQuasiIsoBaseChangeQuasiIso.QisoBC.flat_prod

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.ModuleQuasiIsoBaseChangeQuasiIso
universe u
open TensorProduct
namespace QisoBC

Lean source · statement

theorem flat_prod {R : Type u} [CommRing R] (M N : Type u) [AddCommGroup M] [Module R M]
    [AddCommGroup N] [Module R N] [Module.Flat R M] [Module.Flat R N] : Module.Flat R (M × N)

def

Cone

L58 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.ModuleQuasiIsoBaseChangeQuasiIso.QisoBC.Cone

Documentation

The graded cone has K 0 in degree zero and K (i + 1) × C i in positive degrees.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.ModuleQuasiIsoBaseChangeQuasiIso
universe u
open TensorProduct
namespace QisoBC
variable {S : Type u} [CommRing S]
variable (K : ℕ → Type u) [∀ i, AddCommGroup (K i)] [∀ i, Module S (K i)]
variable (C : ℕ → Type u) [∀ i, AddCommGroup (C i)] [∀ i, Module S (C i)]

Lean source · full declaration

def Cone : ℕ → Type u
  | 0 => K 0
  | i + 1 => K (i + 1) × C i

instance

instACG

L62 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.ModuleQuasiIsoBaseChangeQuasiIso.QisoBC.instACG

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.ModuleQuasiIsoBaseChangeQuasiIso
universe u
open TensorProduct
namespace QisoBC
variable {S : Type u} [CommRing S]
variable (K : ℕ → Type u) [∀ i, AddCommGroup (K i)] [∀ i, Module S (K i)]
variable (C : ℕ → Type u) [∀ i, AddCommGroup (C i)] [∀ i, Module S (C i)]

Lean source · full declaration

instance instACG : ∀ i, AddCommGroup (Cone K C i)
  | 0 => inferInstanceAs (AddCommGroup (K 0))
  | i + 1 => inferInstanceAs (AddCommGroup (K (i + 1) × C i))

instance

instMod

L66 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.ModuleQuasiIsoBaseChangeQuasiIso.QisoBC.instMod

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.ModuleQuasiIsoBaseChangeQuasiIso
universe u
open TensorProduct
namespace QisoBC
variable {S : Type u} [CommRing S]
variable (K : ℕ → Type u) [∀ i, AddCommGroup (K i)] [∀ i, Module S (K i)]
variable (C : ℕ → Type u) [∀ i, AddCommGroup (C i)] [∀ i, Module S (C i)]

Lean source · full declaration

instance instMod : ∀ i, Module S (Cone K C i)
  | 0 => inferInstanceAs (Module S (K 0))
  | i + 1 => inferInstanceAs (Module S (K (i + 1) × C i))

theorem

flat_cone

L70 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.ModuleQuasiIsoBaseChangeQuasiIso.QisoBC.flat_cone

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.ModuleQuasiIsoBaseChangeQuasiIso
universe u
open TensorProduct
namespace QisoBC
variable {S : Type u} [CommRing S]
variable (K : ℕ → Type u) [∀ i, AddCommGroup (K i)] [∀ i, Module S (K i)]
variable (C : ℕ → Type u) [∀ i, AddCommGroup (C i)] [∀ i, Module S (C i)]

Lean source · full declaration

theorem flat_cone [∀ i, Module.Flat S (K i)] [∀ i, Module.Flat S (C i)] :
    ∀ i, Module.Flat S (Cone K C i)
  | 0 => inferInstanceAs (Module.Flat S (K 0))
  | i + 1 => by
      have := flat_prod (R := S) (K (i + 1)) (C i)
      exact inferInstanceAs (Module.Flat S (K (i + 1) × C i))

theorem

subsingleton_cone

L79 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.ModuleQuasiIsoBaseChangeQuasiIso.QisoBC.subsingleton_cone

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.ModuleQuasiIsoBaseChangeQuasiIso
universe u
open TensorProduct
namespace QisoBC
variable {S : Type u} [CommRing S]
variable (K : ℕ → Type u) [∀ i, AddCommGroup (K i)] [∀ i, Module S (K i)]
variable (C : ℕ → Type u) [∀ i, AddCommGroup (C i)] [∀ i, Module S (C i)]
omit [∀ i, AddCommGroup (K i)] [∀ i, AddCommGroup (C i)] [∀ i, Module S (K i)] [∀ i, Module S (C
  i)] in

Lean source · full declaration

theorem subsingleton_cone (n : ℕ) (hK : ∀ i, n < i → Subsingleton (K i))
    (hC : ∀ i, n < i → Subsingleton (C i)) : ∀ i, n + 2 ≤ i → Subsingleton (Cone K C i)
  | 0 => fun h => absurd h (by omega)
  | i + 1 => fun h => by
      have := hK (i + 1) (by omega); have := hC i (by omega)
      exact inferInstanceAs (Subsingleton (K (i + 1) × C i))

def

D

L90 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.ModuleQuasiIsoBaseChangeQuasiIso.QisoBC.D

Documentation

The cone differential combines the differential on K with φ minus the shifted differential on C.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.ModuleQuasiIsoBaseChangeQuasiIso
universe u
open TensorProduct
namespace QisoBC
variable {S : Type u} [CommRing S]
variable (K : ℕ → Type u) [∀ i, AddCommGroup (K i)] [∀ i, Module S (K i)]
variable (C : ℕ → Type u) [∀ i, AddCommGroup (C i)] [∀ i, Module S (C i)]
variable (δ : ∀ i, K i →ₗ[S] K (i + 1)) (d : ∀ i, C i →ₗ[S] C (i + 1)) (φ : ∀ i, K i →ₗ[S] C i)

Lean source · full declaration

def D : ∀ i, Cone K C i →ₗ[S] Cone K C (i + 1)
  | 0 => LinearMap.prod (δ 0) (φ 0)
  | i + 1 => LinearMap.prod (δ (i + 1) ∘ₗ LinearMap.fst S (K (i + 1)) (C i))
      (φ (i + 1) ∘ₗ LinearMap.fst S (K (i + 1)) (C i) - d i ∘ₗ LinearMap.snd S (K (i + 1)) (C i))

theorem

D_zero_apply

L95 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.ModuleQuasiIsoBaseChangeQuasiIso.QisoBC.D_zero_apply

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.ModuleQuasiIsoBaseChangeQuasiIso
universe u
open TensorProduct
namespace QisoBC
variable {S : Type u} [CommRing S]
variable (K : ℕ → Type u) [∀ i, AddCommGroup (K i)] [∀ i, Module S (K i)]
variable (C : ℕ → Type u) [∀ i, AddCommGroup (C i)] [∀ i, Module S (C i)]
variable (δ : ∀ i, K i →ₗ[S] K (i + 1)) (d : ∀ i, C i →ₗ[S] C (i + 1)) (φ : ∀ i, K i →ₗ[S] C i)

Lean source · statement

theorem D_zero_apply (x : K 0) : (D K C δ d φ 0 x : K 1 × C 0) = (δ 0 x, φ 0 x)

theorem

D_succ_apply

L97 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.ModuleQuasiIsoBaseChangeQuasiIso.QisoBC.D_succ_apply

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.ModuleQuasiIsoBaseChangeQuasiIso
universe u
open TensorProduct
namespace QisoBC
variable {S : Type u} [CommRing S]
variable (K : ℕ → Type u) [∀ i, AddCommGroup (K i)] [∀ i, Module S (K i)]
variable (C : ℕ → Type u) [∀ i, AddCommGroup (C i)] [∀ i, Module S (C i)]
variable (δ : ∀ i, K i →ₗ[S] K (i + 1)) (d : ∀ i, C i →ₗ[S] C (i + 1)) (φ : ∀ i, K i →ₗ[S] C i)

Lean source · statement

theorem D_succ_apply (i : ℕ) (z : K (i + 1) × C i) :
    (D K C δ d φ (i + 1) z : K (i + 2) × C (i + 1)) = (δ (i + 1) z.1, φ (i + 1) z.1 - d i z.2)

theorem

D_comp_D

L101 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.ModuleQuasiIsoBaseChangeQuasiIso.QisoBC.D_comp_D

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.ModuleQuasiIsoBaseChangeQuasiIso
universe u
open TensorProduct
namespace QisoBC
variable {S : Type u} [CommRing S]
variable (K : ℕ → Type u) [∀ i, AddCommGroup (K i)] [∀ i, Module S (K i)]
variable (C : ℕ → Type u) [∀ i, AddCommGroup (C i)] [∀ i, Module S (C i)]
variable (δ : ∀ i, K i →ₗ[S] K (i + 1)) (d : ∀ i, C i →ₗ[S] C (i + 1)) (φ : ∀ i, K i →ₗ[S] C i)

Lean source · full declaration

theorem D_comp_D (hδδ : ∀ i, δ (i + 1) ∘ₗ δ i = 0) (hdd : ∀ i, d (i + 1) ∘ₗ d i = 0)
    (hφ : ∀ i, d i ∘ₗ φ i = φ (i + 1) ∘ₗ δ i) : ∀ i, D K C δ d φ (i + 1) ∘ₗ D K C δ d φ i = 0
  | 0 => by
      refine LinearMap.ext fun (x : K 0) => ?_
      change ((δ 1 (δ 0 x), φ 1 (δ 0 x) - d 0 (φ 0 x)) : K 2 × C 1) = 0
      have h1 := congrArg (fun f => f x) (hδδ 0)
      have h2 := congrArg (fun f => f x) (hφ 0)
      simp only [LinearMap.comp_apply, LinearMap.zero_apply] at h1 h2
      rw [h1, h2, sub_self]; rfl
  | i + 1 => by
      refine LinearMap.ext fun z => ?_
      change ((δ (i + 2) (δ (i + 1) z.1), φ (i + 2) (δ (i + 1) z.1) - d (i + 1) (φ (i + 1) z.1 - d
        i z.2)) :
        K (i + 3) × C (i + 2)) = 0
      have h1 := congrArg (fun f => f z.1) (hδδ (i + 1))
      have h2 := congrArg (fun f => f z.1) (hφ (i + 1))
      have h3 := congrArg (fun f => f z.2) (hdd i)
      simp only [LinearMap.comp_apply, LinearMap.zero_apply] at h1 h2 h3
      rw [h1, map_sub, h3, h2, sub_zero, sub_self]; rfl

theorem

cone_exact

L121 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.ModuleQuasiIsoBaseChangeQuasiIso.QisoBC.cone_exact

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.ModuleQuasiIsoBaseChangeQuasiIso
universe u
open TensorProduct
namespace QisoBC
variable {S : Type u} [CommRing S]
variable (K : ℕ → Type u) [∀ i, AddCommGroup (K i)] [∀ i, Module S (K i)]
variable (C : ℕ → Type u) [∀ i, AddCommGroup (C i)] [∀ i, Module S (C i)]
variable (δ : ∀ i, K i →ₗ[S] K (i + 1)) (d : ∀ i, C i →ₗ[S] C (i + 1)) (φ : ∀ i, K i →ₗ[S] C i)

Lean source · statement

theorem cone_exact (hφ : ∀ i, d i ∘ₗ φ i = φ (i + 1) ∘ₗ δ i)
    (h0inj : ∀ x : K 0, δ 0 x = 0 → φ 0 x = 0 → x = 0)
    (h0surj : ∀ y : C 0, d 0 y = 0 → ∃ x : K 0, δ 0 x = 0 ∧ φ 0 x = y)
    (hinj : ∀ (i : ℕ) (x : K (i + 1)), δ (i + 1) x = 0 → φ (i + 1) x ∈ LinearMap.range (d i) →
      x ∈ LinearMap.range (δ i))
    (hsurj : ∀ (i : ℕ) (y : C (i + 1)), d (i + 1) y = 0 →
      ∃ x : K (i + 1), δ (i + 1) x = 0 ∧ φ (i + 1) x - y ∈ LinearMap.range (d i)) :
    LinearMap.ker (D K C δ d φ 0) = ⊥ ∧
      ∀ i, LinearMap.ker (D K C δ d φ (i + 1)) ≤ LinearMap.range (D K C δ d φ i)

theorem

qiso_of_cone_exact

L163 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.ModuleQuasiIsoBaseChangeQuasiIso.QisoBC.qiso_of_cone_exact

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.ModuleQuasiIsoBaseChangeQuasiIso
universe u
open TensorProduct
namespace QisoBC
variable {S : Type u} [CommRing S]
variable (K : ℕ → Type u) [∀ i, AddCommGroup (K i)] [∀ i, Module S (K i)]
variable (C : ℕ → Type u) [∀ i, AddCommGroup (C i)] [∀ i, Module S (C i)]
variable (δ : ∀ i, K i →ₗ[S] K (i + 1)) (d : ∀ i, C i →ₗ[S] C (i + 1)) (φ : ∀ i, K i →ₗ[S] C i)

Lean source · statement

theorem qiso_of_cone_exact (hex0 : LinearMap.ker (D K C δ d φ 0) = ⊥)
    (hex : ∀ i, LinearMap.ker (D K C δ d φ (i + 1)) ≤ LinearMap.range (D K C δ d φ i)) :
    (∀ x : K 0, δ 0 x = 0 → φ 0 x = 0 → x = 0) ∧
    (∀ y : C 0, d 0 y = 0 → ∃ x : K 0, δ 0 x = 0 ∧ φ 0 x = y) ∧
    (∀ (i : ℕ) (x : K (i + 1)), δ (i + 1) x = 0 → φ (i + 1) x ∈ LinearMap.range (d i) →
      x ∈ LinearMap.range (δ i)) ∧
    (∀ (i : ℕ) (y : C (i + 1)), d (i + 1) y = 0 →
      ∃ x : K (i + 1), δ (i + 1) x = 0 ∧ φ (i + 1) x - y ∈ LinearMap.range (d i))

theorem

exact_transfer

L213 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.ModuleQuasiIsoBaseChangeQuasiIso.QisoBC.exact_transfer

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.ModuleQuasiIsoBaseChangeQuasiIso
universe u
open TensorProduct
namespace QisoBC
variable {S : Type u} [CommRing S]
variable (K : ℕ → Type u) [∀ i, AddCommGroup (K i)] [∀ i, Module S (K i)]
variable (C : ℕ → Type u) [∀ i, AddCommGroup (C i)] [∀ i, Module S (C i)]
variable (δ : ∀ i, K i →ₗ[S] K (i + 1)) (d : ∀ i, C i →ₗ[S] C (i + 1)) (φ : ∀ i, K i →ₗ[S] C i)

Lean source · statement

theorem exact_transfer {A : Type u} [CommRing A] (E E' : ℕ → Type u)
    [∀ i, AddCommGroup (E i)] [∀ i, Module A (E i)] [∀ i, AddCommGroup (E' i)] [∀ i, Module A (E'
      i)]
    (D₁ : ∀ i, E i →ₗ[A] E (i + 1)) (D₂ : ∀ i, E' i →ₗ[A] E' (i + 1)) (e : ∀ i, E i ≃ₗ[A] E' i)
    (he : ∀ i z, e (i + 1) (D₁ i z) = D₂ i (e i z))
    (h0 : LinearMap.ker (D₁ 0) = ⊥) (hex : ∀ i, LinearMap.ker (D₁ (i + 1)) ≤ LinearMap.range (D₁
      i)) :
    LinearMap.ker (D₂ 0) = ⊥ ∧ ∀ i, LinearMap.ker (D₂ (i + 1)) ≤ LinearMap.range (D₂ i)

def

coneBC

L241 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.ModuleQuasiIsoBaseChangeQuasiIso.QisoBC.coneBC

Documentation

Tensoring the graded cone identifies it with the cone of the tensor products.

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.ModuleQuasiIsoBaseChangeQuasiIso
universe u
open TensorProduct
namespace QisoBC
variable {S : Type u} [CommRing S]
variable (K : ℕ → Type u) [∀ i, AddCommGroup (K i)] [∀ i, Module S (K i)]
variable (C : ℕ → Type u) [∀ i, AddCommGroup (C i)] [∀ i, Module S (C i)]
variable (δ : ∀ i, K i →ₗ[S] K (i + 1)) (d : ∀ i, C i →ₗ[S] C (i + 1)) (φ : ∀ i, K i →ₗ[S] C i)
section baseChange
variable {R : Type u} [CommRing R]
variable (K : ℕ → Type u) [∀ i, AddCommGroup (K i)] [∀ i, Module R (K i)]
variable (C : ℕ → Type u) [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)]
variable (A : Type u) [CommRing A] [Algebra R A]

Lean source · full declaration

def coneBC :
    ∀ i, A ⊗[R] Cone K C i ≃ₗ[A] Cone (fun j => A ⊗[R] K j) (fun j => A ⊗[R] C j) i
  | 0 => LinearEquiv.refl A (A ⊗[R] K 0)
  | i + 1 => TensorProduct.prodRight R A A (K (i + 1)) (C i)

theorem

coneBC_comm

L248 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.ModuleQuasiIsoBaseChangeQuasiIso.QisoBC.coneBC_comm

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.ModuleQuasiIsoBaseChangeQuasiIso
universe u
open TensorProduct
namespace QisoBC
variable {S : Type u} [CommRing S]
variable (K : ℕ → Type u) [∀ i, AddCommGroup (K i)] [∀ i, Module S (K i)]
variable (C : ℕ → Type u) [∀ i, AddCommGroup (C i)] [∀ i, Module S (C i)]
variable (δ : ∀ i, K i →ₗ[S] K (i + 1)) (d : ∀ i, C i →ₗ[S] C (i + 1)) (φ : ∀ i, K i →ₗ[S] C i)
section baseChange
variable {R : Type u} [CommRing R]
variable (K : ℕ → Type u) [∀ i, AddCommGroup (K i)] [∀ i, Module R (K i)]
variable (C : ℕ → Type u) [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)]
variable (A : Type u) [CommRing A] [Algebra R A]
variable (δ : ∀ i, K i →ₗ[R] K (i + 1)) (d : ∀ i, C i →ₗ[R] C (i + 1)) (φ : ∀ i, K i →ₗ[R] C i)

Lean source · full declaration

theorem coneBC_comm : ∀ (i : ℕ) (z : A ⊗[R] Cone K C i),
    coneBC K C A (i + 1) ((D K C δ d φ i).baseChange A z) =
      D (fun j => A ⊗[R] K j) (fun j => A ⊗[R] C j) (fun j => (δ j).baseChange A)
        (fun j => (d j).baseChange A) (fun j => (φ j).baseChange A) i (coneBC K C A i z)
  | 0, z => by
      induction z using TensorProduct.inductionOn with
      | add x y hx hy => simp only [map_add, hx, hy]
      | tmul a x =>
          change K 0 at x
          change TensorProduct.prodRight R A A (K 1) (C 0) (a ⊗ₜ[R] ((δ 0 x, φ 0 x) : K 1 × C 0)) =
            (((δ 0).baseChange A (a ⊗ₜ[R] x), (φ 0).baseChange A (a ⊗ₜ[R] x)) :
              (A ⊗[R] K 1) × (A ⊗[R] C 0))
          rfl
  | i + 1, z => by
      induction z using TensorProduct.inductionOn with
      | add x y hx hy => simp only [map_add, hx, hy]
      | tmul a z =>
          change K (i + 1) × C i at z
          change TensorProduct.prodRight R A A (K (i + 2)) (C (i + 1))
              (a ⊗ₜ[R] ((δ (i + 1) z.1, φ (i + 1) z.1 - d i z.2) : K (i + 2) × C (i + 1))) =
            (((δ (i + 1)).baseChange A (a ⊗ₜ[R] z.1),
              (φ (i + 1)).baseChange A (a ⊗ₜ[R] z.1) - (d i).baseChange A (a ⊗ₜ[R] z.2)) :
              (A ⊗[R] K (i + 2)) × (A ⊗[R] C (i + 1)))
          rw [TensorProduct.prodRight_tmul, LinearMap.baseChange_tmul, LinearMap.baseChange_tmul,
            LinearMap.baseChange_tmul, TensorProduct.tmul_sub]

theorem

quasiIso_baseChange_of_quasiIso_of_flat

L285 ↗

Module.quasiIso_baseChange_of_quasiIso_of_flat

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.ModuleQuasiIsoBaseChangeQuasiIso
universe u
open TensorProduct
attribute [local instance]
  QisoBC.instACG
attribute [local instance]
  QisoBC.instMod
open QisoBC in

Lean source · statement

theorem _root_.Module.quasiIso_baseChange_of_quasiIso_of_flat
    (R : Type u) [CommRing R]
    (K : ℕ → Type u) [∀ i, AddCommGroup (K i)] [∀ i, Module R (K i)] [∀ i, Module.Flat R (K i)]
    (δ : ∀ i, K i →ₗ[R] K (i + 1)) (hδδ : ∀ i, δ (i + 1) ∘ₗ δ i = 0)
    (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 : ℕ) (hKbdd : ∀ i, n < i → Subsingleton (K i)) (hCbdd : ∀ i, n < i → Subsingleton (C i))
    (φ : ∀ i, K i →ₗ[R] C i) (hφ : ∀ i, d i ∘ₗ φ i = φ (i + 1) ∘ₗ δ i)
    (h0inj : ∀ x : K 0, δ 0 x = 0 → φ 0 x = 0 → x = 0)
    (h0surj : ∀ y : C 0, d 0 y = 0 → ∃ x : K 0, δ 0 x = 0 ∧ φ 0 x = y)
    (hinj : ∀ (i : ℕ) (x : K (i + 1)), δ (i + 1) x = 0 → φ (i + 1) x ∈ LinearMap.range (d i) →
      x ∈ LinearMap.range (δ i))
    (hsurj : ∀ (i : ℕ) (y : C (i + 1)), d (i + 1) y = 0 →
      ∃ x : K (i + 1), δ (i + 1) x = 0 ∧ φ (i + 1) x - y ∈ LinearMap.range (d i))
    (A : Type u) [CommRing A] [Algebra R A] :
    (∀ x : A ⊗[R] K 0, (δ 0).baseChange A x = 0 → (φ 0).baseChange A x = 0 → x = 0) ∧
    (∀ y : A ⊗[R] C 0, (d 0).baseChange A y = 0 →
      ∃ x : A ⊗[R] K 0, (δ 0).baseChange A x = 0 ∧ (φ 0).baseChange A x = y) ∧
    (∀ (i : ℕ) (x : A ⊗[R] K (i + 1)), (δ (i + 1)).baseChange A x = 0 →
      (φ (i + 1)).baseChange A x ∈ LinearMap.range ((d i).baseChange A) →
        x ∈ LinearMap.range ((δ i).baseChange A)) ∧
    (∀ (i : ℕ) (y : A ⊗[R] C (i + 1)), (d (i + 1)).baseChange A y = 0 →
      ∃ x : A ⊗[R] K (i + 1), (δ (i + 1)).baseChange A x = 0 ∧
        (φ (i + 1)).baseChange A x - y ∈ LinearMap.range ((d i).baseChange A))

Module documentation

Module quasi Iso base Change of quasi Iso of flat

Declarations