Module

Module_IsDirectLimit_exists_invertible_linearEquiv_baseChange.lean

Nyll.AlgebraicCurves.Foundations.Algebra.Module_IsDirectLimit_exists_invertible_linearEquiv_baseChange

27 declarations indexed from sourceView source ↗

Module documentation

Descent of invertible modules along direct limits

Descends invertibility and linear equivalences after base change to a finite stage.

Imports26

Mathlib.Algebra.Colimit.DirectLimit
Mathlib.Algebra.Colimit.Module
Mathlib.Algebra.Module.Equiv.Basic
Mathlib.Algebra.Module.LinearMap.Defs
Mathlib.Algebra.Module.FinitePresentation
Mathlib.Data.Finset.Order
Mathlib.Order.Directed
Mathlib.LinearAlgebra.Finsupp.LinearCombination
Mathlib.LinearAlgebra.Pi
Mathlib.LinearAlgebra.Quotient.Defs
Mathlib.LinearAlgebra.Quotient.Basic
Mathlib.LinearAlgebra.TensorProduct.Defs
Mathlib.LinearAlgebra.TensorProduct.Basic
Mathlib.LinearAlgebra.TensorProduct.Map
Mathlib.LinearAlgebra.TensorProduct.DirectLimit
Mathlib.LinearAlgebra.TensorProduct.Pi
Mathlib.LinearAlgebra.TensorProduct.Quotient
Mathlib.LinearAlgebra.TensorProduct.RightExactness
Mathlib.LinearAlgebra.TensorProduct.Tower
Mathlib.RingTheory.Finiteness.Defs
Mathlib.RingTheory.Finiteness.Basic
Mathlib.RingTheory.TensorProduct.Basic
Mathlib.RingTheory.TensorProduct.Finite
Mathlib.RingTheory.PicardGroup
Mathlib.Tactic.Choose
Mathlib.Tactic.Ext

Imported by2

theorem

rTensor_algHom_smul

L60 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_IsDirectLimit_exists_invertible_linearEquiv_baseChange.S17LFP.rTensor_algHom_smul

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_IsDirectLimit_exists_invertible_linearEquiv_baseChange
open TensorProduct
namespace S17LFP
section Helpers
variable {R : Type*} [CommRing R] {S T : Type*} [CommRing S] [CommRing T] [Algebra R
  S] [Algebra R T]

Lean source · statement

theorem rTensor_algHom_smul (σ : S →ₐ[R] T) (Q : Type*) [AddCommGroup Q] [Module R Q]
    (b : S) (z : S ⊗[R] Q) :
    σ.toLinearMap.rTensor Q (b • z) = σ b • σ.toLinearMap.rTensor Q z

theorem

ext_one_tmul

L67 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_IsDirectLimit_exists_invertible_linearEquiv_baseChange.S17LFP.ext_one_tmul

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_IsDirectLimit_exists_invertible_linearEquiv_baseChange
open TensorProduct
namespace S17LFP
section Helpers
variable {R : Type*} [CommRing R] {S T : Type*} [CommRing S] [CommRing T] [Algebra R
  S] [Algebra R T]

Lean source · statement

theorem ext_one_tmul {P N : Type*} [AddCommGroup P] [Module R P] [AddCommGroup N] [Module R N]
    [Module S N] [IsScalarTower R S N]
    {f₁ f₂ : S ⊗[R] P →ₗ[S] N} (h : ∀ p, f₁ (1 ⊗ₜ p) = f₂ (1 ⊗ₜ p)) : f₁ = f₂

theorem

rTensor_comp_apply_tmul

L75 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_IsDirectLimit_exists_invertible_linearEquiv_baseChange.S17LFP.rTensor_comp_apply_tmul

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_IsDirectLimit_exists_invertible_linearEquiv_baseChange
open TensorProduct
namespace S17LFP
section Helpers
variable {R : Type*} [CommRing R] {S T : Type*} [CommRing S] [CommRing T] [Algebra R
  S] [Algebra R T]

Lean source · statement

theorem rTensor_comp_apply_tmul (σ : S →ₐ[R] T) {P Q : Type*} [AddCommGroup P] [Module R P]
    [AddCommGroup Q] [Module R Q] (ξ : S ⊗[R] P →ₗ[S] S ⊗[R] Q) (b : S) (p : P) :
    (σ.toLinearMap.rTensor Q ∘ₗ ξ.restrictScalars R) (b ⊗ₜ p) =
      σ b • σ.toLinearMap.rTensor Q (ξ (1 ⊗ₜ p))

theorem

comp_rTensor_apply_tmul

L82 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_IsDirectLimit_exists_invertible_linearEquiv_baseChange.S17LFP.comp_rTensor_apply_tmul

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_IsDirectLimit_exists_invertible_linearEquiv_baseChange
open TensorProduct
namespace S17LFP
section Helpers
variable {R : Type*} [CommRing R] {S T : Type*} [CommRing S] [CommRing T] [Algebra R
  S] [Algebra R T]

Lean source · statement

theorem comp_rTensor_apply_tmul (σ : S →ₐ[R] T) {P N : Type*} [AddCommGroup P] [Module R P]
    [AddCommGroup N] [Module R N] [Module T N] [IsScalarTower R T N]
    (ξ : T ⊗[R] P →ₗ[T] N) (b : S) (p : P) :
    (ξ.restrictScalars R ∘ₗ σ.toLinearMap.rTensor P) (b ⊗ₜ p) = σ b • ξ (1 ⊗ₜ p)

theorem

rTensor_liftBaseChange_tmul

L90 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_IsDirectLimit_exists_invertible_linearEquiv_baseChange.S17LFP.rTensor_liftBaseChange_tmul

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_IsDirectLimit_exists_invertible_linearEquiv_baseChange
open TensorProduct
namespace S17LFP
section Helpers
variable {R : Type*} [CommRing R] {S T : Type*} [CommRing S] [CommRing T] [Algebra R
  S] [Algebra R T]

Lean source · statement

theorem rTensor_liftBaseChange_tmul (σ : S →ₐ[R] T) {P Q : Type*} [AddCommGroup P] [Module R P]
    [AddCommGroup Q] [Module R Q] (u : P →ₗ[R] S ⊗[R] Q) (b : S) (p : P) :
    σ.toLinearMap.rTensor Q (u.liftBaseChange S (b ⊗ₜ p)) = σ b •
      σ.toLinearMap.rTensor Q (u p)

theorem

finitePresentation_tensorProduct

