Module

HomogeneousLocalization_Away_flat_quotientMk_comp_of_forall_flat_piece.lean

Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.HomogeneousLocalization_Away_flat_quotientMk_comp_of_forall_flat_piece

24 declarations indexed from sourceView source ↗

Module documentation

Homogeneous Localization Away flat quotient Mk comp of forall flat piece

Imports5

Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Mathlib.RingTheory.RingHom.Flat
Mathlib.Tactic.Ext
Mathlib.Tactic.Ring.RingNF
Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.HomogeneousLocalization_Away_flat_fromZeroRingHom_comp_algebraMap_of_forall_flat

Imported by2

def

𝓑

L43 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HomogeneousLocalization_Away_flat_quotientMk_comp_of_forall_flat_piece.AWAYQUOTSOL.𝓑

Documentation

The homogeneous piece of the quotient obtained as the image of the corresponding original piece.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HomogeneousLocalization_Away_flat_quotientMk_comp_of_forall_flat_piece
universe u v
open HomogeneousLocalization
namespace AWAYQUOTSOL
open DirectSum
section Grading
variable {S : Type u} [CommRing S] {A : Type v} [CommRing A] [Algebra S A]
  (𝒜 : ℕ → Submodule S A) [GradedAlgebra 𝒜] (I : Ideal A)

Lean source · statement

def 𝓑 (k : ℕ) : Submodule S (A ⧸ I)

theorem

mk_mem

L45 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HomogeneousLocalization_Away_flat_quotientMk_comp_of_forall_flat_piece.AWAYQUOTSOL.mk_mem

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HomogeneousLocalization_Away_flat_quotientMk_comp_of_forall_flat_piece
universe u v
open HomogeneousLocalization
namespace AWAYQUOTSOL
open DirectSum
section Grading
variable {S : Type u} [CommRing S] {A : Type v} [CommRing A] [Algebra S A]
  (𝒜 : ℕ → Submodule S A) [GradedAlgebra 𝒜] (I : Ideal A)
omit [GradedAlgebra 𝒜] in

Lean source · statement

theorem mk_mem {k : ℕ} {a : A} (ha : a ∈ 𝒜 k) : Ideal.Quotient.mk I a ∈ 𝓑 𝒜 I k

instance

gradedMonoid

L48 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HomogeneousLocalization_Away_flat_quotientMk_comp_of_forall_flat_piece.AWAYQUOTSOL.gradedMonoid

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HomogeneousLocalization_Away_flat_quotientMk_comp_of_forall_flat_piece
universe u v
open HomogeneousLocalization
namespace AWAYQUOTSOL
open DirectSum
section Grading
variable {S : Type u} [CommRing S] {A : Type v} [CommRing A] [Algebra S A]
  (𝒜 : ℕ → Submodule S A) [GradedAlgebra 𝒜] (I : Ideal A)

Lean source · full declaration

instance gradedMonoid : SetLike.GradedMonoid (𝓑 𝒜 I) where
  one_mem := ⟨1, SetLike.one_mem_graded 𝒜, map_one (Ideal.Quotient.mkₐ S I)⟩
  mul_mem := by
    rintro i j x y ⟨a, ha, rfl⟩ ⟨b, hb, rfl⟩
    exact ⟨a * b, SetLike.mul_mem_graded ha hb, map_mul (Ideal.Quotient.mkₐ S I) a b⟩

def

g

L55 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HomogeneousLocalization_Away_flat_quotientMk_comp_of_forall_flat_piece.AWAYQUOTSOL.g

Documentation

The restriction of the quotient map to the indicated homogeneous piece.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HomogeneousLocalization_Away_flat_quotientMk_comp_of_forall_flat_piece
universe u v
open HomogeneousLocalization
namespace AWAYQUOTSOL
open DirectSum
section Grading
variable {S : Type u} [CommRing S] {A : Type v} [CommRing A] [Algebra S A]
  (𝒜 : ℕ → Submodule S A) [GradedAlgebra 𝒜] (I : Ideal A)

Lean source · statement

def g (k : ℕ) : 𝒜 k →ₗ[S] 𝓑 𝒜 I k

theorem

g_apply_coe

L58 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HomogeneousLocalization_Away_flat_quotientMk_comp_of_forall_flat_piece.AWAYQUOTSOL.g_apply_coe

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HomogeneousLocalization_Away_flat_quotientMk_comp_of_forall_flat_piece
universe u v
open HomogeneousLocalization
namespace AWAYQUOTSOL
open DirectSum
section Grading
variable {S : Type u} [CommRing S] {A : Type v} [CommRing A] [Algebra S A]
  (𝒜 : ℕ → Submodule S A) [GradedAlgebra 𝒜] (I : Ideal A)
