NYLL
Module

Scheme_TwoAffineOpenCover_H1baseChangeMap_surjective_and_eq_iff_of_surjective.lean

Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_TwoAffineOpenCover_H1baseChangeMap_surjective_and_eq_iff_of_surjective
6 declarations indexed from sourceView source ↗

Module documentation

Scheme Two Affine Open Cover H1base Change Map surjective and eq iff of surjective

Imports6
Imported by2

Declarations

theorem

exists_eq_one_tmul

L42 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_H1baseChangeMap_surjective_and_eq_iff_of_surjective.PicTanH1BC.exists_eq_one_tmul
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_H1baseChangeMap_surjective_and_eq_iff_of_surjective
universe u
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry NeronModelInfra
  AlgebraicGeometry.Scheme.TwoAffineOpenCover
open scoped TensorProduct
namespace PicTanH1BC
section Algebra
variable {R : Type u} [CommRing R] {A : Type u} [CommRing A] [Algebra R A]
Lean source · statement
theorem exists_eq_one_tmul (hA : Function.Surjective (algebraMap R A)) {P : Type*} [AddCommGroup P]
  [Module R P]
    (w : A ⊗[R] P) : ∃ p : P, w = (1 : A) ⊗ₜ[R] p
theorem

one_tmul_eq_one_tmul_iff

L54 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_H1baseChangeMap_surjective_and_eq_iff_of_surjective.PicTanH1BC.one_tmul_eq_one_tmul_iff
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_H1baseChangeMap_surjective_and_eq_iff_of_surjective
universe u
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry NeronModelInfra
  AlgebraicGeometry.Scheme.TwoAffineOpenCover
open scoped TensorProduct
namespace PicTanH1BC
section Algebra
variable {R : Type u} [CommRing R] {A : Type u} [CommRing A] [Algebra R A]
Lean source · statement
theorem one_tmul_eq_one_tmul_iff (hA : Function.Surjective (algebraMap R A)) {M : Type*}
  [AddCommGroup M]
    [Module R M] (m n : M) :
    (1 : A) ⊗ₜ[R] m = (1 : A) ⊗ₜ[R] n ↔ m - n ∈ RingHom.ker (algebraMap R A) • (⊤ : Submodule R M)
theorem

smul_top_quotient

L73 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_H1baseChangeMap_surjective_and_eq_iff_of_surjective.PicTanH1BC.smul_top_quotient
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_H1baseChangeMap_surjective_and_eq_iff_of_surjective
universe u
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry NeronModelInfra
  AlgebraicGeometry.Scheme.TwoAffineOpenCover
open scoped TensorProduct
namespace PicTanH1BC
section Algebra
variable {R : Type u} [CommRing R] {A : Type u} [CommRing A] [Algebra R A]
Lean source · statement
theorem smul_top_quotient {M : Type*} [AddCommGroup M] [Module R M] (I : Ideal R) (N : Submodule R
  M) :
    (I • (⊤ : Submodule R (M ⧸ N))) = (I • (⊤ : Submodule R M)).map N.mkQ
theorem

one_tmul_mem_range_baseChange_iff

L78 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_H1baseChangeMap_surjective_and_eq_iff_of_surjective.PicTanH1BC.one_tmul_mem_range_baseChange_iff
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_H1baseChangeMap_surjective_and_eq_iff_of_surjective
universe u
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry NeronModelInfra
  AlgebraicGeometry.Scheme.TwoAffineOpenCover
open scoped TensorProduct
namespace PicTanH1BC
section Algebra
variable {R : Type u} [CommRing R] {A : Type u} [CommRing A] [Algebra R A]
Lean source · statement
theorem one_tmul_mem_range_baseChange_iff (hA : Function.Surjective (algebraMap R A))
    {P M : Type*} [AddCommGroup P] [Module R P] [AddCommGroup M] [Module R M] (d : P →ₗ[R] M) (p :
      M) :
    (1 : A) ⊗ₜ[R] p ∈ LinearMap.range (d.baseChange A) ↔
      (Submodule.Quotient.mk p : M ⧸ LinearMap.range d) ∈
        RingHom.ker (algebraMap R A) • (⊤ : Submodule R (M ⧸ LinearMap.range d))
theorem

main

L108 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_H1baseChangeMap_surjective_and_eq_iff_of_surjective.PicTanH1BC.main
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_H1baseChangeMap_surjective_and_eq_iff_of_surjective
universe u
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry NeronModelInfra
  AlgebraicGeometry.Scheme.TwoAffineOpenCover
open scoped TensorProduct
namespace PicTanH1BC
section Main
Lean source · statement
theorem main {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec
  (.of R))
    (A : Type u) [CommRing A] [Algebra R A] (hA : Function.Surjective (algebraMap R A)) :
    Function.Surjective (𝒱.H1baseChangeMap c A) ∧
    ∀ x y : (𝒱.structureSheafSections c).H1,
      𝒱.H1baseChangeMap c A x = 𝒱.H1baseChangeMap c A y ↔
        x - y ∈ RingHom.ker (algebraMap R A) • (⊤ : Submodule R (𝒱.structureSheafSections c).H1)
theorem

H1baseChangeMap_surjective_and_eq_iff_of_surjective

L154 ↗
AlgebraicGeometry.Scheme.TwoAffineOpenCover.H1baseChangeMap_surjective_and_eq_iff_of_surjective
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
universe u
open _root_.AlgebraicCurves.Geometry.Schemes.Proofs in
open Scheme_TwoAffineOpenCover_H1baseChangeMap_surjective_and_eq_iff_of_surjective in
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry NeronModelInfra in
open scoped TensorProduct in
open AlgebraicGeometry.Scheme.TwoAffineOpenCover in
Lean source · statement
theorem H1baseChangeMap_surjective_and_eq_iff_of_surjective
    {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of R))
    (A : Type u) [CommRing A] [Algebra R A] (hA : Function.Surjective (algebraMap R A)) :
    Function.Surjective (𝒱.H1baseChangeMap c A) ∧
    ∀ x y : (𝒱.structureSheafSections c).H1,
      𝒱.H1baseChangeMap c A x = 𝒱.H1baseChangeMap c A y ↔
        x - y ∈ RingHom.ker (algebraMap R A) • (⊤ : Submodule R (𝒱.structureSheafSections c).H1)

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