L96 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_IsDirectLimit_exists_invertible_linearEquiv_baseChange.S17LFP.finitePresentation_tensorProduct

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_IsDirectLimit_exists_invertible_linearEquiv_baseChange
open TensorProduct
namespace S17LFP
section Helpers
variable {R : Type*} [CommRing R] {S T : Type*} [CommRing S] [CommRing T] [Algebra R
  S] [Algebra R T]

Lean source · statement

theorem finitePresentation_tensorProduct (M N : Type*) [AddCommGroup M] [Module R M]
    [AddCommGroup N] [Module R N] [Module.FinitePresentation R M] [Module.FinitePresentation R N] :
    Module.FinitePresentation R (M ⊗[R] N)

theorem

exists_ge_ge

L121 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_IsDirectLimit_exists_invertible_linearEquiv_baseChange.S17LFP.exists_ge_ge

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_IsDirectLimit_exists_invertible_linearEquiv_baseChange
open TensorProduct
namespace S17LFP
section Cocone
variable {R : Type*} [CommRing R] {ι : Type*} [Preorder ι] [Nonempty ι] [IsDirectedOrder ι]
  {G : ι → Type*} [∀ i, AddCommGroup (G i)] [∀ i, Module R (G i)]
  (t : ∀ i j, i ≤ j → G i →ₗ[R] G j)
  {A : Type*} [AddCommGroup A] [Module R A] (ψ : ∀ i, G i →ₗ[R] A)
omit [Nonempty ι] in

Lean source · statement

theorem exists_ge_ge (i j : ι) : ∃ k, i ≤ k ∧ j ≤ k

theorem

cocone_rTensor_surj

L123 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_IsDirectLimit_exists_invertible_linearEquiv_baseChange.S17LFP.cocone_rTensor_surj

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_IsDirectLimit_exists_invertible_linearEquiv_baseChange
open TensorProduct
namespace S17LFP
section Cocone
variable {R : Type*} [CommRing R] {ι : Type*} [Preorder ι] [Nonempty ι] [IsDirectedOrder ι]
  {G : ι → Type*} [∀ i, AddCommGroup (G i)] [∀ i, Module R (G i)]
  (t : ∀ i j, i ≤ j → G i →ₗ[R] G j)
  {A : Type*} [AddCommGroup A] [Module R A] (ψ : ∀ i, G i →ₗ[R] A)
omit [Nonempty ι] in

Lean source · statement

theorem cocone_rTensor_surj (hψ : ∀ i j (h : i ≤ j) x, ψ j (t i j h x) = ψ i x)
    (hsurj : ∀ a, ∃ i x, ψ i x = a) (Q : Type*) [AddCommGroup Q] [Module R Q]
    (z : A ⊗[R] Q) : ∃ (i : ι) (x : G i ⊗[R] Q), (ψ i).rTensor Q x = z

theorem

lift_bijective

L139 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_IsDirectLimit_exists_invertible_linearEquiv_baseChange.S17LFP.lift_bijective

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_IsDirectLimit_exists_invertible_linearEquiv_baseChange
open TensorProduct
namespace S17LFP
section Cocone
variable {R : Type*} [CommRing R] {ι : Type*} [Preorder ι] [Nonempty ι] [IsDirectedOrder ι]
  {G : ι → Type*} [∀ i, AddCommGroup (G i)] [∀ i, Module R (G i)]
  (t : ∀ i j, i ≤ j → G i →ₗ[R] G j)
  {A : Type*} [AddCommGroup A] [Module R A] (ψ : ∀ i, G i →ₗ[R] A)

Lean source · statement

theorem lift_bijective [DecidableEq ι] (hψ : ∀ i j (h : i ≤ j) x, ψ j (t i j h x) = ψ i x)
    (hsurj : ∀ a, ∃ i x, ψ i x = a)
    (hzero : ∀ i x, ψ i x = 0 → ∃ (j : ι) (h : i ≤ j), t i j h x = 0) :
    Function.Bijective (Module.DirectLimit.lift R ι G t ψ hψ)

theorem

cocone_rTensor_zero

L154 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_IsDirectLimit_exists_invertible_linearEquiv_baseChange.S17LFP.cocone_rTensor_zero

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_IsDirectLimit_exists_invertible_linearEquiv_baseChange
open TensorProduct
namespace S17LFP
section Cocone
variable {R : Type*} [CommRing R] {ι : Type*} [Preorder ι] [Nonempty ι] [IsDirectedOrder ι]
  {G : ι → Type*} [∀ i, AddCommGroup (G i)] [∀ i, Module R (G i)]
  (t : ∀ i j, i ≤ j → G i →ₗ[R] G j)
  {A : Type*} [AddCommGroup A] [Module R A] (ψ : ∀ i, G i →ₗ[R] A)

Lean source · statement

theorem cocone_rTensor_zero [DirectedSystem G (t · · ·)]
    (hψ : ∀ i j (h : i ≤ j) x, ψ j (t i j h x) = ψ i x)
    (hsurj : ∀ a, ∃ i x, ψ i x = a)
    (hzero : ∀ i x, ψ i x = 0 → ∃ (j : ι) (h : i ≤ j), t i j h x = 0)
    (Q : Type*) [AddCommGroup Q] [Module R Q] (i : ι) (x : G i ⊗[R] Q)
    (hx : (ψ i).rTensor Q x = 0) : ∃ (j : ι) (h : i ≤ j), (t i j h).rTensor Q x = 0

theorem

exists_comp_eq_of_finite

L173 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_IsDirectLimit_exists_invertible_linearEquiv_baseChange.S17LFP.exists_comp_eq_of_finite

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_IsDirectLimit_exists_invertible_linearEquiv_baseChange
open TensorProduct
namespace S17LFP
section Cocone
variable {R : Type*} [CommRing R] {ι : Type*} [Preorder ι] [Nonempty ι] [IsDirectedOrder ι]
  {G : ι → Type*} [∀ i, AddCommGroup (G i)] [∀ i, Module R (G i)]
  (t : ∀ i j, i ≤ j → G i →ₗ[R] G j)
  {A : Type*} [AddCommGroup A] [Module R A] (ψ : ∀ i, G i →ₗ[R] A)

Lean source · statement

theorem exists_comp_eq_of_finite [DirectedSystem G (t · · ·)]
    (hzero : ∀ i x, ψ i x = 0 → ∃ (j : ι) (h : i ≤ j), t i j h x = 0)
    {M : Type*} [AddCommGroup M] [Module R M] [Module.Finite R M]
    {i : ι} (u v : M →ₗ[R] G i) (huv : ψ i ∘ₗ u = ψ i ∘ₗ v) :
    ∃ (j : ι) (hij : i ≤ j), t i j hij ∘ₗ u = t i j hij ∘ₗ v

