Module

Module_FaithfullyFlat_exists_submodule_isBaseChange_of_cocycle.lean

Nyll.AlgebraicCurves.Foundations.Algebra.Module_FaithfullyFlat_exists_submodule_isBaseChange_of_cocycle

100 declarations indexed from sourceView source ↗

Module documentation

Effective descent of modules along a faithfully flat algebra

The equalizer of the descent maps is the descended submodule. Tensor calculations identify its base change and verify the descent square.

Imports2

Imported by2

theorem

esComp_inv_one_tmul_tmul

L40 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.esComp_inv_one_tmul_tmul

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section HelperE
open scoped ChangeOfRings
variable {R S T : Type u} [CommRing R] [CommRing S] [CommRing T] (f : R →+* S) (g : S →+* T)
  (M : ModuleCat.{u} R)

Lean source · statement

theorem esComp_inv_one_tmul_tmul (x : S) (m : M) :
    (ModuleCat.extendScalarsComp f g).inv.app M
      ((1 : T) ⊗ₜ[S, g] ((x ⊗ₜ[R, f] m : (ModuleCat.extendScalars f).obj M)) :
        (ModuleCat.extendScalars g).obj ((ModuleCat.extendScalars f).obj M)) =
      ((g x) ⊗ₜ[R, g.comp f] m : (ModuleCat.extendScalars (g.comp f)).obj M)

theorem

esComp_hom_one_tmul

L89 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.esComp_hom_one_tmul

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section HelperE
open scoped ChangeOfRings
variable {R S T : Type u} [CommRing R] [CommRing S] [CommRing T] (f : R →+* S) (g : S →+* T)
  (M : ModuleCat.{u} R)

Lean source · statement

theorem esComp_hom_one_tmul (m : M) :
    (ModuleCat.extendScalarsComp f g).hom.app M ((1 : T) ⊗ₜ[R, g.comp f] m :
      (ModuleCat.extendScalars (g.comp f)).obj M) =
      ((1 : T) ⊗ₜ[S, g] ((1 : S) ⊗ₜ[R, f] m : (ModuleCat.extendScalars f).obj M) :
        (ModuleCat.extendScalars g).obj ((ModuleCat.extendScalars f).obj M))

theorem

es_map_one_tmul

L96 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.es_map_one_tmul

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section HelperE
open scoped ChangeOfRings
variable {R S T : Type u} [CommRing R] [CommRing S] [CommRing T] (f : R →+* S) (g : S →+* T)
  (M : ModuleCat.{u} R)

Lean source · statement

theorem es_map_one_tmul {M₁ M₂ : ModuleCat.{u} S} (φ : M₁ ⟶ M₂) (e : M₁) :
    (ModuleCat.extendScalars g).map φ ((1 : T) ⊗ₜ[S, g] e : (ModuleCat.extendScalars g).obj M₁) =
      ((1 : T) ⊗ₜ[S, g] φ e : (ModuleCat.extendScalars g).obj M₂)

theorem

esComp_hom_tmul

L101 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.esComp_hom_tmul

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section HelperE
open scoped ChangeOfRings
variable {R S T : Type u} [CommRing R] [CommRing S] [CommRing T] (f : R →+* S) (g : S →+* T)
  (M : ModuleCat.{u} R)

Lean source · statement

theorem esComp_hom_tmul (s : T) (m : M) :
    (ModuleCat.extendScalarsComp f g).hom.app M ((s ⊗ₜ[R, g.comp f] m : (ModuleCat.extendScalars
      (g.comp f)).obj M)) =
      SMul.smul (M := T)
        (α := (ModuleCat.extendScalars g).obj ((ModuleCat.extendScalars f).obj M)) s
        ((1 : T) ⊗ₜ[S, g] ((1 : S) ⊗ₜ[R, f] m : (ModuleCat.extendScalars f).obj M) :
        (ModuleCat.extendScalars g).obj ((ModuleCat.extendScalars f).obj M))

theorem

eqToHom_extendScalars_tmul

L120 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.eqToHom_extendScalars_tmul

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section HelperE
open scoped ChangeOfRings
variable {R S T : Type u} [CommRing R] [CommRing S] [CommRing T] (f : R →+* S) (g : S →+* T)
  (M : ModuleCat.{u} R)

Lean source · full declaration

