PR Permission

Stream: mathlib4

[Mattias Ehatamm]

Hello,
I'm working under Peter Nelson in adding Matroids to Mathlib4. Could someone give me PR permission?
username: mehatamm

[Johan Commelin]

Welcome! Voila: https://github.com/leanprover-community/mathlib4/invitations

[Madison Crim]

Is this ready for a pull request?

import Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
open Ideal

variable  (R : Type*) [CommSemiring R](S : Type*) [CommSemiring S] [Algebra R S] (M: Submonoid R)

theorem LocalRing.not_mem_maximalIdeal{R : Type u_1} [CommSemiring R] [LocalRing R] (x : R) :
x ∉ LocalRing.maximalIdeal R ↔ IsUnit x := by
  simp only [mem_maximalIdeal, mem_nonunits_iff, not_not]


noncomputable def nilradMax_localization_isSelf (h: (nilradical R).IsMaximal) (h' : (0:R) ∉ M)
 [IsLocalization M S]  : R ≃ₐ[R] S := by
  have : LocalRing R := by
    refine LocalRing.of_unique_max_ideal ⟨nilradical R, h, fun I hI ↦ ?_⟩
    rw [nilradical_eq_sInf] at h ⊢
    apply (IsMaximal.eq_of_le h (IsMaximal.ne_top hI) (sInf_le (Set.mem_setOf.mpr (IsMaximal.isPrime hI) ))).symm
  have : ∀ m ∈ M, IsUnit m := by
    intro m hm
    apply (LocalRing.not_mem_maximalIdeal m).mp
    rw [← LocalRing.eq_maximalIdeal h]
    intro hm'
    obtain ⟨k, hk⟩ := mem_nilradical.mp hm'
    rw [← hk] at h'
    exact h' (Submonoid.pow_mem M hm k)
  exact IsLocalization.atUnits _ _ this

[Kim Morrison]

Looks plausible to me!

[Yury G. Kudryashov]

Note that defs should use lowerCamelCase for names.

[Madison Crim]

Okay, can I please have permission on Github? My username is maddycrim.

[Shaowei Lin]

Hi, I'm Shaowei Lin from the Topos Institute. David Spivak, Andre Muricy, Solomon Bothwell and I have been formalizing polynomial functors for mathlib4. Can I have permissions to the repo? My handle is shaoweilin .

[Julian Berman]

(Welcome to both of you!) @Madison Crim I think the maintainers usually find it helpful if you say something about what you hope to work on / contribute and/or what your background is. oh, I see, I confused this with the other long thread for asking for GH permissions. You obviously are contributing exactly what you sent above.

[Shaowei Lin]

Thanks @Julian Berman ! I should have mentioned that our work will fall under Category Theory, if that wasn't obvious from the topic :stuck_out_tongue_wink:

[Julian Berman]

@maintainers ^

[Julian Berman]

(deleted)

[Floris van Doorn]

@Shaowei Lin invite sent

[Kim Morrison]

@Madison Crim, invitation sent

[Johan Commelin]

@Shaowei Lin Nice! Please make sure to coordinate with @Sina H 𓃵 @Emily Riehl and others. They also have a formalization of polynomial functors. (Let's start a different thread to discuss this.)

[Sina Hazratpour 𓃵]

@Shaowei Lin A formalization of polynomial functors can be found here:
https://github.com/sinhp/Poly

[Sina Hazratpour 𓃵]

This was done during the summer during the trimester program at HIM, Bonn. I was planning to push some of this to mathlib in the coming weeks. Of course, would be happy to join forces as well. Note that our formalization is the most general notion of polynomial functor (slightly more general than LCCCs), so not sure how this compares with your formalization.