theorem

exists_factor_of_finitePresentation

L196 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_IsDirectLimit_exists_invertible_linearEquiv_baseChange.S17LFP.exists_factor_of_finitePresentation

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_IsDirectLimit_exists_invertible_linearEquiv_baseChange
open TensorProduct
namespace S17LFP
section Cocone
variable {R : Type*} [CommRing R] {ι : Type*} [Preorder ι] [Nonempty ι] [IsDirectedOrder ι]
  {G : ι → Type*} [∀ i, AddCommGroup (G i)] [∀ i, Module R (G i)]
  (t : ∀ i j, i ≤ j → G i →ₗ[R] G j)
  {A : Type*} [AddCommGroup A] [Module R A] (ψ : ∀ i, G i →ₗ[R] A)

Lean source · statement

theorem exists_factor_of_finitePresentation [DirectedSystem G (t · · ·)]
    (hψ : ∀ i j (h : i ≤ j) x, ψ j (t i j h x) = ψ i x)
    (hsurj : ∀ a, ∃ i x, ψ i x = a)
    (hzero : ∀ i x, ψ i x = 0 → ∃ (j : ι) (h : i ≤ j), t i j h x = 0)
    {M : Type*} [AddCommGroup M] [Module R M] [Module.FinitePresentation R M]
    (φ : M →ₗ[R] A) : ∃ (i : ι) (u : M →ₗ[R] G i), ψ i ∘ₗ u = φ

theorem

directedSystem_linear

L249 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_IsDirectLimit_exists_invertible_linearEquiv_baseChange.S17LFP.directedSystem_linear

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_IsDirectLimit_exists_invertible_linearEquiv_baseChange
open TensorProduct
namespace S17LFP
section Descent
universe u v w
variable {ι : Type v} [Preorder ι] [IsDirectedOrder ι] [Nonempty ι]
  {B₀ : Type u} [CommRing B₀]
  (B : ι → Type u) [∀ i, CommRing (B i)] [∀ i, Algebra B₀ (B i)]
  (τ : ∀ i j, i ≤ j → B i →ₐ[B₀] B j) [DirectedSystem B (fun i j h => τ i j h)]
  (Bω : Type u) [CommRing Bω] [Algebra B₀ Bω] (g : ∀ i, B i →ₐ[B₀] Bω)
  (hg : ∀ i j (h : i ≤ j), (g j).comp (τ i j h) = g i)
  (hsurj : ∀ b : Bω, ∃ i x, g i x = b)
  (hzero : ∀ i (x : B i), g i x = 0 → ∃ (j : ι) (h : i ≤ j), τ i j h x = 0)
  (P Q : Type*) [AddCommGroup P] [Module B₀ P] [AddCommGroup Q] [Module B₀ Q]
omit [IsDirectedOrder ι] [Nonempty ι] in

Lean source · full declaration

theorem directedSystem_linear : DirectedSystem B (fun i j h => (τ i j h).toLinearMap) :=
  ⟨fun _ x => DirectedSystem.map_self (f := fun i j h => ⇑(τ i j h)) x,
    fun _ _ _ h₁ h₂ x => DirectedSystem.map_map (f := fun i j h => ⇑(τ i j h)) h₁ h₂ x⟩

theorem

rTensor_self

L253 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_IsDirectLimit_exists_invertible_linearEquiv_baseChange.S17LFP.rTensor_self

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_IsDirectLimit_exists_invertible_linearEquiv_baseChange
open TensorProduct
namespace S17LFP
section Descent
universe u v w
variable {ι : Type v} [Preorder ι] [IsDirectedOrder ι] [Nonempty ι]
  {B₀ : Type u} [CommRing B₀]
  (B : ι → Type u) [∀ i, CommRing (B i)] [∀ i, Algebra B₀ (B i)]
  (τ : ∀ i j, i ≤ j → B i →ₐ[B₀] B j) [DirectedSystem B (fun i j h => τ i j h)]
  (Bω : Type u) [CommRing Bω] [Algebra B₀ Bω] (g : ∀ i, B i →ₐ[B₀] Bω)
  (hg : ∀ i j (h : i ≤ j), (g j).comp (τ i j h) = g i)
  (hsurj : ∀ b : Bω, ∃ i x, g i x = b)
  (hzero : ∀ i (x : B i), g i x = 0 → ∃ (j : ι) (h : i ≤ j), τ i j h x = 0)
  (P Q : Type*) [AddCommGroup P] [Module B₀ P] [AddCommGroup Q] [Module B₀ Q]
omit [IsDirectedOrder ι] [Nonempty ι] in

Lean source · statement

theorem rTensor_self (i : ι) {M : Type*} [AddCommGroup M] [Module B₀ M] (z : B i ⊗[B₀] M) :
    (τ i i le_rfl).toLinearMap.rTensor M z = z

theorem

glin_comp

L263 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_IsDirectLimit_exists_invertible_linearEquiv_baseChange.S17LFP.glin_comp

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_IsDirectLimit_exists_invertible_linearEquiv_baseChange
open TensorProduct
namespace S17LFP
section Descent
universe u v w
variable {ι : Type v} [Preorder ι] [IsDirectedOrder ι] [Nonempty ι]
  {B₀ : Type u} [CommRing B₀]
  (B : ι → Type u) [∀ i, CommRing (B i)] [∀ i, Algebra B₀ (B i)]
  (τ : ∀ i j, i ≤ j → B i →ₐ[B₀] B j) [DirectedSystem B (fun i j h => τ i j h)]
  (Bω : Type u) [CommRing Bω] [Algebra B₀ Bω] (g : ∀ i, B i →ₐ[B₀] Bω)
  (hg : ∀ i j (h : i ≤ j), (g j).comp (τ i j h) = g i)
  (hsurj : ∀ b : Bω, ∃ i x, g i x = b)
  (hzero : ∀ i (x : B i), g i x = 0 → ∃ (j : ι) (h : i ≤ j), τ i j h x = 0)
  (P Q : Type*) [AddCommGroup P] [Module B₀ P] [AddCommGroup Q] [Module B₀ Q]
omit [DirectedSystem B (fun i j h => τ i j h)] [IsDirectedOrder ι] [Nonempty ι] in
include hg in

Lean source · statement

theorem glin_comp (k l : ι) (h : k ≤ l) :
    (g l).toLinearMap ∘ₗ (τ k l h).toLinearMap = (g k).toLinearMap

theorem

glin_compat

