NYLL
Module

HomogeneousLocalization_Away_flat_fromZeroRingHom_comp_algebraMap_of_forall_flat.lean

Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.HomogeneousLocalization_Away_flat_fromZeroRingHom_comp_algebraMap_of_forall_flat
19 declarations indexed from sourceView source ↗

Module documentation

Homogeneous Localization Away flat from Zero Ring Hom comp algebra Map of forall flat

Imports2
  • Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
  • Mathlib.RingTheory.RingHom.Flat
Imported by2

Declarations

abbrev

φ

L37 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HomogeneousLocalization_Away_flat_fromZeroRingHom_comp_algebraMap_of_forall_flat.AWAYFLATSOL.φ
Documentation

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

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HomogeneousLocalization_Away_flat_fromZeroRingHom_comp_algebraMap_of_forall_flat
universe u v
open HomogeneousLocalization
namespace AWAYFLATSOL
open DirectSum
variable {S : Type u} [CommRing S] {A : Type v} [CommRing A] [Algebra S A]
  (𝒜 : ℕ → Submodule S A) [GradedAlgebra 𝒜] {d : ℕ} {f : A} (hf : f ∈ 𝒜 d)
Lean source · statement
abbrev φ (f : A) : S →+* Away 𝒜 f
theorem

algebraMap_mem

L41 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HomogeneousLocalization_Away_flat_fromZeroRingHom_comp_algebraMap_of_forall_flat.AWAYFLATSOL.algebraMap_mem
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HomogeneousLocalization_Away_flat_fromZeroRingHom_comp_algebraMap_of_forall_flat
universe u v
open HomogeneousLocalization
namespace AWAYFLATSOL
open DirectSum
variable {S : Type u} [CommRing S] {A : Type v} [CommRing A] [Algebra S A]
  (𝒜 : ℕ → Submodule S A) [GradedAlgebra 𝒜] {d : ℕ} {f : A} (hf : f ∈ 𝒜 d)
Lean source · statement
theorem algebraMap_mem (s : S) : algebraMap S A s ∈ 𝒜 0
theorem

val_φ

L45 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HomogeneousLocalization_Away_flat_fromZeroRingHom_comp_algebraMap_of_forall_flat.AWAYFLATSOL.val_φ
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HomogeneousLocalization_Away_flat_fromZeroRingHom_comp_algebraMap_of_forall_flat
universe u v
open HomogeneousLocalization
namespace AWAYFLATSOL
open DirectSum
variable {S : Type u} [CommRing S] {A : Type v} [CommRing A] [Algebra S A]
  (𝒜 : ℕ → Submodule S A) [GradedAlgebra 𝒜] {d : ℕ} {f : A} (hf : f ∈ 𝒜 d)
Lean source · statement
theorem val_φ (s : S) :
    (φ 𝒜 f s).val = algebraMap S (Localization (Submonoid.powers f)) s
theorem

decompose_mul_shift

L54 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HomogeneousLocalization_Away_flat_fromZeroRingHom_comp_algebraMap_of_forall_flat.AWAYFLATSOL.decompose_mul_shift
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HomogeneousLocalization_Away_flat_fromZeroRingHom_comp_algebraMap_of_forall_flat
universe u v
open HomogeneousLocalization
namespace AWAYFLATSOL
open DirectSum
variable {S : Type u} [CommRing S] {A : Type v} [CommRing A] [Algebra S A]
  (𝒜 : ℕ → Submodule S A) [GradedAlgebra 𝒜] {d : ℕ} {f : A} (hf : f ∈ 𝒜 d)
Lean source · statement
theorem decompose_mul_shift {a b : A} {i j n : ℕ} (ha : a ∈ 𝒜 i) (hn : n = i + j) :
    (decompose 𝒜 (a * b) n : A) = a * decompose 𝒜 b j
def

expo

L60 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HomogeneousLocalization_Away_flat_fromZeroRingHom_comp_algebraMap_of_forall_flat.AWAYFLATSOL.expo
Documentation