theorem eqToHom_extendScalars_tmul {f f' : R →+* S} (h : f = f') (s : S) (m : M) :
    eqToHom (congrArg (fun f : R →+* S => (ModuleCat.extendScalars f).obj M) h)
      (s ⊗ₜ[R, f] m : (ModuleCat.extendScalars f).obj M) = (s ⊗ₜ[R, f'] m :
        (ModuleCat.extendScalars f').obj M) := by
  subst h
  rfl

theorem

es_one_tmul_smul

L127 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.es_one_tmul_smul

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section HelperE
open scoped ChangeOfRings
variable {R S T : Type u} [CommRing R] [CommRing S] [CommRing T] (f : R →+* S) (g : S →+* T)
  (M : ModuleCat.{u} R)

Lean source · statement

theorem es_one_tmul_smul (r : R) (m : M) :
    ((1 : S) ⊗ₜ[R, f] (r • m) : (ModuleCat.extendScalars f).obj M) =
      SMul.smul (M := S) (α := (ModuleCat.extendScalars f).obj M) (f r)
        ((1 : S) ⊗ₜ[R, f] m)

theorem

compareScalarExtensions_one_tmul_tmul

L150 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.compareScalarExtensions_one_tmul_tmul

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Transport
open scoped ChangeOfRings
variable {R S T : Type u} [CommRing R] [CommRing S] [CommRing T]

Lean source · statement

theorem compareScalarExtensions_one_tmul_tmul
    (f : R →+* S) (g₁ g₂ : S →+* T) (h : g₁.comp f = g₂.comp f)
    (M : ModuleCat.{u} R) (x : S) (m : M) :
    compareScalarExtensions f g₁ g₂ h M
      ((1 : T) ⊗ₜ[S, g₁] (x ⊗ₜ[R, f] m : (ModuleCat.extendScalars f).obj M)) =
      ((g₁ x) ⊗ₜ[S, g₂] ((1 : S) ⊗ₜ[R, f] m : (ModuleCat.extendScalars f).obj M) :
        (ModuleCat.extendScalars g₂).obj ((ModuleCat.extendScalars f).obj M))

theorem

comparison_square

L175 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.comparison_square

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Transport
open scoped ChangeOfRings
variable {R S T : Type u} [CommRing R] [CommRing S] [CommRing T]

Lean source · statement

theorem comparison_square (f : R →+* S) (g₁ g₂ : S →+* T)
    (h : g₁.comp f = g₂.comp f) (P : ModuleCat.{u} R) (Q : ModuleCat.{u} S)
    (θ : (ModuleCat.extendScalars f).obj P ⟶ Q)
    (φ : (ModuleCat.extendScalars g₁).obj Q ⟶ (ModuleCat.extendScalars g₂).obj Q)
    (hunit : ∀ m : P,
      φ ((1 : T) ⊗ₜ[S, g₁] θ ((1 : S) ⊗ₜ[R, f] m)) =
        ((1 : T) ⊗ₜ[S, g₂] θ ((1 : S) ⊗ₜ[R, f] m) :
          (ModuleCat.extendScalars g₂).obj Q)) :
    (ModuleCat.extendScalars g₁).map θ ≫ φ =
      compareScalarExtensions f g₁ g₂ h P ≫ (ModuleCat.extendScalars g₂).map θ

abbrev

Nc

L235 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.Nc

Documentation

The given module bundled over the extension ring.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Dictionary
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]

Lean source · statement

abbrev Nc : ModuleCat.{u} B

abbrev

X₁

L238 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.X₁

Documentation

The double tensor ring with scalars restricted along the first coface.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Dictionary
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]

Lean source · statement

abbrev X₁ (A B : Type u) [CommRing A] [CommRing B] [Algebra A B]

abbrev

X₂

L241 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.X₂

Documentation

The double tensor ring with scalars restricted along the second coface.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Dictionary
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]

Lean source · statement

abbrev X₂ (A B : Type u) [CommRing A] [CommRing B] [Algebra A B]

abbrev

E₁

L244 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.E₁

Documentation

Extend the given module along the first coface.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Dictionary
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]

Lean source · statement

abbrev E₁

abbrev

E₂

L246 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.E₂

Documentation

Extend the given module along the second coface.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Dictionary
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]

Lean source · statement

abbrev E₂

theorem

X₁_smul_def

L248 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.X₁_smul_def

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Dictionary
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]

Lean source · full declaration

theorem X₁_smul_def (b : B) (x : B ⊗[A] B) :
    (b • (show X₁ A B from x) : X₁ A B) = (show X₁ A B from (b ⊗ₜ[A] (1 : B)) * x) := rfl

theorem

X₂_smul_def

L250 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.X₂_smul_def

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Dictionary
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]

Lean source · full declaration

theorem X₂_smul_def (b : B) (x : B ⊗[A] B) :
    (b • (show X₂ A B from x) : X₂ A B) = (show X₂ A B from ((1 : B) ⊗ₜ[A] b) * x) := rfl

def

k₁

L254 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.k₁

Documentation

Act on the module by the first tensor factor and retain the second factor.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Dictionary
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]

Lean source · statement

def k₁ : B ⊗[A] B →ₗ[A] N →ₗ[A] N ⊗[A] B

theorem

k₁_tmul

L262 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.k₁_tmul

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Dictionary
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]

Lean source · statement

theorem k₁_tmul (b₁ b₂ : B) (n : N) : k₁ (A := A) N (b₁ ⊗ₜ b₂) n = (b₁ • n) ⊗ₜ b₂

def

u₁

L265 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.u₁

Documentation

The balanced linear map induced by the first-factor action.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Dictionary
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]

Lean source · statement

def u₁ : X₁ A B ⊗[B] N →ₗ[B] N ⊗[A] B

theorem

u₁_tmul

L285 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.u₁_tmul

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Dictionary
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]

Lean source · full declaration

theorem u₁_tmul (b₁ b₂ : B) (n : N) :
    u₁ (A := A) N ((show X₁ A B from b₁ ⊗ₜ[A] b₂) ⊗ₜ[B] n) = (b₁ • n) ⊗ₜ b₂ := by
  exact k₁_tmul (A := A) N b₁ b₂ n

def

k₂

L290 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.k₂

Documentation

Act on the module by the second tensor factor and retain the first factor.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Dictionary
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]

Lean source · statement

def k₂ : B ⊗[A] B →ₗ[A] N →ₗ[A] N ⊗[A] B

theorem

k₂_tmul

L293 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.k₂_tmul

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Dictionary
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]

Lean source · statement

theorem k₂_tmul (b₁ b₂ : B) (n : N) : k₂ (A := A) N (b₁ ⊗ₜ b₂) n = (b₂ • n) ⊗ₜ b₁

def

u₂

L296 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.u₂

Documentation

The balanced linear map induced by the second-factor action.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Dictionary
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]

Lean source · statement

def u₂ : X₂ A B ⊗[B] N →ₗ[B] N ⊗[A] B

theorem

u₂_tmul

L316 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.u₂_tmul

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Dictionary
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]

Lean source · full declaration

theorem u₂_tmul (b₁ b₂ : B) (n : N) :
    u₂ (A := A) N ((show X₂ A B from b₁ ⊗ₜ[A] b₂) ⊗ₜ[B] n) = (b₂ • n) ⊗ₜ b₁ := by
  exact k₂_tmul (A := A) N b₁ b₂ n

def

v₂

L321 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.v₂

Documentation

Insert a unit tensor factor to invert the second-factor comparison.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Dictionary
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]

Lean source · statement

def v₂ : N ⊗[A] B →+ X₂ A B ⊗[B] N