L268 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_IsDirectLimit_exists_invertible_linearEquiv_baseChange.S17LFP.glin_compat

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_IsDirectLimit_exists_invertible_linearEquiv_baseChange
open TensorProduct
namespace S17LFP
section Descent
universe u v w
variable {ι : Type v} [Preorder ι] [IsDirectedOrder ι] [Nonempty ι]
  {B₀ : Type u} [CommRing B₀]
  (B : ι → Type u) [∀ i, CommRing (B i)] [∀ i, Algebra B₀ (B i)]
  (τ : ∀ i j, i ≤ j → B i →ₐ[B₀] B j) [DirectedSystem B (fun i j h => τ i j h)]
  (Bω : Type u) [CommRing Bω] [Algebra B₀ Bω] (g : ∀ i, B i →ₐ[B₀] Bω)
  (hg : ∀ i j (h : i ≤ j), (g j).comp (τ i j h) = g i)
  (hsurj : ∀ b : Bω, ∃ i x, g i x = b)
  (hzero : ∀ i (x : B i), g i x = 0 → ∃ (j : ι) (h : i ≤ j), τ i j h x = 0)
  (P Q : Type*) [AddCommGroup P] [Module B₀ P] [AddCommGroup Q] [Module B₀ Q]
omit [DirectedSystem B (fun i j h => τ i j h)] [IsDirectedOrder ι] [Nonempty ι] in
include hg in

Lean source · statement

theorem glin_compat : ∀ k l (h : k ≤ l) (x : B k),
    (g l).toLinearMap ((τ k l h).toLinearMap x) = (g k).toLinearMap x

theorem

gQ_compat

L273 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_IsDirectLimit_exists_invertible_linearEquiv_baseChange.S17LFP.gQ_compat

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_IsDirectLimit_exists_invertible_linearEquiv_baseChange
open TensorProduct
namespace S17LFP
section Descent
universe u v w
variable {ι : Type v} [Preorder ι] [IsDirectedOrder ι] [Nonempty ι]
  {B₀ : Type u} [CommRing B₀]
  (B : ι → Type u) [∀ i, CommRing (B i)] [∀ i, Algebra B₀ (B i)]
  (τ : ∀ i j, i ≤ j → B i →ₐ[B₀] B j) [DirectedSystem B (fun i j h => τ i j h)]
  (Bω : Type u) [CommRing Bω] [Algebra B₀ Bω] (g : ∀ i, B i →ₐ[B₀] Bω)
  (hg : ∀ i j (h : i ≤ j), (g j).comp (τ i j h) = g i)
  (hsurj : ∀ b : Bω, ∃ i x, g i x = b)
  (hzero : ∀ i (x : B i), g i x = 0 → ∃ (j : ι) (h : i ≤ j), τ i j h x = 0)
  (P Q : Type*) [AddCommGroup P] [Module B₀ P] [AddCommGroup Q] [Module B₀ Q]
omit [DirectedSystem B (fun i j h => τ i j h)] [IsDirectedOrder ι] [Nonempty ι] in
include hg in

Lean source · statement

theorem gQ_compat (Q : Type*) [AddCommGroup Q] [Module B₀ Q] : ∀ k l (h : k ≤ l) (x : B k ⊗[B₀] Q),
    (g l).toLinearMap.rTensor Q ((τ k l h).toLinearMap.rTensor Q x) = (g
      k).toLinearMap.rTensor Q x

theorem

gQ_surj

L281 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_IsDirectLimit_exists_invertible_linearEquiv_baseChange.S17LFP.gQ_surj

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_IsDirectLimit_exists_invertible_linearEquiv_baseChange
open TensorProduct
namespace S17LFP
section Descent
universe u v w
variable {ι : Type v} [Preorder ι] [IsDirectedOrder ι] [Nonempty ι]
  {B₀ : Type u} [CommRing B₀]
  (B : ι → Type u) [∀ i, CommRing (B i)] [∀ i, Algebra B₀ (B i)]
  (τ : ∀ i j, i ≤ j → B i →ₐ[B₀] B j) [DirectedSystem B (fun i j h => τ i j h)]
  (Bω : Type u) [CommRing Bω] [Algebra B₀ Bω] (g : ∀ i, B i →ₐ[B₀] Bω)
  (hg : ∀ i j (h : i ≤ j), (g j).comp (τ i j h) = g i)
  (hsurj : ∀ b : Bω, ∃ i x, g i x = b)
  (hzero : ∀ i (x : B i), g i x = 0 → ∃ (j : ι) (h : i ≤ j), τ i j h x = 0)
  (P Q : Type*) [AddCommGroup P] [Module B₀ P] [AddCommGroup Q] [Module B₀ Q]
include hg hsurj in
omit [DirectedSystem B (fun i j h => τ i j h)] in
omit [Nonempty ι] in

Lean source · statement

theorem gQ_surj (Q : Type*) [AddCommGroup Q] [Module B₀ Q] :
    ∀ z : Bω ⊗[B₀] Q, ∃ (i : ι) (x : B i ⊗[B₀] Q), (g i).toLinearMap.rTensor Q x = z

theorem

gQ_zero

L286 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_IsDirectLimit_exists_invertible_linearEquiv_baseChange.S17LFP.gQ_zero

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_IsDirectLimit_exists_invertible_linearEquiv_baseChange
open TensorProduct
namespace S17LFP
section Descent
universe u v w
variable {ι : Type v} [Preorder ι] [IsDirectedOrder ι] [Nonempty ι]
  {B₀ : Type u} [CommRing B₀]
  (B : ι → Type u) [∀ i, CommRing (B i)] [∀ i, Algebra B₀ (B i)]
  (τ : ∀ i j, i ≤ j → B i →ₐ[B₀] B j) [DirectedSystem B (fun i j h => τ i j h)]
  (Bω : Type u) [CommRing Bω] [Algebra B₀ Bω] (g : ∀ i, B i →ₐ[B₀] Bω)
  (hg : ∀ i j (h : i ≤ j), (g j).comp (τ i j h) = g i)
  (hsurj : ∀ b : Bω, ∃ i x, g i x = b)
  (hzero : ∀ i (x : B i), g i x = 0 → ∃ (j : ι) (h : i ≤ j), τ i j h x = 0)
  (P Q : Type*) [AddCommGroup P] [Module B₀ P] [AddCommGroup Q] [Module B₀ Q]
include hg hsurj hzero in

Lean source · statement

theorem gQ_zero (Q : Type*) [AddCommGroup Q] [Module B₀ Q] :
    ∀ (i : ι) (x : B i ⊗[B₀] Q), (g i).toLinearMap.rTensor Q x = 0 →
      ∃ (j : ι) (h : i ≤ j), (τ i j h).toLinearMap.rTensor Q x = 0