omit [GradedAlgebra 𝒜] in

Lean source · statement

theorem g_apply_coe (k : ℕ) (a : 𝒜 k) : (g 𝒜 I k a : A ⧸ I) = Ideal.Quotient.mk I a

def

ψ

L61 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HomogeneousLocalization_Away_flat_quotientMk_comp_of_forall_flat_piece.AWAYQUOTSOL.ψ

Documentation

The linear map sending an element to its family of homogeneous components in the quotient.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HomogeneousLocalization_Away_flat_quotientMk_comp_of_forall_flat_piece
universe u v
open HomogeneousLocalization
namespace AWAYQUOTSOL
open DirectSum
section Grading
variable {S : Type u} [CommRing S] {A : Type v} [CommRing A] [Algebra S A]
  (𝒜 : ℕ → Submodule S A) [GradedAlgebra 𝒜] (I : Ideal A)

Lean source · statement

def ψ : A →ₗ[S] ⨁ k, 𝓑 𝒜 I k

theorem

ψ_apply

L64 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HomogeneousLocalization_Away_flat_quotientMk_comp_of_forall_flat_piece.AWAYQUOTSOL.ψ_apply

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HomogeneousLocalization_Away_flat_quotientMk_comp_of_forall_flat_piece
universe u v
open HomogeneousLocalization
namespace AWAYQUOTSOL
open DirectSum
section Grading
variable {S : Type u} [CommRing S] {A : Type v} [CommRing A] [Algebra S A]
  (𝒜 : ℕ → Submodule S A) [GradedAlgebra 𝒜] (I : Ideal A)

Lean source · statement

theorem ψ_apply (a : A) : ψ 𝒜 I a = lmap (g 𝒜 I) (decompose 𝒜 a)

theorem

coe_lmap

L66 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HomogeneousLocalization_Away_flat_quotientMk_comp_of_forall_flat_piece.AWAYQUOTSOL.coe_lmap

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HomogeneousLocalization_Away_flat_quotientMk_comp_of_forall_flat_piece
universe u v
open HomogeneousLocalization
namespace AWAYQUOTSOL
open DirectSum
section Grading
variable {S : Type u} [CommRing S] {A : Type v} [CommRing A] [Algebra S A]
  (𝒜 : ℕ → Submodule S A) [GradedAlgebra 𝒜] (I : Ideal A)
omit [GradedAlgebra 𝒜] in

Lean source · statement

theorem coe_lmap [DecidableEq ℕ] (x : ⨁ k, 𝒜 k) :
    DirectSum.coeLinearMap (𝓑 𝒜 I) (lmap (g 𝒜 I) x) =
      Ideal.Quotient.mkₐ S I (DirectSum.coeLinearMap 𝒜 x)

theorem

ψ_eq_zero

L77 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HomogeneousLocalization_Away_flat_quotientMk_comp_of_forall_flat_piece.AWAYQUOTSOL.ψ_eq_zero

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HomogeneousLocalization_Away_flat_quotientMk_comp_of_forall_flat_piece
universe u v
open HomogeneousLocalization
namespace AWAYQUOTSOL
open DirectSum
section Grading
variable {S : Type u} [CommRing S] {A : Type v} [CommRing A] [Algebra S A]
  (𝒜 : ℕ → Submodule S A) [GradedAlgebra 𝒜] (I : Ideal A)

Lean source · statement

theorem ψ_eq_zero (hI : ∀ a ∈ I, ∀ k : ℕ, (DirectSum.decompose 𝒜 a k : A) ∈ I)
    {a : A} (ha : a ∈ I) : ψ 𝒜 I a = 0

def

δ

L87 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HomogeneousLocalization_Away_flat_quotientMk_comp_of_forall_flat_piece.AWAYQUOTSOL.δ

Documentation

The decomposition map on the quotient by a homogeneous ideal.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HomogeneousLocalization_Away_flat_quotientMk_comp_of_forall_flat_piece
universe u v
open HomogeneousLocalization
namespace AWAYQUOTSOL
open DirectSum
section Grading
variable {S : Type u} [CommRing S] {A : Type v} [CommRing A] [Algebra S A]
  (𝒜 : ℕ → Submodule S A) [GradedAlgebra 𝒜] (I : Ideal A)

Lean source · full declaration

