feat(RingTheory): etale lifting property of henselian local rings

Mathlib.lean

@@ -6669,6 +6669,7 @@ public import Mathlib.RingTheory.Ideal.Quotient.PowTransition
 public import Mathlib.RingTheory.Ideal.Span
 public import Mathlib.RingTheory.IdealFilter.Basic
 public import Mathlib.RingTheory.IdealFilter.Topology
+public import Mathlib.RingTheory.IdempotentInstances
 public import Mathlib.RingTheory.Idempotents
 public import Mathlib.RingTheory.Int.Basic
 public import Mathlib.RingTheory.IntegralClosure.Algebra.Basic
@@ -6747,6 +6748,7 @@ public import Mathlib.RingTheory.LocalRing.ResidueField.Ideal
 public import Mathlib.RingTheory.LocalRing.ResidueField.Instances
 public import Mathlib.RingTheory.LocalRing.ResidueField.Polynomial
 public import Mathlib.RingTheory.LocalRing.RingHom.Basic
+public import Mathlib.RingTheory.LocalRing.RingHom.IsIntegral
 public import Mathlib.RingTheory.LocalRing.Subring
 public import Mathlib.RingTheory.Localization.Algebra
 public import Mathlib.RingTheory.Localization.AsSubring

Mathlib/Algebra/Algebra/Equiv.lean

@@ -768,10 +768,10 @@ def algHomUnitsEquiv (R S : Type*) [CommSemiring R] [Semiring S] [Algebra R S] :
 instance _root_.Finite.algEquiv [Finite (A₁ →ₐ[R] A₂)] : Finite (A₁ ≃ₐ[R] A₂) :=
   Finite.of_injective _ AlgEquiv.coe_toAlgHom_injective
 
--- TODO Morally this is just `isLocalHom_equiv`: can we obviate the need for this instance?
-instance : IsLocalHom e.toAlgHom := by
-  have : IsLocalHom e.toRingEquiv := inferInstance
-  exact ⟨this.map_nonunit⟩
+-- TODO Morally these are just `isLocalHom_equiv`: can we obviate the need for this instance?
+instance : IsLocalHom e.toAlgHom := ⟨by simp⟩
+instance : IsLocalHom e.toRingEquiv.toRingHom := ⟨by simp⟩
+instance : IsLocalHom e.toAlgHom.toRingHom := ⟨by simp⟩
 
 end Semiring
 

Mathlib/LinearAlgebra/Dimension/Free.lean

