Documentation

TauCeti.RingTheory.FittingIdeal.Generators

Computing Fitting ideals from relation generators #

The definition of Submodule.minorsIdeal allows arbitrary elements of a relation submodule as rows of a minor. If the relations are generated by a set s, multilinearity of the determinant reduces the ideal to minors whose rows belong to s. This gives a presentation formula for TauCeti.fittingIdeal that can be used with explicit finite lists of relations, particularly when computing the singular locus of a curve from its module of relative differentials.

source
def TauCeti.minorsIdealOfSet {R : Type u_1} {F : Type u_2} [CommRing R] [AddCommGroup F] [Module R F] (s : Set F) (p : ℕ) :
Ideal R

The ideal generated by the p-minors formed from rows in a set s.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem TauCeti.minorsIdealOfSet_def {R : Type u_1} {F : Type u_2} [CommRing R] [AddCommGroup F] [Module R F] (s : Set F) (p : ℕ) :
    minorsIdealOfSet s p = Ideal.span {r : R | ∃ (f : Fin p → Module.Dual R F) (v : Fin p → F), (∀ (i : Fin p), v i ∈ s) ∧ (Matrix.of fun (i j : Fin p) => (f j) (v i)).det = r}

    The generators defining the minors ideal of a set.

    source
    theorem TauCeti.det_mem_minorsIdealOfSet {R : Type u_1} {F : Type u_2} [CommRing R] [AddCommGroup F] [Module R F] {s : Set F} {p : ℕ} (f : Fin p → Module.Dual R F) {v : Fin p → F} (hv : ∀ (i : Fin p), v i ∈ s) :
    (Matrix.of fun (i j : Fin p) => (f j) (v i)).det ∈ minorsIdealOfSet s p

    A determinant whose rows belong to s lies in minorsIdealOfSet s p.

    source
    theorem TauCeti.minorsIdealOfSet_induction {R : Type u_1} {F : Type u_2} [CommRing R] [AddCommGroup F] [Module R F] {s : Set F} {p : ℕ} {P : R → Prop} {x : R} (hx : x ∈ minorsIdealOfSet s p) (hdet : ∀ (f : Fin p → Module.Dual R F) (v : Fin p → F), (∀ (i : Fin p), v i ∈ s) → P (Matrix.of fun (i j : Fin p) => (f j) (v i)).det) (hzero : P 0) (hadd : ∀ (x y : R), P x → P y → P (x + y)) (hsmul : ∀ (a x : R), P x → P (a * x)) :
    P x

    Prove a property of every element of minorsIdealOfSet s p from the generating determinants and closure under the ideal operations.

    source
    @[simp]
    theorem Submodule.minorsIdeal_span {R : Type u_1} {F : Type u_2} [CommRing R] [AddCommGroup F] [Module R F] (s : Set F) (p : ℕ) :
    (span R s).minorsIdeal p = TauCeti.minorsIdealOfSet s p

    Minors of a submodule generated by s can be computed using only rows in s.

    source
    theorem TauCeti.minorsIdealOfSet_eq_of_span_eq {R : Type u_1} {F : Type u_2} [CommRing R] [AddCommGroup F] [Module R F] {s t : Set F} (h : Submodule.span R s = Submodule.span R t) (p : ℕ) :
    minorsIdealOfSet s p = minorsIdealOfSet t p

    Sets generating the same relation submodule have the same minors ideal.

    source
    theorem TauCeti.fittingIdeal_eq_minorsIdealOfSet {R : Type u_3} {F : Type u_4} {M : Type u_5} [CommRing R] [AddCommGroup F] [Module R F] [Module.Free R F] [Module.Finite R F] [AddCommGroup M] [Module R M] [Module.Finite R M] {φ : F →ₗ[R] M} (hφ : Function.Surjective ⇑φ) (s : Set F) (hs : Submodule.span R s = φ.ker) (k : ℕ) :
    fittingIdeal R M k = minorsIdealOfSet s (Module.finrank R F - k)

    Compute a Fitting ideal from generators of the kernel of a finite free presentation. No finiteness assumption on the chosen generating set is needed.