theorem

v₂_tmul

L344 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.v₂_tmul

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Dictionary
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]

Lean source · full declaration

theorem v₂_tmul (n : N) (b : B) :
      v₂ (A := A) N (n ⊗ₜ b) = (((show X₂ A B from b ⊗ₜ[A] (1 : B)) ⊗ₜ[B] n : X₂ A B ⊗[B] N)) := rfl

theorem

v₂_u₂

L347 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.v₂_u₂

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Dictionary
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]

Lean source · statement

theorem v₂_u₂ (e : X₂ A B ⊗[B] N) : v₂ (A := A) N (u₂ (A := A) N e) = e

theorem

u₂_injective

L367 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.u₂_injective

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Dictionary
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]

Lean source · statement

theorem u₂_injective : Function.Injective (u₂ (A := A) (B := B) N)

abbrev

X₃

L371 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.X₃

Documentation

The triple tensor ring with scalars restricted to its third factor.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Dictionary
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]

Lean source · statement

abbrev X₃ (A B : Type u) [CommRing A] [CommRing B] [Algebra A B]

abbrev

F₃

L374 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.F₃

Documentation

Extend the given module to the triple tensor ring through its third factor.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Dictionary
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]

Lean source · statement

abbrev F₃

theorem

j₃_apply

L376 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.j₃_apply

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Dictionary
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]

Lean source · statement

theorem j₃_apply (b : B) : (i₂ A B ≫ c₂₃ A B).hom b = 1 ⊗ₜ (1 ⊗ₜ b)

def

act

L379 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.act

Documentation

Evaluate the scalar action on a tensor product with the module.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Dictionary
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]

Lean source · statement

def act : B ⊗[A] N →ₗ[A] N

theorem

act_tmul

L384 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.act_tmul

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Dictionary
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]

Lean source · statement

theorem act_tmul (b : B) (n : N) : act (A := A) N (b ⊗ₜ n) = b • n

def

K₃

L387 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.K₃

Documentation

Move the module factor past the first two scalars and evaluate the third scalar.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Dictionary
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]

Lean source · statement

def K₃ : (B ⊗[A] (B ⊗[A] B)) ⊗[A] N →ₗ[A] N ⊗[A] (B ⊗[A] B)

theorem

K₃_tmul

L394 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.K₃_tmul

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Dictionary
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]

Lean source · statement

theorem K₃_tmul (b₁ b₂ b₃ : B) (n : N) :
    K₃ (A := A) N ((b₁ ⊗ₜ (b₂ ⊗ₜ b₃)) ⊗ₜ n) = (b₃ • n) ⊗ₜ (b₁ ⊗ₜ b₂)

def

k₃

L399 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.k₃

Documentation

The curried form of the triple-tensor comparison.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Dictionary
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]

Lean source · statement

def k₃ : B ⊗[A] (B ⊗[A] B) →ₗ[A] N →ₗ[A] N ⊗[A] (B ⊗[A] B)

theorem

k₃_tmul

L402 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.k₃_tmul

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Dictionary
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]

Lean source · statement

theorem k₃_tmul (b₁ b₂ b₃ : B) (n : N) :
    k₃ (A := A) N (b₁ ⊗ₜ (b₂ ⊗ₜ b₃)) n = (b₃ • n) ⊗ₜ (b₁ ⊗ₜ b₂)

def

u₃

L407 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.u₃

Documentation

The balanced triple-tensor comparison through the third-factor action.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Dictionary
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]

Lean source · statement

def u₃ : X₃ A B ⊗[B] N →ₗ[B] N ⊗[A] (B ⊗[A] B)

theorem

u₃_tmul

L436 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.u₃_tmul

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Dictionary
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]

Lean source · full declaration

theorem u₃_tmul (b₁ b₂ b₃ : B) (n : N) :
    u₃ (A := A) N ((show X₃ A B from b₁ ⊗ₜ[A] (b₂ ⊗ₜ[A] b₃)) ⊗ₜ[B] n) = (b₃ • n) ⊗ₜ (b₁ ⊗ₜ b₂) := by
  exact k₃_tmul (A := A) N b₁ b₂ b₃ n

abbrev

Xc

L441 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.Xc

Documentation

Restrict scalars on the triple tensor ring along the chosen composite coface.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Dictionary
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]

Lean source · statement

abbrev Xc (c : R₂ A B ⟶ R₃ A B)

abbrev

Fc

L444 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.Fc

Documentation

Extend the given module along the chosen composite coface.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Dictionary
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]

Lean source · statement

abbrev Fc (c : R₂ A B ⟶ R₃ A B)

def

push

L448 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.push

Documentation

Apply a coface to the ring factor of a balanced tensor.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Dictionary
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]

Lean source · statement

def push (c : R₂ A B ⟶ R₃ A B) : X₂ A B ⊗[B] N →ₗ[B] Xc c ⊗[B] N

theorem

push_tmul

L465 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.push_tmul

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Dictionary
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]
omit [Module A N] [IsScalarTower A B N] in

Lean source · full declaration

theorem push_tmul (c : R₂ A B ⟶ R₃ A B) (x : B ⊗[A] B) (n : N) :
    push (A := A) N c ((show X₂ A B from x) ⊗ₜ[B] n : X₂ A B ⊗[B] N) =
      ((show Xc c from c.hom x) ⊗ₜ[B] n : Xc c ⊗[B] N) := by
  exact TensorProduct.lift.tmul (show X₂ A B from x) n

theorem

esc_inv_one_tmul

L471 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.esc_inv_one_tmul

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Dictionary
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]
omit [Module A N] [IsScalarTower A B N] in

Lean source · statement

theorem esc_inv_one_tmul (c : R₂ A B ⟶ R₃ A B) (e : E₂ (A := A) N) :
    (ModuleCat.extendScalarsComp (i₂ A B).hom c.hom).inv.app (Nc N)
      ((1 : R₃ A B) ⊗ₜ[R₂ A B, c.hom] e :
        (ModuleCat.extendScalars c.hom).obj (E₂ (A := A) N)) = push (A := A) N c e