def δ (hI : ∀ a ∈ I, ∀ k : ℕ, (DirectSum.decompose 𝒜 a k : A) ∈ I) :
    (A ⧸ I) →ₗ[S] ⨁ k, 𝓑 𝒜 I k where
  toFun q := Quotient.liftOn' q (ψ 𝒜 I) (fun a b hab => by
    have hab' : a - b ∈ I := (Submodule.quotientRel_def I).1 hab
    have h0 := ψ_eq_zero 𝒜 I hI hab'
    rwa [map_sub, sub_eq_zero] at h0)
  map_add' x y := by
    induction x using Quotient.inductionOn' with | h a =>
    induction y using Quotient.inductionOn' with | h b =>
    exact map_add (ψ 𝒜 I) a b
  map_smul' s x := by
    induction x using Quotient.inductionOn' with | h a =>
    exact map_smul (ψ 𝒜 I) s a

theorem

δ_mk

L101 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HomogeneousLocalization_Away_flat_quotientMk_comp_of_forall_flat_piece.AWAYQUOTSOL.δ_mk

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HomogeneousLocalization_Away_flat_quotientMk_comp_of_forall_flat_piece
universe u v
open HomogeneousLocalization
namespace AWAYQUOTSOL
open DirectSum
section Grading
variable {S : Type u} [CommRing S] {A : Type v} [CommRing A] [Algebra S A]
  (𝒜 : ℕ → Submodule S A) [GradedAlgebra 𝒜] (I : Ideal A)

Lean source · statement

theorem δ_mk (hI : ∀ a ∈ I, ∀ k : ℕ, (DirectSum.decompose 𝒜 a k : A) ∈ I) (a : A) :
    δ 𝒜 I hI (Ideal.Quotient.mk I a) = ψ 𝒜 I a

def

gradedAlgebra

L105 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HomogeneousLocalization_Away_flat_quotientMk_comp_of_forall_flat_piece.AWAYQUOTSOL.gradedAlgebra

Documentation

The grading on the quotient induced by an ideal stable under homogeneous components.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HomogeneousLocalization_Away_flat_quotientMk_comp_of_forall_flat_piece
universe u v
open HomogeneousLocalization
namespace AWAYQUOTSOL
open DirectSum
section Grading
variable {S : Type u} [CommRing S] {A : Type v} [CommRing A] [Algebra S A]
  (𝒜 : ℕ → Submodule S A) [GradedAlgebra 𝒜] (I : Ideal A)

Lean source · statement

def gradedAlgebra
    (hI : ∀ a ∈ I, ∀ k : ℕ, (DirectSum.decompose 𝒜 a k : A) ∈ I) : GradedAlgebra (𝓑 𝒜 I)

theorem

flat_piece

L131 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HomogeneousLocalization_Away_flat_quotientMk_comp_of_forall_flat_piece.AWAYQUOTSOL.flat_piece

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HomogeneousLocalization_Away_flat_quotientMk_comp_of_forall_flat_piece
universe u v
open HomogeneousLocalization
namespace AWAYQUOTSOL
open DirectSum
section Grading
variable {S : Type u} [CommRing S] {A : Type v} [CommRing A] [Algebra S A]
  (𝒜 : ℕ → Submodule S A) [GradedAlgebra 𝒜] (I : Ideal A)
omit [GradedAlgebra 𝒜] in

Lean source · statement

theorem flat_piece (hflat : ∀ k : ℕ, Module.Flat S (↥(𝒜 k) ⧸ Submodule.comap (𝒜 k).subtype
  (I.restrictScalars S)))
    (k : ℕ) : Module.Flat S (𝓑 𝒜 I k)

theorem

algebraMap_mem

L149 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HomogeneousLocalization_Away_flat_quotientMk_comp_of_forall_flat_piece.AWAYQUOTSOL.algebraMap_mem

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HomogeneousLocalization_Away_flat_quotientMk_comp_of_forall_flat_piece
universe u v
open HomogeneousLocalization
namespace AWAYQUOTSOL
open DirectSum
section Grading
variable {S : Type u} [CommRing S] {A : Type v} [CommRing A] [Algebra S A]
  (𝒜 : ℕ → Submodule S A) [GradedAlgebra 𝒜] (I : Ideal A)

Lean source · statement

theorem algebraMap_mem (s : S) : algebraMap S A s ∈ 𝒜 0

def

θ

L161 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HomogeneousLocalization_Away_flat_quotientMk_comp_of_forall_flat_piece.AWAYQUOTSOL.θ

Documentation