theorem

hom_inj

L293 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_IsDirectLimit_exists_invertible_linearEquiv_baseChange.S17LFP.hom_inj

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_IsDirectLimit_exists_invertible_linearEquiv_baseChange
open TensorProduct
namespace S17LFP
section Descent
universe u v w
variable {ι : Type v} [Preorder ι] [IsDirectedOrder ι] [Nonempty ι]
  {B₀ : Type u} [CommRing B₀]
  (B : ι → Type u) [∀ i, CommRing (B i)] [∀ i, Algebra B₀ (B i)]
  (τ : ∀ i j, i ≤ j → B i →ₐ[B₀] B j) [DirectedSystem B (fun i j h => τ i j h)]
  (Bω : Type u) [CommRing Bω] [Algebra B₀ Bω] (g : ∀ i, B i →ₐ[B₀] Bω)
  (hg : ∀ i j (h : i ≤ j), (g j).comp (τ i j h) = g i)
  (hsurj : ∀ b : Bω, ∃ i x, g i x = b)
  (hzero : ∀ i (x : B i), g i x = 0 → ∃ (j : ι) (h : i ≤ j), τ i j h x = 0)
  (P Q : Type*) [AddCommGroup P] [Module B₀ P] [AddCommGroup Q] [Module B₀ Q]
include hg hsurj hzero in

Lean source · statement