theorem

T_one_tmul

L488 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.T_one_tmul

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Dictionary
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]
omit [Module A N] [IsScalarTower A B N] in

Lean source · statement

theorem T_one_tmul (c : R₂ A B ⟶ R₃ A B) (φ' : E₁ (A := A) N ⟶ E₂ (A := A) N) (n : N) :
    T (Nc N) c φ' ((1 : R₃ A B) ⊗ₜ[B,(i₁ A B ≫ c).hom] n :
        (ModuleCat.extendScalars (i₁ A B ≫ c).hom).obj (Nc N)) =
      push (A := A) N c (φ' ((1 : R₂ A B) ⊗ₜ[B,(i₁ A B).hom] n : E₁ (A := A) N))

def

ins₁

L500 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.ins₁

Documentation

Insert one in the second tensor factor.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Dictionary
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]

Lean source · statement

def ins₁ : B →ₗ[A] B ⊗[A] B

def

ins₂

L502 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.ins₂

Documentation

Insert one in the first tensor factor.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Dictionary
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]

Lean source · statement

def ins₂ : B →ₗ[A] B ⊗[A] B

theorem

ins₁_apply

L504 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.ins₁_apply

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Dictionary
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]

Lean source · statement

theorem ins₁_apply (b : B) : ins₁ (A := A) (B := B) b = b ⊗ₜ 1

theorem

ins₂_apply

L505 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.ins₂_apply

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Dictionary
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]

Lean source · statement

theorem ins₂_apply (b : B) : ins₂ (A := A) (B := B) b = 1 ⊗ₜ b

def

σ

L508 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.σ

Documentation

Reassociate the tensor product and exchange the two ring factors.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Dictionary
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]

Lean source · statement

def σ : (N ⊗[A] B) ⊗[A] B ≃ₗ[A] N ⊗[A] (B ⊗[A] B)

theorem

σ_tmul

L512 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.σ_tmul

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Dictionary
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]
omit [Module B N] [IsScalarTower A B N] in

Lean source · statement

theorem σ_tmul (m : N) (β' β : B) : σ (A := A) N ((m ⊗ₜ β') ⊗ₜ β) = m ⊗ₜ (β ⊗ₜ β')

theorem

u₃_push₁₃

L514 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.u₃_push₁₃

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Dictionary
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]

Lean source · statement

theorem u₃_push₁₃ (e : E₂ (A := A) N) :
    u₃ (A := A) N (push (A := A) N (c₁₃ A B) e) = (ins₁ (A := A) (B := B)).lTensor N (u₂ (A := A) N
      e)

theorem

u₃_push₂₃

L536 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.u₃_push₂₃

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Dictionary
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]

Lean source · statement

theorem u₃_push₂₃ (e : E₂ (A := A) N) :
    u₃ (A := A) N (push (A := A) N (c₂₃ A B) e) = (ins₂ (A := A) (B := B)).lTensor N (u₂ (A := A) N
      e)

theorem

u₃_c₁₂_mul_tmul

L555 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.u₃_c₁₂_mul_tmul

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Dictionary
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]

Lean source · statement

theorem u₃_c₁₂_mul_tmul (x : B ⊗[A] B) (y : B ⊗[A] (B ⊗[A] B)) (n : N) :
    u₃ (A := A) N ((((c₁₂ A B).hom x) * y) ⊗ₜ[B] n : X₃ A B ⊗[B] N) =
      (LinearMap.mulLeft A x).lTensor N (u₃ (A := A) N (y ⊗ₜ[B] n : X₃ A B ⊗[B] N))

theorem

u₃_c₁₂_smul

L607 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.u₃_c₁₂_smul

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Dictionary
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]

Lean source · statement

theorem u₃_c₁₂_smul (x : B ⊗[A] B) (f : X₃ A B ⊗[B] N) :
    u₃ (A := A) N (SMul.smul (M := R₃ A B) (α := F₃ (A := A) N) ((c₁₂ A B).hom x) f) =
      (LinearMap.mulLeft A x).lTensor N (u₃ (A := A) N f)

def

δ

L636 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.δ

Documentation