The graded ring homomorphism induced by the quotient map.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HomogeneousLocalization_Away_flat_quotientMk_comp_of_forall_flat_piece
universe u v
open HomogeneousLocalization
namespace AWAYQUOTSOL
open DirectSum
section Localise
variable {S : Type u} [CommRing S] {A : Type v} [CommRing A] [Algebra S A]
  (𝒜 : ℕ → Submodule S A) [GradedAlgebra 𝒜] (I : Ideal A) [GradedAlgebra (𝓑 𝒜 I)]

Lean source · statement

def θ : 𝒜 →+*ᵍ 𝓑 𝒜 I

theorem

θ_apply

L165 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HomogeneousLocalization_Away_flat_quotientMk_comp_of_forall_flat_piece.AWAYQUOTSOL.θ_apply

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HomogeneousLocalization_Away_flat_quotientMk_comp_of_forall_flat_piece
universe u v
open HomogeneousLocalization
namespace AWAYQUOTSOL
open DirectSum
section Localise
variable {S : Type u} [CommRing S] {A : Type v} [CommRing A] [Algebra S A]
  (𝒜 : ℕ → Submodule S A) [GradedAlgebra 𝒜] (I : Ideal A) [GradedAlgebra (𝓑 𝒜 I)]
omit [GradedAlgebra 𝒜] [GradedAlgebra (𝓑 𝒜 I)] in

Lean source · statement

theorem θ_apply (a : A) : θ 𝒜 I a = Ideal.Quotient.mk I a

def

Φ

L170 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HomogeneousLocalization_Away_flat_quotientMk_comp_of_forall_flat_piece.AWAYQUOTSOL.Φ

Documentation

The map of homogeneous localizations induced by the graded quotient homomorphism.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HomogeneousLocalization_Away_flat_quotientMk_comp_of_forall_flat_piece
universe u v
open HomogeneousLocalization
namespace AWAYQUOTSOL
open DirectSum
section Localise
variable {S : Type u} [CommRing S] {A : Type v} [CommRing A] [Algebra S A]
  (𝒜 : ℕ → Submodule S A) [GradedAlgebra 𝒜] (I : Ideal A) [GradedAlgebra (𝓑 𝒜 I)]
variable {d : ℕ} {f : A}

Lean source · statement

def Φ (f : A) : Away 𝒜 f →+* Away (𝓑 𝒜 I) (θ 𝒜 I f)

theorem

Φ_surjective

L172 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HomogeneousLocalization_Away_flat_quotientMk_comp_of_forall_flat_piece.AWAYQUOTSOL.Φ_surjective

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HomogeneousLocalization_Away_flat_quotientMk_comp_of_forall_flat_piece
universe u v
open HomogeneousLocalization
namespace AWAYQUOTSOL
open DirectSum
section Localise
variable {S : Type u} [CommRing S] {A : Type v} [CommRing A] [Algebra S A]
  (𝒜 : ℕ → Submodule S A) [GradedAlgebra 𝒜] (I : Ideal A) [GradedAlgebra (𝓑 𝒜 I)]
variable {d : ℕ} {f : A}

Lean source · statement

theorem Φ_surjective (hf : f ∈ 𝒜 d) : Function.Surjective (Φ 𝒜 I f)

def

G

L179 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HomogeneousLocalization_Away_flat_quotientMk_comp_of_forall_flat_piece.AWAYQUOTSOL.G

Documentation

The homogeneous fractions admitting a numerator in the specified ideal.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HomogeneousLocalization_Away_flat_quotientMk_comp_of_forall_flat_piece
universe u v
open HomogeneousLocalization
namespace AWAYQUOTSOL
open DirectSum
section Localise
variable {S : Type u} [CommRing S] {A : Type v} [CommRing A] [Algebra S A]
  (𝒜 : ℕ → Submodule S A) [GradedAlgebra 𝒜] (I : Ideal A) [GradedAlgebra (𝓑 𝒜 I)]
variable {d : ℕ} {f : A}

Lean source · statement

def G (f : A) : Set (Away 𝒜 f)

theorem

ker_Φ

L183 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HomogeneousLocalization_Away_flat_quotientMk_comp_of_forall_flat_piece.AWAYQUOTSOL.ker_Φ

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HomogeneousLocalization_Away_flat_quotientMk_comp_of_forall_flat_piece
universe u v
open HomogeneousLocalization
namespace AWAYQUOTSOL
open DirectSum
section Localise
variable {S : Type u} [CommRing S] {A : Type v} [CommRing A] [Algebra S A]
  (𝒜 : ℕ → Submodule S A) [GradedAlgebra 𝒜] (I : Ideal A) [GradedAlgebra (𝓑 𝒜 I)]
variable {d : ℕ} {f : A}

Lean source · statement