A chosen exponent expressing the denominator as a power of the distinguished homogeneous element.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HomogeneousLocalization_Away_flat_fromZeroRingHom_comp_algebraMap_of_forall_flat
universe u v
open HomogeneousLocalization
namespace AWAYFLATSOL
open DirectSum
variable {S : Type u} [CommRing S] {A : Type v} [CommRing A] [Algebra S A]
  (𝒜 : ℕ → Submodule S A) [GradedAlgebra 𝒜] {d : ℕ} {f : A} (hf : f ∈ 𝒜 d)
Lean source · statement
def expo (b : Submonoid.powers f) : ℕ
theorem

pow_expo

L62 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HomogeneousLocalization_Away_flat_fromZeroRingHom_comp_algebraMap_of_forall_flat.AWAYFLATSOL.pow_expo
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HomogeneousLocalization_Away_flat_fromZeroRingHom_comp_algebraMap_of_forall_flat
universe u v
open HomogeneousLocalization
namespace AWAYFLATSOL
open DirectSum
variable {S : Type u} [CommRing S] {A : Type v} [CommRing A] [Algebra S A]
  (𝒜 : ℕ → Submodule S A) [GradedAlgebra 𝒜] {d : ℕ} {f : A} (hf : f ∈ 𝒜 d)
Lean source · statement
theorem pow_expo (b : Submonoid.powers f) : f ^ expo b = (b : A)
theorem

mem_of_pow_eq

L65 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HomogeneousLocalization_Away_flat_fromZeroRingHom_comp_algebraMap_of_forall_flat.AWAYFLATSOL.mem_of_pow_eq
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_fromZeroRingHom_comp_algebraMap_of_forall_flat
universe u v
open HomogeneousLocalization
namespace AWAYFLATSOL
open DirectSum
variable {S : Type u} [CommRing S] {A : Type v} [CommRing A] [Algebra S A]
  (𝒜 : ℕ → Submodule S A) [GradedAlgebra 𝒜] {d : ℕ} {f : A} (hf : f ∈ 𝒜 d)
include hf in
Lean source · statement
theorem mem_of_pow_eq {b : Submonoid.powers f} {k : ℕ} (hk : f ^ k = (b : A)) :
    (b : A) ∈ 𝒜 (k • d)
def

F'

L70 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HomogeneousLocalization_Away_flat_fromZeroRingHom_comp_algebraMap_of_forall_flat.AWAYFLATSOL.F'
Documentation

The homogeneous fraction formed from the component matching the specified denominator degree.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HomogeneousLocalization_Away_flat_fromZeroRingHom_comp_algebraMap_of_forall_flat
universe u v
open HomogeneousLocalization
namespace AWAYFLATSOL
open DirectSum
variable {S : Type u} [CommRing S] {A : Type v} [CommRing A] [Algebra S A]
  (𝒜 : ℕ → Submodule S A) [GradedAlgebra 𝒜] {d : ℕ} {f : A} (hf : f ∈ 𝒜 d)
Lean source · statement
def F' (a : A) (b : Submonoid.powers f) (k : ℕ) (hk : f ^ k = (b : A)) : Away 𝒜 f
theorem

val_F'

L77 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HomogeneousLocalization_Away_flat_fromZeroRingHom_comp_algebraMap_of_forall_flat.AWAYFLATSOL.val_F'
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HomogeneousLocalization_Away_flat_fromZeroRingHom_comp_algebraMap_of_forall_flat
universe u v
open HomogeneousLocalization
namespace AWAYFLATSOL
open DirectSum
variable {S : Type u} [CommRing S] {A : Type v} [CommRing A] [Algebra S A]
  (𝒜 : ℕ → Submodule S A) [GradedAlgebra 𝒜] {d : ℕ} {f : A} (hf : f ∈ 𝒜 d)