Apply the descent morphism to a unit tensor.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Core
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]
  (φ' : E₁ (A := A) (B := B) N ⟶ E₂ (A := A) (B := B) N)

Lean source · statement

def δ (n : N) : E₂ (A := A) (B := B) N

theorem

δ_add

L640 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.δ_add

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Core
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]
  (φ' : E₁ (A := A) (B := B) N ⟶ E₂ (A := A) (B := B) N)
omit [Module A N] [IsScalarTower A B N] in

Lean source · statement

theorem δ_add (n n' : N) : δ N φ' (n + n') = δ N φ' n + δ N φ' n'

theorem

one_tmul_smul_E₁

L645 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.one_tmul_smul_E₁

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Core
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]
  (φ' : E₁ (A := A) (B := B) N ⟶ E₂ (A := A) (B := B) N)
omit [Module A N] [IsScalarTower A B N] in

Lean source · statement

theorem one_tmul_smul_E₁ (b : B) (n : N) :
    ((1 : R₂ A B) ⊗ₜ[B,(i₁ A B).hom] (b • n) : E₁ (A := A) (B := B) N) =
      SMul.smul (M := R₂ A B) (α := E₁ (A := A) (B := B) N)
        ((i₁ A B).hom b) ((1 : R₂ A B) ⊗ₜ[B,(i₁ A B).hom] n)

theorem

one_tmul_smul_E₂

L652 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.one_tmul_smul_E₂

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Core
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]
  (φ' : E₁ (A := A) (B := B) N ⟶ E₂ (A := A) (B := B) N)
omit [Module A N] [IsScalarTower A B N] in

Lean source · statement

theorem one_tmul_smul_E₂ (b : B) (n : N) :
    ((1 : R₂ A B) ⊗ₜ[B,(i₂ A B).hom] (b • n) : E₂ (A := A) (B := B) N) =
      SMul.smul (M := R₂ A B) (α := E₂ (A := A) (B := B) N)
        ((i₂ A B).hom b) ((1 : R₂ A B) ⊗ₜ[B,(i₂ A B).hom] n)

theorem

δ_smul

L659 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.δ_smul

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Core
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]
  (φ' : E₁ (A := A) (B := B) N ⟶ E₂ (A := A) (B := B) N)
omit [Module A N] [IsScalarTower A B N] in

Lean source · statement

theorem δ_smul (b : B) (n : N) : δ N φ' (b • n) = ((i₁ A B).hom b) • δ N φ' n

theorem

u₂_i₁_smul

L663 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.u₂_i₁_smul

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Core
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]
  (φ' : E₁ (A := A) (B := B) N ⟶ E₂ (A := A) (B := B) N)

Lean source · statement

theorem u₂_i₁_smul (b : B) (e : E₂ (A := A) (B := B) N) :
    u₂ (A := A) N (SMul.smul (M := R₂ A B) (α := E₂ (A := A) (B := B) N) ((i₁ A B).hom b) e) =
      (LinearMap.mulLeft A b).lTensor N (u₂ (A := A) N e)

theorem

u₂_one_tmul

L702 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.u₂_one_tmul

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Core
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]
  (φ' : E₁ (A := A) (B := B) N ⟶ E₂ (A := A) (B := B) N)

Lean source · statement

theorem u₂_one_tmul (n : N) : u₂ (A := A) N ((1 : B ⊗[A] B) ⊗ₜ[B] n : X₂ A B ⊗[B] N) = n ⊗ₜ 1

theorem

u₁_one_tmul

L707 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.u₁_one_tmul

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Core
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]
  (φ' : E₁ (A := A) (B := B) N ⟶ E₂ (A := A) (B := B) N)

Lean source · statement

theorem u₁_one_tmul (n : N) : u₁ (A := A) N ((1 : B ⊗[A] B) ⊗ₜ[B] n : X₁ A B ⊗[B] N) = n ⊗ₜ 1

theorem

lTensor_mulLeft_algebraMap

L713 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.lTensor_mulLeft_algebraMap

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Core
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]
  (φ' : E₁ (A := A) (B := B) N ⟶ E₂ (A := A) (B := B) N)
omit [Module B N] [IsScalarTower A B N] in

Lean source · statement

theorem lTensor_mulLeft_algebraMap (a : A) (z : N ⊗[A] B) :
    (LinearMap.mulLeft A (algebraMap A B a)).lTensor N z = a • z

def

δ₂

L722 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.δ₂

Documentation

Express the descent coaction in the module-first tensor product.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Core
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]
  (φ' : E₁ (A := A) (B := B) N ⟶ E₂ (A := A) (B := B) N)

Lean source · full declaration

def δ₂ : N →ₗ[A] N ⊗[A] B where
  toFun n := u₂ (A := A) N (δ N φ' n)
  map_add' n n' := (congrArg (u₂ (A := A) N) (δ_add N φ' n n')).trans
    (map_add (u₂ (A := A) N) _ _)
  map_smul' a n := by
    rw [RingHom.id_apply, ← IsScalarTower.algebraMap_smul B a n]
    exact (congrArg (u₂ (A := A) N) (δ_smul N φ' (algebraMap A B a) n)).trans
      ((u₂_i₁_smul (A := A) N (algebraMap A B a) (δ N φ' n)).trans
        (lTensor_mulLeft_algebraMap (A := A) N a _))

theorem

δ₂_apply

L732 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.δ₂_apply

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Core
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]
  (φ' : E₁ (A := A) (B := B) N ⟶ E₂ (A := A) (B := B) N)

Lean source · statement

theorem δ₂_apply (n : N) : δ₂ N φ' n = u₂ (A := A) N (δ N φ' n)

def

ι₂

L735 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.ι₂

Documentation

The unit-insertion map in the module-first tensor product.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Core
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]
  (φ' : E₁ (A := A) (B := B) N ⟶ E₂ (A := A) (B := B) N)

Lean source · statement

def ι₂ : N →ₗ[A] N ⊗[A] B

theorem

ι₂_apply

L738 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.ι₂_apply

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Core
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]
  (φ' : E₁ (A := A) (B := B) N ⟶ E₂ (A := A) (B := B) N)
omit [Module B N] [IsScalarTower A B N] in

Lean source · statement

theorem ι₂_apply (n : N) : ι₂ (A := A) (B := B) N n = n ⊗ₜ 1

def

Msub

L741 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.Msub

Documentation

The equalizer submodule fixed by the descent coaction.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Core
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]
  (φ' : E₁ (A := A) (B := B) N ⟶ E₂ (A := A) (B := B) N)

Lean source · full declaration

def Msub : Submodule A N where
  carrier := {n | δ N φ' n = ((1 : R₂ A B) ⊗ₜ[B,(i₂ A B).hom] n : E₂ (A := A) (B := B) N)}
  add_mem' {n n'} hn hn' := by
    change δ N φ' (n + n') = _
    exact (δ_add N φ' n n').trans ((congrArg₂ (· + ·) hn hn').trans
      (TensorProduct.tmul_add (show X₂ A B from (1 : R₂ A B))
        (show Nc N from n) (show Nc N from n')).symm)
  zero_mem' := by
    change δ N φ' 0 = _
    exact ((congrArg φ' (TensorProduct.tmul_zero (R := B) (Nc N) (show X₁ A B from (1 : R₂ A
      B)))).trans
      (map_zero φ'.hom)).trans
        (TensorProduct.tmul_zero (R := B) (Nc N) (show X₂ A B from (1 : R₂ A B))).symm
  smul_mem' a n hn := by
    change δ N φ' (a • n) = ((1 : R₂ A B) ⊗ₜ[B,(i₂ A B).hom] (a • n) : E₂ (A := A) (B := B) N)
    rw [← IsScalarTower.algebraMap_smul B a n, δ_smul, hn, one_tmul_smul_E₂]
    congr 1
    exact congrArg (fun f : CommRingCat.of A ⟶ R₂ A B => f.hom a) (algebraMap_i₁_eq_i₂ A B)

theorem

mem_Msub_iff

L760 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.mem_Msub_iff

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Core
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]
  (φ' : E₁ (A := A) (B := B) N ⟶ E₂ (A := A) (B := B) N)

Lean source · statement

theorem mem_Msub_iff (n : N) :
    n ∈ Msub N φ' ↔ φ' ((1 : R₂ A B) ⊗ₜ[B,(i₁ A B).hom] n : E₁ (A := A) (B := B) N) = ((1 : R₂ A
      B) ⊗ₜ[B,(i₂ A B).hom] n : E₂ (A := A) (B := B) N)

theorem

δ₂_of_mem

L765 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.δ₂_of_mem

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Core
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]
  (φ' : E₁ (A := A) (B := B) N ⟶ E₂ (A := A) (B := B) N)

Lean source · statement

theorem δ₂_of_mem {m : N} (hm : m ∈ Msub N φ') : δ₂ N φ' m = m ⊗ₜ 1

theorem

δ₂_smul_of_mem

L768 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.δ₂_smul_of_mem

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Core
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]
  (φ' : E₁ (A := A) (B := B) N ⟶ E₂ (A := A) (B := B) N)

Lean source · statement

theorem δ₂_smul_of_mem {m : N} (hm : m ∈ Msub N φ') (b : B) : δ₂ N φ' (b • m) = m ⊗ₜ b

theorem

aux₁

L775 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.aux₁

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Core
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]
  (φ' : E₁ (A := A) (B := B) N ⟶ E₂ (A := A) (B := B) N)
omit [Module B N] [IsScalarTower A B N] in

Lean source · statement

theorem aux₁ (b₁ b₂ : B) (z : N ⊗[A] B) :
    (LinearMap.mulLeft A (b₁ ⊗ₜ[A] b₂) ∘ₗ ins₂ (A := A) (B := B)).lTensor N z =
      σ (A := A) N (((LinearMap.mulLeft A b₂).lTensor N z) ⊗ₜ b₁)

theorem

aux₂

L786 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.aux₂

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Core
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]
  (φ' : E₁ (A := A) (B := B) N ⟶ E₂ (A := A) (B := B) N)
omit [Module B N] [IsScalarTower A B N] in

Lean source · statement

theorem aux₂ (z : N ⊗[A] B) :
    (ins₁ (A := A) (B := B)).lTensor N z = σ (A := A) N ((ι₂ (A := A) (B := B) N).rTensor B z)

theorem

T_tmul

L793 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.T_tmul

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Core
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]
  (φ' : E₁ (A := A) (B := B) N ⟶ E₂ (A := A) (B := B) N)
omit [Module A N] [IsScalarTower A B N] in

Lean source · statement

theorem T_tmul (c : R₂ A B ⟶ R₃ A B) (y : B ⊗[A] (B ⊗[A] B)) (n : N) :
    T (Nc N) c φ'
      (y ⊗ₜ[B,(i₁ A B ≫ c).hom] n : (ModuleCat.extendScalars (i₁ A B ≫ c).hom).obj (Nc N)) =
      SMul.smul (M := R₃ A B) (α := Fc (A := A) N c) y
        (push (A := A) N c (φ' ((1 : R₂ A B) ⊗ₜ[B,(i₁ A B).hom] n)))

theorem

u₃_T₂₃_push₁₂

L804 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.u₃_T₂₃_push₁₂

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Core
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]
  (φ' : E₁ (A := A) (B := B) N ⟶ E₂ (A := A) (B := B) N)

Lean source · statement

theorem u₃_T₂₃_push₁₂ (e : E₂ (A := A) (B := B) N) :
    u₃ (A := A) N (T (Nc N) (c₂₃ A B) φ' (push (A := A) N (c₁₂ A B) e)) =
      σ (A := A) N ((δ₂ N φ').rTensor B (u₂ (A := A) N e))

theorem

u₃_push₁₃'

L838 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.u₃_push₁₃'

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Core
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]
  (φ' : E₁ (A := A) (B := B) N ⟶ E₂ (A := A) (B := B) N)

Lean source · statement

theorem u₃_push₁₃' (e : E₂ (A := A) (B := B) N) :
    u₃ (A := A) N (push (A := A) N (c₁₃ A B) e) = σ (A := A) N ((ι₂ (A := A) (B := B) N).rTensor B
      (u₂ (A := A) N e))

theorem

coassoc

L843 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.coassoc

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Core
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]
  (φ' : E₁ (A := A) (B := B) N ⟶ E₂ (A := A) (B := B) N)

Lean source · statement

theorem coassoc (hcoc : Cocycle (Nc N) φ') (n : N) :
    (δ₂ N φ').rTensor B (δ₂ N φ' n) = (ι₂ (A := A) (B := B) N).rTensor B (δ₂ N φ' n)

theorem

tmul_one_injective

L855 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.tmul_one_injective

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Core
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]
  (φ' : E₁ (A := A) (B := B) N ⟶ E₂ (A := A) (B := B) N)
omit [Module B N] [IsScalarTower A B N] in

Lean source · full declaration

theorem tmul_one_injective [Module.FaithfullyFlat A B] :
    Function.Injective (fun n : N => n ⊗ₜ[A] (1 : B)) := by
  let g : N →ₗ[A] N ⊗[A] B := (TensorProduct.mk A N B).flip 1
  have hg : ⇑g = fun n : N => n ⊗ₜ[A] (1 : B) := rfl
  rw [← hg]
  let r : B ⊗[A] (N ⊗[A] B) →ₗ[A] B ⊗[A] N :=
    (LinearMap.mul' A B).rTensor N ∘ₗ (TensorProduct.assoc A B B N).symm.toLinearMap ∘ₗ
      (TensorProduct.comm A N B).toLinearMap.lTensor B
  have hr : ∀ z, r (g.lTensor B z) = z := by
    intro z
    induction z using TensorProduct.inductionOn with
    | add x y hx hy => simp only [map_add, hx, hy]
    | tmul b n => simp [r, g]
  have hinj : Function.Injective (g.lTensor B) := Function.LeftInverse.injective hr
  exact (Module.FaithfullyFlat.lTensor_injective_iff_injective A B g).mp hinj

theorem

lTensor_comm_comp

L872 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.lTensor_comm_comp

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Core
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]
  (φ' : E₁ (A := A) (B := B) N ⟶ E₂ (A := A) (B := B) N)
omit [Module B N] [IsScalarTower A B N] in

Lean source · statement

theorem lTensor_comm_comp (f : N →ₗ[A] N ⊗[A] B) (z : N ⊗[A] B) :
    ((TensorProduct.comm A N B).toLinearMap ∘ₗ f).lTensor B (TensorProduct.comm A N B z) =
      (TensorProduct.comm A N B).toLinearMap.lTensor B
        (TensorProduct.comm A (N ⊗[A] B) B (f.rTensor B z))

abbrev

δt

L881 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.δt

Documentation

Express the descent coaction in the ring-first tensor product.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Core
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]
  (φ' : E₁ (A := A) (B := B) N ⟶ E₂ (A := A) (B := B) N)

Lean source · statement

abbrev δt : N →ₗ[A] B ⊗[A] N

abbrev

ιt

L883 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.ιt

Documentation

The unit-insertion map in the ring-first tensor product.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Core
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]
  (φ' : E₁ (A := A) (B := B) N ⟶ E₂ (A := A) (B := B) N)

Lean source · statement

abbrev ιt : N →ₗ[A] B ⊗[A] N

theorem

ιt_apply

L887 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.ιt_apply

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Core
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]
  (φ' : E₁ (A := A) (B := B) N ⟶ E₂ (A := A) (B := B) N)
omit [Module B N] [IsScalarTower A B N] in

Lean source · statement

theorem ιt_apply (n : N) : ιt (A := A) (B := B) N n = (1 : B) ⊗ₜ n

theorem

Msub_eq

L889 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.Msub_eq

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Core
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]
  (φ' : E₁ (A := A) (B := B) N ⟶ E₂ (A := A) (B := B) N)

Lean source · statement

theorem Msub_eq : Msub N φ' = LinearMap.eqLocus (δt N φ') (ιt (A := A) (B := B) N)

theorem

lTensor_δt_δt

L902 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.lTensor_δt_δt

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Core
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]
  (φ' : E₁ (A := A) (B := B) N ⟶ E₂ (A := A) (B := B) N)

Lean source · statement

theorem lTensor_δt_δt (hcoc : Cocycle (Nc N) φ') (n : N) :
    (δt N φ').lTensor B (δt N φ' n) = (ιt (A := A) (B := B) N).lTensor B (δt N φ' n)

theorem

δt_smul_of_mem

L908 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.δt_smul_of_mem

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Core
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]
  (φ' : E₁ (A := A) (B := B) N ⟶ E₂ (A := A) (B := B) N)

Lean source · statement

theorem δt_smul_of_mem {m : N} (hm : m ∈ Msub N φ') (b : B) : δt N φ' (b • m) = b ⊗ₜ m

theorem

δ_injective

L912 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.δ_injective

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Core
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]
  (φ' : E₁ (A := A) (B := B) N ⟶ E₂ (A := A) (B := B) N)

Lean source · statement

theorem δ_injective [Module.FaithfullyFlat A B] (hφ : Function.Injective φ') : Function.Injective
  (δ N φ')

theorem

δt_injective

L919 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.δt_injective

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Core
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]
  (φ' : E₁ (A := A) (B := B) N ⟶ E₂ (A := A) (B := B) N)

Lean source · statement

theorem δt_injective [Module.FaithfullyFlat A B] (hφ : Function.Injective φ') :
    Function.Injective (δt N φ')

theorem

liftBaseChange_bijective

L923 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.liftBaseChange_bijective

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Core
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]
  (φ' : E₁ (A := A) (B := B) N ⟶ E₂ (A := A) (B := B) N)

Lean source · statement

theorem liftBaseChange_bijective [Module.FaithfullyFlat A B] (hφ : Function.Injective φ')
    (hcoc : Cocycle (Nc N) φ') :
    Function.Bijective ((Msub N φ').subtype.liftBaseChange B)

theorem

isBaseChange_Msub

L961 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.isBaseChange_Msub

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Core
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]
  (φ' : E₁ (A := A) (B := B) N ⟶ E₂ (A := A) (B := B) N)

Lean source · statement

theorem isBaseChange_Msub [Module.FaithfullyFlat A B] (hφ : Function.Injective φ')
    (hcoc : Cocycle (Nc N) φ') :
    IsBaseChange B (Msub N φ').subtype

abbrev

XB

L971 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.XB

Documentation

The extension ring with its original base-ring action via restriction of scalars.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Core
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]
  (φ' : E₁ (A := A) (B := B) N ⟶ E₂ (A := A) (B := B) N)

Lean source · statement

abbrev XB (A B : Type u) [CommRing A] [CommRing B] [Algebra A B]

def

idXB

L975 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.idXB

Documentation

Identify the restricted scalar carrier with the original algebra.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Core
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]
  (φ' : E₁ (A := A) (B := B) N ⟶ E₂ (A := A) (B := B) N)

Lean source · full declaration

def idXB (A B : Type u) [CommRing A] [CommRing B] [Algebra A B] : XB A B ≃ₗ[A] B where
  toFun x := (x : B)
  invFun b := b
  map_add' _ _ := rfl
  map_smul' a x := by
    change algebraMap A B a * (show B from x) = a • (show B from x)
    exact (Algebra.smul_def a (show B from x)).symm
  left_inv _ := rfl
  right_inv _ := rfl

abbrev

EM

L988 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.EM

Documentation

The scalar extension of the candidate descended submodule.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Core
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]
  (φ' : E₁ (A := A) (B := B) N ⟶ E₂ (A := A) (B := B) N)
variable (M : Submodule A N)

Lean source · statement

abbrev EM

def

incl

L991 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.incl

Documentation

The submodule inclusion as a morphism into the restricted module.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Core
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]
  (φ' : E₁ (A := A) (B := B) N ⟶ E₂ (A := A) (B := B) N)
variable (M : Submodule A N)

Lean source · statement

def incl :
    ModuleCat.of A M ⟶ (ModuleCat.restrictScalars (algebraMap A B)).obj (Nc N)

def

θh

L1001 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.θh

Documentation

The scalar-extended submodule inclusion obtained from the extension-restriction adjunction.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Core
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]
  (φ' : E₁ (A := A) (B := B) N ⟶ E₂ (A := A) (B := B) N)
variable (M : Submodule A N)

Lean source · statement

def θh : EM (A := A) (B := B) N M ⟶ Nc N

theorem

θh_tmul

L1004 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.θh_tmul

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Core
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]
  (φ' : E₁ (A := A) (B := B) N ⟶ E₂ (A := A) (B := B) N)
variable (M : Submodule A N)

Lean source · statement

theorem θh_tmul (b : B) (m : M) :
    θh N M ((b ⊗ₜ[A, algebraMap A B] m : EM (A := A) (B := B) N M)) = b • (m : N)

theorem

θh_eq

L1008 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.θh_eq

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Core
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]
  (φ' : E₁ (A := A) (B := B) N ⟶ E₂ (A := A) (B := B) N)
variable (M : Submodule A N)

Lean source · statement

theorem θh_eq (z : EM (A := A) (B := B) N M) :
    θh N M z = M.subtype.liftBaseChange B (TensorProduct.congr (idXB A B) (LinearEquiv.refl A M) z)

theorem

θh_bijective

L1022 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.θh_bijective

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Core
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]
  (φ' : E₁ (A := A) (B := B) N ⟶ E₂ (A := A) (B := B) N)
variable (M : Submodule A N)

Lean source · statement

theorem θh_bijective [Module.FaithfullyFlat A B] (hφ : Function.Injective φ')
    (hcoc : Cocycle (Nc N) φ') :
    Function.Bijective (θh (B := B) N (Msub N φ'))

theorem

isIso_θh

L1036 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.isIso_θh

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Core
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]
  (φ' : E₁ (A := A) (B := B) N ⟶ E₂ (A := A) (B := B) N)
variable (M : Submodule A N)

Lean source · statement

theorem isIso_θh [Module.FaithfullyFlat A B] (hφ : Function.Injective φ')
    (hcoc : Cocycle (Nc N) φ') :
    IsIso (θh (B := B) N (Msub N φ'))

theorem

square

L1043 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent.S17C1.square

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
namespace S17C1
section Core
open ChangeOfRings
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
  (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]
  (φ' : E₁ (A := A) (B := B) N ⟶ E₂ (A := A) (B := B) N)
variable (M : Submodule A N)

Lean source · statement

theorem square (hM : ∀ m ∈ M,
    δ N φ' m = ((1 : R₂ A B) ⊗ₜ[B,(i₂ A B).hom] m : E₂ (A := A) (B := B) N)) :
    (ModuleCat.extendScalars (i₁ A B).hom).map (θh N M) ≫ φ' =
      canonical A B (ModuleCat.of A M) ≫ (ModuleCat.extendScalars (i₂ A B).hom).map (θh N M)

theorem

exists_submodule_isBaseChange_of_cocycle

L1062 ↗

Module.FaithfullyFlat.exists_submodule_isBaseChange_of_cocycle

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.FaithfullyFlatDescent
open TensorProduct CategoryTheory Algebra.DescentCofaces
universe u
open S17C1 in

Lean source · statement

theorem _root_.Module.FaithfullyFlat.exists_submodule_isBaseChange_of_cocycle
    {A B : Type u} [CommRing A] [CommRing B] [Algebra A B] [Module.FaithfullyFlat A B]
    (N : Type u) [AddCommGroup N] [Module B N] [Module A N] [IsScalarTower A B N]
    (φ' : (ModuleCat.extendScalars (i₁ A B).hom).obj (ModuleCat.of B N) ≅
      (ModuleCat.extendScalars (i₂ A B).hom).obj (ModuleCat.of B N))
    (hcocycle : Cocycle (ModuleCat.of B N) φ'.hom) :
    ∃ M : Submodule A N,
      (∀ n : N, n ∈ M ↔
        φ'.hom (((1 : B ⊗[A] B) ⊗ₜ[B] n : (ModuleCat.extendScalars (i₁ A B).hom).obj (ModuleCat.of
          B N))) =
          ((1 : B ⊗[A] B) ⊗ₜ[B] n : (ModuleCat.extendScalars (i₂ A B).hom).obj (ModuleCat.of B N)))
            ∧
      IsBaseChange B M.subtype ∧
      (∃ θ : (ModuleCat.extendScalars (algebraMap A B)).obj (ModuleCat.of A M) ≅ ModuleCat.of B N,
        (∀ (b : B) (m : M),
          θ.hom ((b ⊗ₜ[A] m : (ModuleCat.extendScalars (algebraMap A B)).obj (ModuleCat.of A M))) =
            b • (m : N)) ∧
        (ModuleCat.extendScalars (i₁ A B).hom).map θ.hom ≫ φ'.hom =
          canonical A B (ModuleCat.of A M) ≫ (ModuleCat.extendScalars (i₂ A B).hom).map θ.hom) ∧
      (Module.Invertible B N → Module.Invertible A M)

Module documentation

Effective descent of modules along a faithfully flat algebra

Declarations