feat: define geometrically reduced algebras #27400

dleijnse · 2025-07-23T19:49:08Z

Define geometrically reduced algebras, and prove that if all finitely generated subalgebras of an algebra A are geometrically reduced, then A is geometrically reduced.

introduced geometrically reduced algebras.

github-actions · 2025-07-23T19:50:23Z

PR summary 3d51c1a073

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.RingTheory.Nilpotent.GeometricallyReduced` (new file)	1986

Declarations diff

+ FGsubalgebra_baseChange_of_element
+ IsGeometricallyReduced
+ all_FG_geometricallyReduced_isGeometricallyReduced
+ geometricallyReduced_indep_of_algebraicClosure
+ isGeometricallyReduced_isReduced
+ isGeometricallyReduced_of_injective
+ notReduced_has_nilpotent
+ subAlgebraBaseChange

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

kckennylau

Congratulations on your first PR! Please don't be deterred by how many comments there are, this is perfectly normal.

Please check in each theorem and def that the implicit and explicit variables are correct. In general, if a variable can be inferred (i.e. appears) in any later variables, then the original variable can be made implicit.

And please sure you state things in the correct generality, where "correct" means "maximal".

I'll give this a second-round to make sure the names fit mathlib's covnention.

Mathlib/RingTheory/Nilpotent/GeometricallyReduced.lean

kckennylau · 2025-07-23T23:47:46Z

Mathlib/RingTheory/Nilpotent/GeometricallyReduced.lean

+def subAlgebraBaseChange (C : Subalgebra k A) : Subalgebra B (TensorProduct k B A) :=
+  AlgHom.range (baseChange k C A C.val B)


Please move this to Mathlib/RingTheory/TensorProduct/Basic.lean
and make only B and C explicit.

kckennylau · 2025-07-24T00:03:51Z

Mathlib/RingTheory/Nilpotent/GeometricallyReduced.lean

+lemma FGsubalgebra_baseChange_of_element (x : TensorProduct k A B) :
+    ∃ C : Subalgebra k B , C.FG ∧ x ∈ subAlgebraBaseChange k B A C := by
+  obtain ⟨S, hS⟩ := TensorProduct.exists_finset x
+  let S1 := Set.image (fun j ↦ j.2) S.toSet
+  let C := Algebra.adjoin k S1
+  use C
+  constructor
+  · rw [Subalgebra.fg_def]
+    use S1
+    refine ⟨?_, rfl⟩
+    exact Set.Finite.image (fun j ↦ j.2) (Finset.finite_toSet S)
+  · rw [hS]
+    refine Subalgebra.sum_mem _ ?_
+    intro s hs
+    have hCS : ∀ i ∈ S, i.2 ∈ C := by
+      intro i hi
+      apply SetLike.mem_of_subset
+      · apply Algebra.subset_adjoin
+      · use i
+        exact ⟨hi, rfl⟩
+    use s.1 ⊗ₜ[k] ⟨s.2, hCS s hs⟩
+    rfl


Suggested change

lemma FGsubalgebra_baseChange_of_element (x : TensorProduct k A B) :

∃ C : Subalgebra k B , C.FG ∧ x ∈ subAlgebraBaseChange k B A C := by

obtain ⟨S, hS⟩ := TensorProduct.exists_finset x

let S1 := Set.image (fun j ↦ j.2) S.toSet

let C := Algebra.adjoin k S1

use C

constructor

· rw [Subalgebra.fg_def]

use S1

refine ⟨?_, rfl⟩

exact Set.Finite.image (fun j ↦ j.2) (Finset.finite_toSet S)

· rw [hS]

refine Subalgebra.sum_mem _ ?_

intro s hs

have hCS : ∀ i ∈ S, i.2 ∈ C := by

intro i hi

apply SetLike.mem_of_subset

· apply Algebra.subset_adjoin

· use i

exact ⟨hi, rfl⟩

use s.1 ⊗ₜ[k] ⟨s.2, hCS s hs⟩

rfl

lemma FGsubalgebra_baseChange_of_element (x : A ⊗[k] B) :

∃ C : Subalgebra k B, C.FG ∧ x ∈ subAlgebraBaseChange k B A C := by

obtain ⟨S, hS⟩ := TensorProduct.exists_finset x

classical

refine ⟨Algebra.adjoin k (S.image fun j ↦ j.2), ?_, ?_⟩

· exact Subalgebra.fg_adjoin_finset _

· exact hS ▸ Subalgebra.sum_mem _ fun s hs ↦ ⟨s.1 ⊗ₜ[k] ⟨s.2, Algebra.subset_adjoin

(Finset.mem_image_of_mem _ hs)⟩, rfl⟩

When you're proving it at first, you can use let and etc. to explore around, but after proving it you can clean those up.

Please also move this lemma to the file suggested above, and make sure to prove things with minimal assumptions.

kckennylau · 2025-07-24T00:12:34Z

Mathlib/RingTheory/Nilpotent/GeometricallyReduced.lean

+-- reduced. The result is in https://stacks.math.columbia.edu/tag/030T
+theorem all_FG_geometricallyReduced_isGeometricallyReduced
+    (h : ∀ B : Subalgebra k A, B.FG → IsGeometricallyReduced k B) :
+    IsGeometricallyReduced k A := by


I haven't looked at this proof yet.

this proof has nothing to do with the algebraic closure, or even that k is a field. You should generalise this theorem.

kckennylau

I have suggested name changes to follow mathlib convention.

kckennylau · 2025-07-24T00:18:36Z

Mathlib/RingTheory/Nilpotent/GeometricallyReduced.lean

+  exact isReduced_of_injective fK hfK
+
+
+theorem isGeometricallyReduced_isReduced [IsGeometricallyReduced k A] : IsReduced A := by


Suggested change

theorem isGeometricallyReduced_isReduced [IsGeometricallyReduced k A] : IsReduced A := by

theorem isReduced_of_isGeometricallyReduced [IsGeometricallyReduced k A] : IsReduced A := by

Remember that the main statement always goes first, followed by the assumptions separated by of.

kckennylau · 2025-07-24T00:20:18Z

Mathlib/RingTheory/Nilpotent/GeometricallyReduced.lean

+
+/-- Given a subalgebra C of a k-algebra A, and a k-algebra B, the basechange of C to a subalgebra
+of A ⊗[k] B -/
+def subAlgebraBaseChange (C : Subalgebra k A) : Subalgebra B (TensorProduct k B A) :=


Suggested change

def subAlgebraBaseChange (C : Subalgebra k A) : Subalgebra B (TensorProduct k B A) :=

def Subalgebra.baseChange (C : Subalgebra k A) : Subalgebra B (TensorProduct k B A) :=

This allows you to use dot notation, i.e. you can use s.baseChange B to base change a sub-algebra s to B.

kckennylau · 2025-07-24T00:21:43Z

Mathlib/RingTheory/Nilpotent/GeometricallyReduced.lean

+def subAlgebraBaseChange (C : Subalgebra k A) : Subalgebra B (TensorProduct k B A) :=
+  AlgHom.range (baseChange k C A C.val B)
+
+lemma FGsubalgebra_baseChange_of_element (x : TensorProduct k A B) :


Suggested change

lemma FGsubalgebra_baseChange_of_element (x : TensorProduct k A B) :

lemma exists_fg_and_mem_baseChange (x : TensorProduct k A B) :

kckennylau · 2025-07-24T00:22:53Z

Mathlib/RingTheory/Nilpotent/GeometricallyReduced.lean

+
+-- If all finitely generated subalgebras of A are geometrically reduced, then A is geometrically
+-- reduced. The result is in https://stacks.math.columbia.edu/tag/030T
+theorem all_FG_geometricallyReduced_isGeometricallyReduced


Suggested change

theorem all_FG_geometricallyReduced_isGeometricallyReduced

theorem IsGeometricallyReduced.of_FG

…en algebraic closure

dleijnse added 4 commits July 22, 2025 21:14

Added the file GeometricallyReduced.lean, which

5f9b4cb

introduced geometrically reduced algebras.

Small changes

4421515

Ran lake exe mk_all

eb009ad

Replaced import Mathlib by minimal imports

339c9d0

github-actions bot added new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-algebra Algebra (groups, rings, fields, etc) labels Jul 23, 2025

Added more documentation

6369aec

kckennylau suggested changes Jul 24, 2025

View reviewed changes

dleijnse added 6 commits July 24, 2025 22:11

Changed tensor product notation

7d6f52e

Removed definition of baseChange

274ede1

Remove baseChange_of_inj

ce19a00

Add proof that being geometrically reduced is independent of the chos…

17b0390

…en algebraic closure

Make some variables implicit

e5e9abd

added instance attribute

fbd25e1

		def subAlgebraBaseChange (C : Subalgebra k A) : Subalgebra B (TensorProduct k B A) :=
		AlgHom.range (baseChange k C A C.val B)

		exact isReduced_of_injective fK hfK


		theorem isGeometricallyReduced_isReduced [IsGeometricallyReduced k A] : IsReduced A := by

	theorem isGeometricallyReduced_isReduced [IsGeometricallyReduced k A] : IsReduced A := by
	theorem isReduced_of_isGeometricallyReduced [IsGeometricallyReduced k A] : IsReduced A := by

	def subAlgebraBaseChange (C : Subalgebra k A) : Subalgebra B (TensorProduct k B A) :=
	def Subalgebra.baseChange (C : Subalgebra k A) : Subalgebra B (TensorProduct k B A) :=

	lemma FGsubalgebra_baseChange_of_element (x : TensorProduct k A B) :
	lemma exists_fg_and_mem_baseChange (x : TensorProduct k A B) :

	theorem all_FG_geometricallyReduced_isGeometricallyReduced
	theorem IsGeometricallyReduced.of_FG

feat: define geometrically reduced algebras #27400

Are you sure you want to change the base?

feat: define geometrically reduced algebras #27400

Conversation

dleijnse commented Jul 23, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Jul 23, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 3d51c1a073

Import changes for modified files

Declarations diff

Uh oh!

kckennylau left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

kckennylau left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

dleijnse commented Jul 23, 2025 •

edited

Loading

github-actions bot commented Jul 23, 2025 •

edited

Loading

kckennylau left a comment •

edited

Loading