Lean source · statement
theorem val_F' (a : A) (b : Submonoid.powers f) (k : ℕ) (hk : f ^ k = (b : A)) :
    (F' 𝒜 hf a b k hk).val = Localization.mk (decompose 𝒜 a (k • d) : A) b
theorem

smul_deg_eq

L80 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HomogeneousLocalization_Away_flat_fromZeroRingHom_comp_algebraMap_of_forall_flat.AWAYFLATSOL.smul_deg_eq
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_fromZeroRingHom_comp_algebraMap_of_forall_flat
universe u v
open HomogeneousLocalization
namespace AWAYFLATSOL
open DirectSum
variable {S : Type u} [CommRing S] {A : Type v} [CommRing A] [Algebra S A]
  (𝒜 : ℕ → Submodule S A) [GradedAlgebra 𝒜] {d : ℕ} {f : A} (hf : f ∈ 𝒜 d)
include hf in
Lean source · statement
theorem smul_deg_eq {k k' : ℕ} (h : f ^ k = f ^ k') (h0 : (0 : A) ∉ Submonoid.powers f) :
    k • d = k' • d
theorem

F'_indep

L86 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HomogeneousLocalization_Away_flat_fromZeroRingHom_comp_algebraMap_of_forall_flat.AWAYFLATSOL.F'_indep
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HomogeneousLocalization_Away_flat_fromZeroRingHom_comp_algebraMap_of_forall_flat
universe u v
open HomogeneousLocalization
namespace AWAYFLATSOL
open DirectSum
variable {S : Type u} [CommRing S] {A : Type v} [CommRing A] [Algebra S A]
  (𝒜 : ℕ → Submodule S A) [GradedAlgebra 𝒜] {d : ℕ} {f : A} (hf : f ∈ 𝒜 d)
Lean source · statement
theorem F'_indep (a : A) (b : Submonoid.powers f) (k k' : ℕ) (hk : f ^ k = (b : A)) (hk' : f ^ k' =
  (b : A)) :
    F' 𝒜 hf a b k hk = F' 𝒜 hf a b k' hk'
def

F

L95 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HomogeneousLocalization_Away_flat_fromZeroRingHom_comp_algebraMap_of_forall_flat.AWAYFLATSOL.F
Documentation

The homogeneous fraction formed using a chosen exponent of the denominator.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HomogeneousLocalization_Away_flat_fromZeroRingHom_comp_algebraMap_of_forall_flat
universe u v
open HomogeneousLocalization
namespace AWAYFLATSOL
open DirectSum
variable {S : Type u} [CommRing S] {A : Type v} [CommRing A] [Algebra S A]
  (𝒜 : ℕ → Submodule S A) [GradedAlgebra 𝒜] {d : ℕ} {f : A} (hf : f ∈ 𝒜 d)
Lean source · statement
def F (a : A) (b : Submonoid.powers f) : Away 𝒜 f
theorem

val_F

L97 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HomogeneousLocalization_Away_flat_fromZeroRingHom_comp_algebraMap_of_forall_flat.AWAYFLATSOL.val_F
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HomogeneousLocalization_Away_flat_fromZeroRingHom_comp_algebraMap_of_forall_flat
universe u v
open HomogeneousLocalization
namespace AWAYFLATSOL
open DirectSum
variable {S : Type u} [CommRing S] {A : Type v} [CommRing A] [Algebra S A]
  (𝒜 : ℕ → Submodule S A) [GradedAlgebra 𝒜] {d : ℕ} {f : A} (hf : f ∈ 𝒜 d)
Lean source · statement
theorem val_F (a : A) (b : Submonoid.powers f) :
    (F 𝒜 hf a b).val = Localization.mk (decompose 𝒜 a (expo b • d) : A) b
theorem

F_wd

L100 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HomogeneousLocalization_Away_flat_fromZeroRingHom_comp_algebraMap_of_forall_flat.AWAYFLATSOL.F_wd
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HomogeneousLocalization_Away_flat_fromZeroRingHom_comp_algebraMap_of_forall_flat
universe u v
open HomogeneousLocalization
namespace AWAYFLATSOL
open DirectSum
variable {S : Type u} [CommRing S] {A : Type v} [CommRing A] [Algebra S A]
  (𝒜 : ℕ → Submodule S A) [GradedAlgebra 𝒜] {d : ℕ} {f : A} (hf : f ∈ 𝒜 d)
Lean source · statement
theorem F_wd {a c : A} {b e : Submonoid.powers f}
    (h : Localization.r (Submonoid.powers f) (a, b) (c, e)) : F 𝒜 hf a b = F 𝒜 hf c e
def

retr

L121 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HomogeneousLocalization_Away_flat_fromZeroRingHom_comp_algebraMap_of_forall_flat.AWAYFLATSOL.retr
Documentation