@@ -360,6 +360,17 @@ noncomputable def _root_.LinearEquiv.smul_id_of_finrank_eq_one (d1 : Module.finr
     simp [← (LinearMap.existsUnique_eq_smul_id_of_finrank_eq_one d1 _).choose_spec.2 c]
   right_inv u := ((u.existsUnique_eq_smul_id_of_finrank_eq_one d1).choose_spec.1).symm
 
+lemma finrank_eq_one_iff_algebraMap_bijective
+    {R S : Type*} [CommSemiring R] [CommSemiring S] [StrongRankCondition R] [Algebra R S]
+    [Module.Free R S] :
+    Module.finrank R S = 1 ↔ Function.Bijective (algebraMap R S) := by
+  constructor
+  · intro H
+    let := (Module.basisUnique Unit H).repr ≪≫ₗ Finsupp.uniqueLinearEquiv _ _ .unit
+    exact (LinearEquiv.algEquivOfRing this.symm).bijective
+  · intro H
+    rw [← (AlgEquiv.ofBijective (Algebra.ofId R S) H).toLinearEquiv.finrank_eq, finrank_self]
+
 end Module
 
 end StrongRankCondition

Mathlib/RingTheory/IdempotentInstances.lean

@@ -0,0 +1,27 @@
+/-
+Copyright (c) 2026 Andrew Yang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Andrew Yang
+-/
+module
+
+public import Mathlib.RingTheory.Flat.Stability
+public import Mathlib.RingTheory.Idempotents
+
+/-! # Instances on corners -/
+
+@[expose] public section
+
+variable {R A : Type*} [CommSemiring R]
+  [CommSemiring A] [Algebra R A] {e : A} (he : IsIdempotentElem e)
+
+instance [Module.Projective R A] : Module.Projective R he.Corner :=
+  .of_split ⟨⟨Subtype.val, fun _ _ ↦ rfl⟩, fun _ _ ↦ rfl⟩
+    (IsScalarTower.toAlgHom _ A _).toLinearMap
+    (LinearMap.ext fun a ↦ Subtype.ext ((Subsemigroup.mem_corner_iff he).mp a.2).2)
+
+instance [Module.Flat R A] : Module.Flat R he.Corner :=
+  .trans R A _
+
+instance [Module.Finite R A] : Module.Finite R he.Corner :=
+  .of_surjective (IsScalarTower.toAlgHom _ _ _).toLinearMap he.algebraMap_corner_surjective

Mathlib/RingTheory/Idempotents.lean

@@ -5,6 +5,7 @@ Authors: Andrew Yang
 -/
 module
 
+public import Mathlib.Algebra.Algebra.Tower
 public import Mathlib.Algebra.BigOperators.Fin
 public import Mathlib.Algebra.Ring.GeomSum
 public import Mathlib.RingTheory.Ideal.Quotient.Operations
@@ -587,6 +588,47 @@ instance [NonUnitalCommRing R] (idem : IsIdempotentElem e) : CommRing idem.Corne
   __ : NonUnitalCommRing idem.Corner :=
     inferInstanceAs <| NonUnitalCommRing (NonUnitalRing.corner e)
 
+instance {R S : Type*} [CommSemiring R] [Semiring S] [Algebra R S]
+    {e : S} (he : IsIdempotentElem e) : Algebra R he.Corner where
+  smul r x := ⟨r • x.1, by
+    simp [he, Subsemigroup.mem_corner_iff, (Subsemigroup.mem_corner_iff he).mp x.2]⟩
+  algebraMap :=
+  { toFun r := ⟨r • e, by simp [he, Subsemigroup.mem_corner_iff, he.eq]⟩
+    map_one' := by simp; rfl
+    map_mul' a b := Subtype.ext <| show (a * b) • e = (a • e) * (b • e) by
+      simp [he.eq, ← mul_smul, mul_comm]
+    map_zero' := by simp; rfl
+    map_add' a b := Subtype.ext (add_smul _ _ _) }
+  commutes' r x := Subtype.ext (show r • e * x.1 = x.1 * r • e by
+    simp [(Subsemigroup.mem_corner_iff he).mp x.2])
+  smul_def' r x := Subtype.ext (show r • x.1 = (r • e) * x.1 by
+    simp [(Subsemigroup.mem_corner_iff he).mp x.2])
+
+instance {R R' S : Type*} [CommSemiring R] [CommSemiring R'] [Semiring S] [Algebra R S]
+    [Algebra R R'] [Algebra R' S] [IsScalarTower R R' S]
+    {e : S} (he : IsIdempotentElem e) : IsScalarTower R R' he.Corner :=
+  .of_algebraMap_eq fun _ ↦ Subtype.ext (IsScalarTower.algebraMap_smul _ _ _).symm
+
+@[simp]
+lemma IsIdempotentElem.algebraMap_corner_apply
+    {R S : Type*} [CommSemiring R] [Semiring S] [Algebra R S]
+    {e : S} (he : IsIdempotentElem e) (x : R) :
+    (algebraMap R he.Corner x).1 = x • e := rfl
+
+lemma IsIdempotentElem.algebraMap_corner_surjective [CommSemiring R]
+    {e : R} (he : IsIdempotentElem e) :
+    Function.Surjective (algebraMap R he.Corner) :=
+  fun x ↦ ⟨x.1, Subtype.ext ((Subsemigroup.mem_corner_iff he).mp x.2).2⟩
+
+lemma IsIdempotentElem.ker_algebraMap_corner [CommRing R] {e : R} (he : IsIdempotentElem e) :
+    RingHom.ker (algebraMap R he.Corner) = Ideal.span {1 - e} := by
+  apply le_antisymm
+  · intro x hx
+    refine Ideal.mem_span_singleton.mpr ⟨x, ?_⟩
+    simp [show x * e = 0 from congr($(hx).1), sub_mul, mul_comm e]
+  · simpa [Ideal.span_le, sub_eq_zero, -FaithfulSMul.ker_algebraMap_eq_bot] using!
+      Subtype.ext he.eq.symm
+
 variable {I : Type*} [Fintype I] {e : I → R}
 
 /-- A complete orthogonal family of central idempotents in a semiring

Mathlib/RingTheory/LocalRing/RingHom/IsIntegral.lean

@@ -0,0 +1,26 @@
+/-
+Copyright (c) 2026 Andrew Yang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Andrew Yang
+-/
+module
+public import Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
+public import Mathlib.RingTheory.LocalRing.RingHom.Basic
+
+/-! # Integral ring homomorphisms over local rings are local -/
+
+@[expose] public section
+
+variable {R S : Type*} [CommRing R] [CommRing S] [Algebra R S]
+
+instance [IsLocalRing R] [Algebra.IsIntegral R S] [Nontrivial S] :
+    IsLocalHom (algebraMap R S) := by
+  have : (algebraMap R S).kerLift.IsIntegral :=
+    .tower_top (Ideal.Quotient.mk _) _
+      (by have := algebraMap_isIntegral_iff.mpr ‹Algebra.IsIntegral R S›; exact this)
+  have := this.isLocalHom (algebraMap R S).kerLift_injective
+  have : Nontrivial (R ⧸ RingHom.ker (algebraMap R S)) :=
+    Ideal.Quotient.nontrivial_iff.mpr (RingHom.ker_ne_top _)
+  have : IsLocalHom (Ideal.Quotient.mk (RingHom.ker (algebraMap R S))) :=
+    .of_surjective _ Ideal.Quotient.mk_surjective
+  exact RingHom.isLocalHom_comp (algebraMap R S).kerLift (Ideal.Quotient.mk _)