theorem hom_inj [Module.Finite B₀ P] (i : ι) (φ φ' : B i ⊗[B₀] P →ₗ[B i] B i ⊗[B₀] Q)
    (h : (g i).toLinearMap.rTensor Q ∘ₗ φ.restrictScalars B₀ =
      (g i).toLinearMap.rTensor Q ∘ₗ φ'.restrictScalars B₀) :
    ∃ (j : ι) (h : i ≤ j),
      (τ i j h).toLinearMap.rTensor Q ∘ₗ φ.restrictScalars B₀ =
        (τ i j h).toLinearMap.rTensor Q ∘ₗ φ'.restrictScalars B₀

theorem

hom_surj

L312 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_IsDirectLimit_exists_invertible_linearEquiv_baseChange.S17LFP.hom_surj

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_IsDirectLimit_exists_invertible_linearEquiv_baseChange
open TensorProduct
namespace S17LFP
section Descent
universe u v w
variable {ι : Type v} [Preorder ι] [IsDirectedOrder ι] [Nonempty ι]
  {B₀ : Type u} [CommRing B₀]
  (B : ι → Type u) [∀ i, CommRing (B i)] [∀ i, Algebra B₀ (B i)]
  (τ : ∀ i j, i ≤ j → B i →ₐ[B₀] B j) [DirectedSystem B (fun i j h => τ i j h)]
  (Bω : Type u) [CommRing Bω] [Algebra B₀ Bω] (g : ∀ i, B i →ₐ[B₀] Bω)
  (hg : ∀ i j (h : i ≤ j), (g j).comp (τ i j h) = g i)
  (hsurj : ∀ b : Bω, ∃ i x, g i x = b)
  (hzero : ∀ i (x : B i), g i x = 0 → ∃ (j : ι) (h : i ≤ j), τ i j h x = 0)
  (P Q : Type*) [AddCommGroup P] [Module B₀ P] [AddCommGroup Q] [Module B₀ Q]
include hg hsurj hzero in

Lean source · statement

theorem hom_surj [Module.FinitePresentation B₀ P] (φ : Bω ⊗[B₀] P →ₗ[Bω] Bω ⊗[B₀] Q) :
    ∃ (i : ι) (φᵢ : B i ⊗[B₀] P →ₗ[B i] B i ⊗[B₀] Q),
      φ.restrictScalars B₀ ∘ₗ (g i).toLinearMap.rTensor P =
        (g i).toLinearMap.rTensor Q ∘ₗ φᵢ.restrictScalars B₀

theorem

iso_desc

L328 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_IsDirectLimit_exists_invertible_linearEquiv_baseChange.S17LFP.iso_desc

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_IsDirectLimit_exists_invertible_linearEquiv_baseChange
open TensorProduct
namespace S17LFP
section Descent
universe u v w
variable {ι : Type v} [Preorder ι] [IsDirectedOrder ι] [Nonempty ι]
  {B₀ : Type u} [CommRing B₀]
  (B : ι → Type u) [∀ i, CommRing (B i)] [∀ i, Algebra B₀ (B i)]
  (τ : ∀ i j, i ≤ j → B i →ₐ[B₀] B j) [DirectedSystem B (fun i j h => τ i j h)]
  (Bω : Type u) [CommRing Bω] [Algebra B₀ Bω] (g : ∀ i, B i →ₐ[B₀] Bω)
  (hg : ∀ i j (h : i ≤ j), (g j).comp (τ i j h) = g i)
  (hsurj : ∀ b : Bω, ∃ i x, g i x = b)
  (hzero : ∀ i (x : B i), g i x = 0 → ∃ (j : ι) (h : i ≤ j), τ i j h x = 0)
  (P Q : Type*) [AddCommGroup P] [Module B₀ P] [AddCommGroup Q] [Module B₀ Q]
include hg hsurj hzero in

Lean source · statement

theorem iso_desc [Module.FinitePresentation B₀ P] [Module.FinitePresentation B₀ Q]
    (e : Bω ⊗[B₀] P ≃ₗ[Bω] Bω ⊗[B₀] Q) :
    ∃ (i : ι) (eᵢ : B i ⊗[B₀] P ≃ₗ[B i] B i ⊗[B₀] Q),
      (e : _ →ₗ[Bω] _).restrictScalars B₀ ∘ₗ (g i).toLinearMap.rTensor P =
        (g i).toLinearMap.rTensor Q ∘ₗ (eᵢ : _ →ₗ[B i] _).restrictScalars B₀

theorem

obj

L443 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_IsDirectLimit_exists_invertible_linearEquiv_baseChange.S17LFP.obj

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_IsDirectLimit_exists_invertible_linearEquiv_baseChange
open TensorProduct
namespace S17LFP
section Descent
universe u v w
variable {ι : Type v} [Preorder ι] [IsDirectedOrder ι] [Nonempty ι]
  {B₀ : Type u} [CommRing B₀]
  (B : ι → Type u) [∀ i, CommRing (B i)] [∀ i, Algebra B₀ (B i)]
  (τ : ∀ i j, i ≤ j → B i →ₐ[B₀] B j) [DirectedSystem B (fun i j h => τ i j h)]
  (Bω : Type u) [CommRing Bω] [Algebra B₀ Bω] (g : ∀ i, B i →ₐ[B₀] Bω)
  (hg : ∀ i j (h : i ≤ j), (g j).comp (τ i j h) = g i)
  (hsurj : ∀ b : Bω, ∃ i x, g i x = b)
  (hzero : ∀ i (x : B i), g i x = 0 → ∃ (j : ι) (h : i ≤ j), τ i j h x = 0)
  (P Q : Type*) [AddCommGroup P] [Module B₀ P] [AddCommGroup Q] [Module B₀ Q]
omit [DirectedSystem B (fun i j h => τ i j h)] in
include hg hsurj in

Lean source · full declaration

theorem obj (Y : Type w) [AddCommGroup Y] [Module Bω Y] [Module.FinitePresentation Bω Y] :
    ∃ (i : ι) (Pᵢ : Type u) (_ : AddCommGroup Pᵢ) (_ : Module (B i) Pᵢ),
      Module.FinitePresentation (B i) Pᵢ ∧
      Nonempty (letI := (g i).toRingHom.toAlgebra; Bω ⊗[B i] Pᵢ ≃ₗ[Bω] Y) := by
  classical
  obtain ⟨n, K, e, hK⟩ := Module.FinitePresentation.exists_fin Bω Y
  obtain ⟨m, v, hv⟩ := Submodule.fg_iff_exists_fin_generating_family.mp hK
  choose i₀ x₀ hx₀ using fun a : Fin m × Fin n => hsurj (v a.1 a.2)
  obtain ⟨i, hi⟩ := Finset.exists_le (Finset.univ.image i₀)
  have hle : ∀ a, i₀ a ≤ i := fun a => hi _ (Finset.mem_image_of_mem _ (Finset.mem_univ a))
  let y : Fin m → (Fin n → B i) := fun a k => τ (i₀ (a, k)) i (hle _) (x₀ (a, k))
  have hy : ∀ a k, g i (y a k) = v a k := fun a k => by
    simp only [y]
    rw [← AlgHom.comp_apply, hg]
    exact hx₀ (a, k)
  let Kᵢ : Submodule (B i) (Fin n → B i) := Submodule.span (B i) (Set.range y)
  let : Algebra (B i) Bω := (g i).toRingHom.toAlgebra
  have halg : ∀ b : B i, algebraMap (B i) Bω b = g i b := fun b => rfl
  refine ⟨i, (Fin n → B i) ⧸ Kᵢ, inferInstance, inferInstance, ?_, ⟨?_⟩⟩
  · exact Module.finitePresentation_of_surjective Kᵢ.mkQ (Submodule.mkQ_surjective Kᵢ)
      (by rw [Submodule.ker_mkQ]; exact Submodule.fg_span (Set.finite_range y))
  · let π := TensorProduct.piScalarRight (B i) Bω Bω (Fin n)
    refine TensorProduct.AlgebraTensorModule.tensorQuotientEquiv Bω (B i) Bω Kᵢ ≪≫ₗ
      Submodule.Quotient.equiv _ K π ?_ ≪≫ₗ e.symm
    apply le_antisymm
    · rintro _ ⟨x, ⟨w, rfl⟩, rfl⟩
      induction w using TensorProduct.inductionOn with
      | add w₁ w₂ h₁ h₂ => simpa only [map_add] using add_mem h₁ h₂
      | tmul b k =>
        obtain ⟨k, hk⟩ := k
        simp only [TensorProduct.AlgebraTensorModule.lTensor_tmul, LinearMap.restrictScalars_apply,
          Submodule.subtype_apply, LinearEquiv.coe_coe, π, TensorProduct.piScalarRight_apply,
          TensorProduct.piScalarRightHom_tmul]
        induction hk using Submodule.span_induction generalizing b with
        | mem z hz =>
          obtain ⟨a, rfl⟩ := hz
          have : (fun j => y a j • b) = b • v a := by
            funext j
            simp [Algebra.smul_def, halg, hy, mul_comm]
          rw [this, ← hv]
          exact Submodule.smul_mem _ _ (Submodule.subset_span ⟨a, rfl⟩)
        | zero =>
          simp only [Pi.zero_apply, zero_smul]
          exact zero_mem K
        | add z₁ z₂ _ _ h₁ h₂ =>
          have : (fun j => (z₁ + z₂) j • b) = (fun j => z₁ j • b) + (fun j => z₂ j • b) := by
            funext j
            simp [add_smul]
          rw [this]
          exact add_mem (h₁ b) (h₂ b)
        | smul c z _ hz =>
          have : (fun j => (c • z) j • b) = fun j => z j • (c • b) := by
            funext j
            simp [mul_comm c, mul_smul]
          rw [this]
          exact hz _
    · rw [← hv, Submodule.span_le]
      rintro _ ⟨a, rfl⟩
      refine ⟨(1 : Bω) ⊗ₜ y a, ⟨(1 : Bω) ⊗ₜ ⟨y a, Submodule.subset_span ⟨a, rfl⟩⟩, rfl⟩, ?_⟩
      simp only [LinearEquiv.coe_coe, π, TensorProduct.piScalarRight_apply,
        TensorProduct.piScalarRightHom_tmul]
      funext j
      simp [Algebra.smul_def, halg, hy]

theorem

iso_desc_stage

L508 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_IsDirectLimit_exists_invertible_linearEquiv_baseChange.S17LFP.iso_desc_stage

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_IsDirectLimit_exists_invertible_linearEquiv_baseChange
open TensorProduct
namespace S17LFP
section Descent
universe u v w
variable {ι : Type v} [Preorder ι] [IsDirectedOrder ι] [Nonempty ι]
  {B₀ : Type u} [CommRing B₀]
  (B : ι → Type u) [∀ i, CommRing (B i)] [∀ i, Algebra B₀ (B i)]
  (τ : ∀ i j, i ≤ j → B i →ₐ[B₀] B j) [DirectedSystem B (fun i j h => τ i j h)]
  (Bω : Type u) [CommRing Bω] [Algebra B₀ Bω] (g : ∀ i, B i →ₐ[B₀] Bω)
  (hg : ∀ i j (h : i ≤ j), (g j).comp (τ i j h) = g i)
  (hsurj : ∀ b : Bω, ∃ i x, g i x = b)
  (hzero : ∀ i (x : B i), g i x = 0 → ∃ (j : ι) (h : i ≤ j), τ i j h x = 0)
  (P Q : Type*) [AddCommGroup P] [Module B₀ P] [AddCommGroup Q] [Module B₀ Q]
omit [Nonempty ι] in
include hg hsurj hzero in

Lean source · full declaration

theorem iso_desc_stage {i : ι} (M N : Type*) [AddCommGroup M] [Module (B i) M]
    [Module.FinitePresentation (B i) M] [AddCommGroup N] [Module (B i) N]
    [Module.FinitePresentation (B i) N]
    (e : letI := (g i).toRingHom.toAlgebra; Bω ⊗[B i] M ≃ₗ[Bω] Bω ⊗[B i] N) :
    ∃ (j : ι) (hij : i ≤ j),
      Nonempty (letI := (τ i j hij).toRingHom.toAlgebra; B j ⊗[B i] M ≃ₗ[B j] B j ⊗[B i] N) := by
  let algω : Algebra (B i) Bω := (g i).toRingHom.toAlgebra
  let ι' := {j : ι // i ≤ j}
  let : Nonempty ι' := ⟨⟨i, le_rfl⟩⟩
  have : IsDirectedOrder ι' := ⟨fun a b => by
    obtain ⟨k, h1, h2⟩ := exists_ge_ge a.1 b.1
    exact ⟨⟨k, a.2.trans h1⟩, h1, h2⟩⟩
  let B' : ι' → Type u := fun j => B j.1
  let algj : ∀ j : ι', Algebra (B i) (B' j) := fun j => (τ i j.1 j.2).toRingHom.toAlgebra
  let τ' : ∀ j k : ι', j ≤ k → B' j →ₐ[B i] B' k := fun j k h =>
    { (τ j.1 k.1 h).toRingHom with
      commutes' := fun b => by
        change τ j.1 k.1 h (τ i j.1 j.2 b) = τ i k.1 k.2 b
        exact DirectedSystem.map_map (f := fun i j h => ⇑(τ i j h)) j.2 h b }
  have : DirectedSystem B' (fun j k h => τ' j k h) :=
    ⟨fun j x => DirectedSystem.map_self (f := fun i j h => ⇑(τ i j h)) x,
     fun a b c h1 h2 x => DirectedSystem.map_map (f := fun i j h => ⇑(τ i j h)) h1 h2 x⟩
  let g' : ∀ j : ι', B' j →ₐ[B i] Bω := fun j =>
    { (g j.1).toRingHom with
      commutes' := fun b => by
        change g j.1 (τ i j.1 j.2 b) = g i b
        rw [← AlgHom.comp_apply, hg] }
  have hg' : ∀ j k (h : j ≤ k), (g' k).comp (τ' j k h) = g' j := fun j k h =>
    AlgHom.ext fun x => by
      change g k.1 (τ j.1 k.1 h x) = g j.1 x
      rw [← AlgHom.comp_apply, hg]
  have hsurj' : ∀ b : Bω, ∃ j x, g' j x = b := fun b => by
    obtain ⟨i₁, x, rfl⟩ := hsurj b
    obtain ⟨k, h1, h2⟩ := exists_ge_ge i i₁
    refine ⟨⟨k, h1⟩, τ i₁ k h2 x, ?_⟩
    change g k (τ i₁ k h2 x) = g i₁ x
    rw [← AlgHom.comp_apply, hg]
  have hzero' : ∀ j (x : B' j), g' j x = 0 → ∃ (k : ι') (h : j ≤ k), τ' j k h x = 0 :=
    fun j x hx => by
      obtain ⟨k, hjk, hk⟩ := hzero j.1 x hx
      exact ⟨⟨k, j.2.trans hjk⟩, hjk, hk⟩
  obtain ⟨j, eⱼ, -⟩ := iso_desc B' τ' Bω g' hg' hsurj' hzero' M N e
  exact ⟨j.1, j.2, ⟨eⱼ⟩⟩