The map from ordinary localization to homogeneous localization induced by homogeneous components.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HomogeneousLocalization_Away_flat_fromZeroRingHom_comp_algebraMap_of_forall_flat
universe u v
open HomogeneousLocalization
namespace AWAYFLATSOL
open DirectSum
variable {S : Type u} [CommRing S] {A : Type v} [CommRing A] [Algebra S A]
  (𝒜 : ℕ → Submodule S A) [GradedAlgebra 𝒜] {d : ℕ} {f : A} (hf : f ∈ 𝒜 d)
Lean source · statement
def retr (x : Localization (Submonoid.powers f)) : Away 𝒜 f
theorem

retr_mk

L124 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HomogeneousLocalization_Away_flat_fromZeroRingHom_comp_algebraMap_of_forall_flat.AWAYFLATSOL.retr_mk
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HomogeneousLocalization_Away_flat_fromZeroRingHom_comp_algebraMap_of_forall_flat
universe u v
open HomogeneousLocalization
namespace AWAYFLATSOL
open DirectSum
variable {S : Type u} [CommRing S] {A : Type v} [CommRing A] [Algebra S A]
  (𝒜 : ℕ → Submodule S A) [GradedAlgebra 𝒜] {d : ℕ} {f : A} (hf : f ∈ 𝒜 d)
Lean source · statement
theorem retr_mk (a : A) (b : Submonoid.powers f) :
    retr 𝒜 hf (Localization.mk a b) = F 𝒜 hf a b
theorem

retr_add

L128 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HomogeneousLocalization_Away_flat_fromZeroRingHom_comp_algebraMap_of_forall_flat.AWAYFLATSOL.retr_add
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HomogeneousLocalization_Away_flat_fromZeroRingHom_comp_algebraMap_of_forall_flat
universe u v
open HomogeneousLocalization
namespace AWAYFLATSOL
open DirectSum
variable {S : Type u} [CommRing S] {A : Type v} [CommRing A] [Algebra S A]
  (𝒜 : ℕ → Submodule S A) [GradedAlgebra 𝒜] {d : ℕ} {f : A} (hf : f ∈ 𝒜 d)
Lean source · statement
theorem retr_add (x y : Localization (Submonoid.powers f)) :
    retr 𝒜 hf (x + y) = retr 𝒜 hf x + retr 𝒜 hf y
theorem

val_F_smul

L150 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HomogeneousLocalization_Away_flat_fromZeroRingHom_comp_algebraMap_of_forall_flat.AWAYFLATSOL.val_F_smul
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HomogeneousLocalization_Away_flat_fromZeroRingHom_comp_algebraMap_of_forall_flat
universe u v
open HomogeneousLocalization
namespace AWAYFLATSOL
open DirectSum
variable {S : Type u} [CommRing S] {A : Type v} [CommRing A] [Algebra S A]
  (𝒜 : ℕ → Submodule S A) [GradedAlgebra 𝒜] {d : ℕ} {f : A} (hf : f ∈ 𝒜 d)
Lean source · statement
theorem val_F_smul (s : S) (a : A) (b : Submonoid.powers f) :
    (F 𝒜 hf (s • a) b).val = s • (F 𝒜 hf a b).val
theorem

flat_fromZeroRingHom_comp_algebraMap_of_forall_flat

L157 ↗
HomogeneousLocalization.Away.flat_fromZeroRingHom_comp_algebraMap_of_forall_flat
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HomogeneousLocalization_Away_flat_fromZeroRingHom_comp_algebraMap_of_forall_flat
universe u v
open HomogeneousLocalization
open AWAYFLATSOL DirectSum in
Lean source · statement
theorem _root_.HomogeneousLocalization.Away.flat_fromZeroRingHom_comp_algebraMap_of_forall_flat
    {S : Type u} [CommRing S] {A : Type v} [CommRing A] [Algebra S A]
    (𝒜 : ℕ → Submodule S A) [GradedAlgebra 𝒜]
    (hflat : ∀ n : ℕ, Module.Flat S (𝒜 n))
    {d : ℕ} (f : A) (hf : f ∈ 𝒜 d) :
    ((HomogeneousLocalization.fromZeroRingHom 𝒜 (Submonoid.powers f)).comp
        ((GradedRing.projZeroRingHom' 𝒜).comp (algebraMap S A))).Flat

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