instSemilatticeInf — Mathlib

Lean4
instance : SemilatticeInf (IdealSheafData X)
    where
  inf I
    J :=
    { ideal := I.ideal ⊓ J.ideal
      map_ideal_basicOpen U
        f := by
        dsimp
        have : (X.presheaf.map (homOfLE (X.basicOpen_le f)).op).hom = algebraMap _ _ := rfl
        have inst := U.2.isLocalization_basicOpen f
        rw [← I.map_ideal_basicOpen U f, ← J.map_ideal_basicOpen U f, this]
        ext x
        obtain ⟨x, s, rfl⟩ := IsLocalization.mk'_surjective (.powers f) x
        simp only [IsLocalization.mk'_mem_map_algebraMap_iff, Submonoid.mem_powers_iff, Ideal.mem_inf,
          exists_exists_eq_and]
        refine ⟨fun ⟨n, h₁, h₂⟩ ↦ ⟨⟨n, h₁⟩, ⟨n, h₂⟩⟩, ?_⟩
        rintro ⟨⟨n₁, h₁⟩, ⟨n₂, h₂⟩⟩
        refine ⟨n₁ + n₂, ?_, ?_⟩
        · rw [add_comm, pow_add, mul_assoc]; exact Ideal.mul_mem_left _ _ h₁
        · rw [pow_add, mul_assoc]; exact Ideal.mul_mem_left _ _ h₂ }
  inf_le_left I J U := inf_le_left
  inf_le_right I J U := inf_le_right
  le_inf I J K hIJ hIK U := le_inf (hIJ U) (hIK U)
Похожие утверждения