theorem

inv_desc

L552 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_IsDirectLimit_exists_invertible_linearEquiv_baseChange.S17LFP.inv_desc

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_IsDirectLimit_exists_invertible_linearEquiv_baseChange
open TensorProduct
namespace S17LFP
section Descent
universe u v w
variable {ι : Type v} [Preorder ι] [IsDirectedOrder ι] [Nonempty ι]
  {B₀ : Type u} [CommRing B₀]
  (B : ι → Type u) [∀ i, CommRing (B i)] [∀ i, Algebra B₀ (B i)]
  (τ : ∀ i j, i ≤ j → B i →ₐ[B₀] B j) [DirectedSystem B (fun i j h => τ i j h)]
  (Bω : Type u) [CommRing Bω] [Algebra B₀ Bω] (g : ∀ i, B i →ₐ[B₀] Bω)
  (hg : ∀ i j (h : i ≤ j), (g j).comp (τ i j h) = g i)
  (hsurj : ∀ b : Bω, ∃ i x, g i x = b)
  (hzero : ∀ i (x : B i), g i x = 0 → ∃ (j : ι) (h : i ≤ j), τ i j h x = 0)
  (P Q : Type*) [AddCommGroup P] [Module B₀ P] [AddCommGroup Q] [Module B₀ Q]
include hg hsurj hzero in

Lean source · statement

theorem inv_desc [Module.FinitePresentation B₀ P] [Module.Invertible Bω (Bω ⊗[B₀] P)] :
    ∃ i : ι, Module.Invertible (B i) (B i ⊗[B₀] P)

theorem

inv_obj

L584 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_IsDirectLimit_exists_invertible_linearEquiv_baseChange.S17LFP.inv_obj

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_IsDirectLimit_exists_invertible_linearEquiv_baseChange
open TensorProduct
namespace S17LFP
section Descent
universe u v w
variable {ι : Type v} [Preorder ι] [IsDirectedOrder ι] [Nonempty ι]
  {B₀ : Type u} [CommRing B₀]
  (B : ι → Type u) [∀ i, CommRing (B i)] [∀ i, Algebra B₀ (B i)]
  (τ : ∀ i j, i ≤ j → B i →ₐ[B₀] B j) [DirectedSystem B (fun i j h => τ i j h)]
  (Bω : Type u) [CommRing Bω] [Algebra B₀ Bω] (g : ∀ i, B i →ₐ[B₀] Bω)
  (hg : ∀ i j (h : i ≤ j), (g j).comp (τ i j h) = g i)
  (hsurj : ∀ b : Bω, ∃ i x, g i x = b)
  (hzero : ∀ i (x : B i), g i x = 0 → ∃ (j : ι) (h : i ≤ j), τ i j h x = 0)
  (P Q : Type*) [AddCommGroup P] [Module B₀ P] [AddCommGroup Q] [Module B₀ Q]
include hg hsurj hzero in

Lean source · full declaration