theorem ker_Φ (hf : f ∈ 𝒜 d) : RingHom.ker (Φ 𝒜 I f) = Ideal.span (G 𝒜 I f)

abbrev

φ

L216 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HomogeneousLocalization_Away_flat_quotientMk_comp_of_forall_flat_piece.AWAYQUOTSOL.φ

Documentation

The base-ring map to the homogeneous localization through the degree-zero projection.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HomogeneousLocalization_Away_flat_quotientMk_comp_of_forall_flat_piece
universe u v
open HomogeneousLocalization
namespace AWAYQUOTSOL
open DirectSum
section Localise
variable {S : Type u} [CommRing S] {A : Type v} [CommRing A] [Algebra S A]
  (𝒜 : ℕ → Submodule S A) [GradedAlgebra 𝒜] (I : Ideal A) [GradedAlgebra (𝓑 𝒜 I)]
variable {d : ℕ} {f : A}

Lean source · statement

abbrev φ (f : A) : S →+* Away 𝒜 f

theorem

Φ_comp_φ

L220 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HomogeneousLocalization_Away_flat_quotientMk_comp_of_forall_flat_piece.AWAYQUOTSOL.Φ_comp_φ

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HomogeneousLocalization_Away_flat_quotientMk_comp_of_forall_flat_piece
universe u v
open HomogeneousLocalization
namespace AWAYQUOTSOL
open DirectSum
section Localise
variable {S : Type u} [CommRing S] {A : Type v} [CommRing A] [Algebra S A]
  (𝒜 : ℕ → Submodule S A) [GradedAlgebra 𝒜] (I : Ideal A) [GradedAlgebra (𝓑 𝒜 I)]
variable {d : ℕ} {f : A}

Lean source · statement

theorem Φ_comp_φ :
    (Φ 𝒜 I f).comp (φ 𝒜 f) =
      (HomogeneousLocalization.fromZeroRingHom (𝓑 𝒜 I) (Submonoid.powers (θ 𝒜 I f))).comp
        ((GradedRing.projZeroRingHom' (𝓑 𝒜 I)).comp (algebraMap S (A ⧸ I)))

theorem

flat_of_eq

L244 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HomogeneousLocalization_Away_flat_quotientMk_comp_of_forall_flat_piece.AWAYQUOTSOL.flat_of_eq

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HomogeneousLocalization_Away_flat_quotientMk_comp_of_forall_flat_piece
universe u v
open HomogeneousLocalization
namespace AWAYQUOTSOL
open DirectSum

Lean source · statement

theorem flat_of_eq {R : Type u} {B : Type v} [CommRing R] [CommRing B] (φ' : R →+* B)
    {J J' : Ideal B} (h : J = J') (hJ' : ((Ideal.Quotient.mk J').comp φ').Flat) :
    ((Ideal.Quotient.mk J).comp φ').Flat

theorem

flat_quotientMk_comp_of_forall_flat_piece

L255 ↗

HomogeneousLocalization.Away.flat_quotientMk_comp_of_forall_flat_piece

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HomogeneousLocalization_Away_flat_quotientMk_comp_of_forall_flat_piece
universe u v
open HomogeneousLocalization
attribute [local instance] AWAYQUOTSOL.gradedMonoid
open AWAYQUOTSOL DirectSum in

Lean source · statement

theorem _root_.HomogeneousLocalization.Away.flat_quotientMk_comp_of_forall_flat_piece
    {S : Type u} [CommRing S] {A : Type v} [CommRing A] [Algebra S A]
    (𝒜 : ℕ → Submodule S A) [GradedAlgebra 𝒜]
    (I : Ideal A) (hI : ∀ a ∈ I, ∀ k : ℕ, (DirectSum.decompose 𝒜 a k : A) ∈ I)
    (hflat : ∀ k : ℕ, Module.Flat S (↥(𝒜 k) ⧸ Submodule.comap (𝒜 k).subtype (I.restrictScalars S)))
    {d : ℕ} (f : A) (hf : f ∈ 𝒜 d) :
    ((Ideal.Quotient.mk (Ideal.span {x : Away 𝒜 f |
          ∃ y : NumDenSameDeg 𝒜 (Submonoid.powers f), (y.num : A) ∈ I ∧ HomogeneousLocalization.mk
            y = x})).comp
      ((HomogeneousLocalization.fromZeroRingHom 𝒜 (Submonoid.powers f)).comp
        ((GradedRing.projZeroRingHom' 𝒜).comp (algebraMap S A)))).Flat

Module documentation

Homogeneous Localization Away flat quotient Mk comp of forall flat piece

Declarations