Skip to content

feat(RingTheory): adds a few IsLocalHom instances to AlgHom #36245

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
BryceT233 wants to merge 9 commits into from
+13 −0
Closed

feat(RingTheory): adds a few IsLocalHom instances to AlgHom #36245

Changes from 7 commits
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
7f0e4fc
Update Basic.lean
BryceT233 Mar 6, 2026
413570e
Update Basic.lean
BryceT233 Mar 6, 2026
1e2e5d1
Update Basic.lean
BryceT233 Mar 6, 2026
895666e
Merge branch 'leanprover-community:master' into aux_local_hom
BryceT233 Mar 15, 2026
212cda7
Merge branch 'leanprover-community:master' into aux_local_hom
BryceT233 Mar 23, 2026
799ea43
Update Basic.lean
BryceT233 Mar 31, 2026
3c859b5
Merge branch 'leanprover-community:master' into aux_local_hom
BryceT233 Mar 31, 2026
9ab8866
apply suggestions
BryceT233 Apr 1, 2026
ab8c29f
apply suggestions
BryceT233 Apr 1, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
21 changes: 21 additions & 0 deletions Mathlib/RingTheory/LocalRing/RingHom/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -53,6 +53,27 @@ theorem RingHom.domain_isLocalRing {R S : Type*} [Semiring R] [CommSemiring S] [
simp_rw [← map_mem_nonunits_iff f, f.map_add]
exact IsLocalRing.nonunits_add

section AlgHom

variable {A : Type*} [CommSemiring A] [Algebra A R] [Algebra A S] [Algebra A T]

variable (A) in
@[instance]
theorem isLocalHom_algHomId : IsLocalHom (AlgHom.id A R) := ⟨fun _ ↦ id⟩

@[instance]
theorem AlgHom.isLocalHom_comp (f : R →ₐ[A] S) (g : S →ₐ[A] T) [IsLocalHom f] [IsLocalHom g] :
IsLocalHom (g.comp f) where
map_nonunit a := IsLocalHom.map_nonunit a ∘ IsLocalHom.map_nonunit (f := g) (f a)
Comment on lines +60 to +65
Copy link
Copy Markdown
Contributor

@j-loreaux j-loreaux Apr 1, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Can you say why you want these to be instances? I know there are reasons for RingHoms, but I'm not sure about AlgHoms. Also, note that we generally write instance foo ... instead of @[instance] theorem foo ....

Copy link
Copy Markdown
Contributor Author

@BryceT233 BryceT233 Apr 1, 2026 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks for the advice! I am trying to design the category of local algebras with a fixed residue field, which will eventually lead to the base category used in deformation theory (see https://stacks.math.columbia.edu/tag/06GC for the definition of a base category). It is still a work-in-progress, but you can view a one-file version of it here: https://github.com/BryceT233/deformation_theory_basics

Since the morphisms in this category are local AlgHoms, I thought it would be better to have IsLocalHom instances directly for AlgHom. I could try to work around this by coercing the AlgHoms to RingHoms, but I'm worried that might not lead to the ideal shape for the definition.

About the style issue, I think I was just copying the existing style from RingHom part of the code above in the same file, usually I used instance too :)


-- see note [lower instance priority]
@[instance 100]
theorem isLocalHom_toAlgHom {F : Type*} [FunLike F R S]
[AlgHomClass F A R S] (f : F) [IsLocalHom f] : IsLocalHom (f : R →ₐ[A] S) :=
⟨IsLocalHom.map_nonunit (f := f)⟩

end AlgHom

end

section
Expand Down
Loading