theorem inv_obj (Y : Type*) [AddCommGroup Y] [Module Bω Y] [Module.Invertible Bω Y] :
    ∃ (i : ι) (L : Type u) (_ : AddCommGroup L) (_ : Module (B i) L),
      Module.Invertible (B i) L ∧
      Nonempty (letI := (g i).toRingHom.toAlgebra; Bω ⊗[B i] L ≃ₗ[Bω] Y) := by
  have : Module.FinitePresentation Bω Y := Module.finitePresentation_of_projective _ _
  have : Module.FinitePresentation Bω (Module.Dual Bω Y) :=
    Module.finitePresentation_of_projective _ _
  obtain ⟨i₁, L₁, _, _, hL₁, ⟨eL⟩⟩ := obj B τ Bω g hg hsurj Y
  obtain ⟨i₂, D₂, _, _, hD₂, ⟨eD⟩⟩ := obj B τ Bω g hg hsurj (Module.Dual Bω Y)
  have := hL₁
  have := hD₂
  obtain ⟨i, h₁, h₂⟩ := exists_ge_ge i₁ i₂
  let aω₁ : Algebra (B i₁) Bω := (g i₁).toRingHom.toAlgebra
  let aω₂ : Algebra (B i₂) Bω := (g i₂).toRingHom.toAlgebra
  let aω : Algebra (B i) Bω := (g i).toRingHom.toAlgebra
  let a₁ : Algebra (B i₁) (B i) := (τ i₁ i h₁).toRingHom.toAlgebra
  let a₂ : Algebra (B i₂) (B i) := (τ i₂ i h₂).toRingHom.toAlgebra
  have : IsScalarTower (B i₁) (B i) Bω := IsScalarTower.of_algebraMap_eq fun x => by
    change g i₁ x = g i (τ i₁ i h₁ x)
    rw [← AlgHom.comp_apply, hg]
  have : IsScalarTower (B i₂) (B i) Bω := IsScalarTower.of_algebraMap_eq fun x => by
    change g i₂ x = g i (τ i₂ i h₂ x)
    rw [← AlgHom.comp_apply, hg]
  let Lᵢ := B i ⊗[B i₁] L₁
  let Dᵢ := B i ⊗[B i₂] D₂
  let eLᵢ : Bω ⊗[B i] Lᵢ ≃ₗ[Bω] Y :=
    TensorProduct.AlgebraTensorModule.cancelBaseChange (B i₁) (B i) Bω Bω L₁ ≪≫ₗ eL
  let eDᵢ : Bω ⊗[B i] Dᵢ ≃ₗ[Bω] Module.Dual Bω Y :=
    TensorProduct.AlgebraTensorModule.cancelBaseChange (B i₂) (B i) Bω Bω D₂ ≪≫ₗ eD
  have := finitePresentation_tensorProduct (R := B i) Lᵢ Dᵢ
  let e : Bω ⊗[B i] (Lᵢ ⊗[B i] Dᵢ) ≃ₗ[Bω] Bω ⊗[B i] B i :=
    TensorProduct.AlgebraTensorModule.distribBaseChange (B i) Bω Lᵢ Dᵢ ≪≫ₗ
      TensorProduct.congr eLᵢ eDᵢ ≪≫ₗ
      (TensorProduct.comm _ _ _ ≪≫ₗ Module.Invertible.linearEquiv Bω Y) ≪≫ₗ
      (TensorProduct.AlgebraTensorModule.rid (B i) Bω Bω).symm
  obtain ⟨j, hij, ⟨eⱼ⟩⟩ := iso_desc_stage B τ Bω g hg hsurj hzero (Lᵢ ⊗[B i] Dᵢ) (B i) e
  let aj : Algebra (B i) (B j) := (τ i j hij).toRingHom.toAlgebra
  let aωj : Algebra (B j) Bω := (g j).toRingHom.toAlgebra
  have : IsScalarTower (B i) (B j) Bω := IsScalarTower.of_algebraMap_eq fun x => by
    change g i x = g j (τ i j hij x)
    rw [← AlgHom.comp_apply, hg]
  let f : (B j ⊗[B i] Lᵢ) ⊗[B j] (B j ⊗[B i] Dᵢ) ≃ₗ[B j] B j :=
    (TensorProduct.AlgebraTensorModule.distribBaseChange (B i) (B j) Lᵢ Dᵢ).symm ≪≫ₗ
      eⱼ ≪≫ₗ TensorProduct.AlgebraTensorModule.rid (B i) (B j) (B j)
  refine ⟨j, B j ⊗[B i] Lᵢ, inferInstance, inferInstance, Module.Invertible.left f, ⟨?_⟩⟩
  exact TensorProduct.AlgebraTensorModule.cancelBaseChange (B i) (B j) Bω Bω Lᵢ ≪≫ₗ eLᵢ

theorem

exists_invertible_linearEquiv_baseChange

L637 ↗

Module.IsDirectLimit.exists_invertible_linearEquiv_baseChange

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_IsDirectLimit_exists_invertible_linearEquiv_baseChange
open TensorProduct
universe u v w

Lean source · full declaration

theorem _root_.Module.IsDirectLimit.exists_invertible_linearEquiv_baseChange
    {ι : Type v} [Preorder ι] [IsDirectedOrder ι] [Nonempty ι]
    {B₀ : Type u} [CommRing B₀]
    (B : ι → Type u) [∀ i, CommRing (B i)] [∀ i, Algebra B₀ (B i)]
    (τ : ∀ i j, i ≤ j → B i →ₐ[B₀] B j) [DirectedSystem B (fun i j h => τ i j h)]
    (Bω : Type u) [CommRing Bω] [Algebra B₀ Bω] (g : ∀ i, B i →ₐ[B₀] Bω)
    (hg : ∀ i j (h : i ≤ j), (g j).comp (τ i j h) = g i)
    (hsurj : ∀ b : Bω, ∃ i x, g i x = b)
    (hzero : ∀ i (x : B i), g i x = 0 → ∃ (j : ι) (h : i ≤ j), τ i j h x = 0)
    (Y : Type w) [AddCommGroup Y] [Module Bω Y] [Module.Invertible Bω Y] :
    ∃ (i : ι) (L : Type u) (_ : AddCommGroup L) (_ : Module (B i) L),
      Module.Invertible (B i) L ∧
      Nonempty (letI := (g i).toRingHom.toAlgebra; TensorProduct (B i) Bω L ≃ₗ[Bω] Y) :=
  S17LFP.inv_obj B τ Bω g hg hsurj hzero Y

Module documentation

Descent of invertible modules along direct limits

Declarations