Module

Scheme_IdealSheafData_IsInvertible_mul_left_cancel.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_IdealSheafData_IsInvertible_mul_left_cancel

2 declarations indexed from sourceView source ↗

Module documentation

Cancellation by an invertible ideal sheaf

Multiplication by an invertible ideal sheaf can be cancelled from equality of ideal-sheaf products, using local non-zero-divisor generators.

Imports1

Nyll.AlgebraicCurves.RelativeDivisors.Cartier

Imported by5

theorem

span_singleton_mul_right_injective_of_mem_nonZeroDivisors

L32 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_IsInvertible_mul_left_cancel.Ideal.span_singleton_mul_right_injective_of_mem_nonZeroDivisors

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_IsInvertible_mul_left_cancel
universe u
open scoped _root_.Ideal in

Lean source · full declaration

theorem Ideal.span_singleton_mul_right_injective_of_mem_nonZeroDivisors {R : Type*} [CommRing R]
    {a : R} (ha : a ∈ nonZeroDivisors R) :
    Function.Injective fun K : Ideal R ↦ Ideal.span {a} * K := by
  suffices key : ∀ K K' : Ideal R, Ideal.span {a} * K = Ideal.span {a} * K' → K ≤ K' from
    fun K K' h ↦ le_antisymm (key K K' h) (key K' K h.symm)
  intro K K' h x hx
  have hax : a * x ∈ Ideal.span {a} * K' := h ▸ Ideal.mem_span_singleton_mul.mpr ⟨x, hx, rfl⟩
  obtain ⟨y, hy, hyx⟩ := Ideal.mem_span_singleton_mul.mp hax
  rwa [← (mul_cancel_left_mem_nonZeroDivisors ha).mp hyx]

theorem

mul_left_cancel

L44 ↗

AlgebraicGeometry.Scheme.IdealSheafData.IsInvertible.mul_left_cancel